File tree Expand file tree Collapse file tree 5 files changed +16565
-12762
lines changed Expand file tree Collapse file tree 5 files changed +16565
-12762
lines changed Original file line number Diff line number Diff line change @@ -54,11 +54,12 @@ <h1><img style="display: inline;" src="/pluginIcon.svg" width="26"> T
54
54
< option value ="examples/lambda/lambda_app.tidy "> Lambda Calculus</ option >
55
55
< option value ="examples/def_before_use/def_before_use.tidy "> Def-Before-Use</ option >
56
56
</ select >
57
- < label > Generation timeout:< input id ="timeout " type ="number " value ="1000 " min ="100 " step ="100 " style ="margin-left: 0.4em; margin-right: 0.4em; width: 5em " > ms</ label > < div style ="margin-right: 4em "> </ div >
57
+ < label > Generation timeout:< input id ="timeout " type ="number " value ="300 " min ="100 " step ="100 " style ="margin-left: 0.4em; margin-right: 0.4em; width: 5em " > ms</ label > < div style ="margin-right: 4em "> </ div >
58
58
< label for ="minimize-checkbox "> Minimize repairs </ label >
59
- < input type ="checkbox " id ="minimize-checkbox ">
59
+ < input type ="checkbox " id ="minimize-checkbox " checked >
60
60
</ div >
61
61
< div id ="confrow2 ">
62
+ < div id ="gpuAvail " style ="margin-right: 330px; margin-top:-45px "> </ div >
62
63
< label > Max edit distance: < a href ="https://en.wikipedia.org/wiki/Edit_distance#Language_edit_distance "> LED</ a > + < input id ="max-edits " type ="number " value ="1 " min ="0 " max ="3 " step ="1 " style ="margin-right: 0.4em "> </ label > < div style ="margin-right: 4.43em "> </ div >
63
64
< label for ="ntstubs-checkbox "> Nonterminal stubs </ label >
64
65
< input type ="checkbox " id ="ntstubs-checkbox " checked >
Original file line number Diff line number Diff line change @@ -55,12 +55,12 @@ <h1><img style="display: inline;" src="/pluginIcon.svg" width="26"> T
55
55
</ div >
56
56
</ div >
57
57
< div title ="Minimizes total edits per repair. " id ="confrow1 ">
58
- < label > Generation timeout: < input id ="timeout " type ="number " value ="1000 " min ="100 " step =" 100 " style =" margin-left: 0.4em; margin-right: 0.4em; width: 5em " > ms </ label > < div style ="margin-right: 4em "> </ div >
58
+ < label > Max edit distance: < a href =" https://en.wikipedia.org/wiki/Edit_distance#Language_edit_distance " > LED </ a > + < input id ="max-edits " type ="number " value ="2 " min ="0 " max =" 3 " step =" 1 " style ="margin-right: 4.2em "> </ label >
59
59
< label for ="minimize-checkbox "> Minimize repairs </ label >
60
60
< input type ="checkbox " id ="minimize-checkbox " checked >
61
61
</ div >
62
62
< div title ="Adds nonterminal stubs to CFG. " id ="confrow2 ">
63
- < label > Max edit distance: < a href =" https://en.wikipedia.org/wiki/Edit_distance#Language_edit_distance " > LED </ a > + < input id ="max-edits " type =" number " value =" 2 " min =" 0 " max =" 3 " step =" 1 " style ="margin-right: 12.2em " > </ label > < div style =" margin-right: 4.43em "> </ div >
63
+ < div id ="gpuAvail " style ="margin-right: 770px; margin-top:-50px "> </ div >
64
64
<!-- <label for="ntstubs-checkbox">Nonterminal stubs </label>-->
65
65
<!-- <input type="checkbox" id="ntstubs-checkbox" checked>-->
66
66
</ div >
You can’t perform that action at this time.
0 commit comments