Commit 4b4c6350 authored by MARCHE Claude's avatar MARCHE Claude

add another tab for server log, and make the resize bar work (!)

parent 06a1fb7f
......@@ -89,6 +89,9 @@ why3.conf
/bin/why3wc.opt
/bin/why3wc.byte
/bin/why3wc
/bin/why3webserver.opt
/bin/why3webserver.byte
/bin/why3webserver
# /doc/
/doc/version.tex
......@@ -194,6 +197,9 @@ pvsbin/
/src/util/config.ml
/src/util/lexlib.ml
/src/util/rc.ml
/src/util/json_lexer.ml
/src/util/json_parser.mli
/src/util/json_parser.ml
# /src/session
/src/session/xml.ml
......@@ -203,6 +209,10 @@ pvsbin/
# /src/tools
/src/tools/why3wc.ml
# /src/ide
/src/ide/why3_js.byte
/src/ide/why3_js.js
# /plugins/tptp/
/plugins/tptp/tptp_lexer.ml
/plugins/tptp/tptp_parser.ml
......
......@@ -95,13 +95,22 @@
<span class="why3-tab-label why3-widget" >Task tree</span>
<div class="why3-widget why3-tab">
<div id="why3-task-list" class="why3-widget">
Ceci est l'arbre des taches</div>
Ceci est l'arbre des taches</div>
</div>
<span class="why3-tab-label why3-widget why3-inactive">Source code</span>
<div id="why3-editor-container" class="why3-container">
<div id="why3-editor-bg" class="why3-widget"> </div>
<div id="why3-editor" tabindex="-1" ></div>
</div>
<div class="why3-widget why3-tab">
<div id="why3-editor-container" class="why3-container">
<div id="why3-editor-bg" class="why3-widget"> </div>
<div id="why3-editor" tabindex="-1" ></div>
</div>
</div>
<span class="why3-tab-label why3-widget why3-inactive">Log</span>
<div class="why3-widget why3-tab">
<div id="why3-error-container" class="why3-container">
<div id="why3-error-bg" class="why3-widget"></div>
<iframe name="form-answer"></iframe>
</div>
</div>
</div>
</div>
......@@ -116,14 +125,6 @@
</div>
<!-- TODO to be changed error -->
<div id="why3-error-panel" class="why3-wide-view">
<span class="why3-tab-label why3-widget why3-inactive">Errors</span>
<div id="why3-error-container" class="why3-container">
<div id="why3-error-bg" class="why3-widget"> </div>
<div id="why3-error" tabindex="-1" ></div>
</div>
</div>
<!-- TODO saisie -->
<div id="why3-form-cont" class="why3-wide-view">
......@@ -132,7 +133,6 @@
action="http://localhost:6789/request" target="form-answer">
<input type="text" name="Command">
</form>
<iframe name="form-answer"></iframe>
</div>
......
......@@ -42,6 +42,9 @@ module AsHtml =
let span e = element e
end
let select e cls =
Dom.list_of_nodeList (e ## querySelectorAll (Js.string cls))
let getElement_exn cast id =
Js.Opt.get (cast (Dom_html.getElementById id)) (fun () -> raise Not_found)
......@@ -86,6 +89,33 @@ let readBody (xhr: XmlHttpRequest.xmlHttpRequest Js.t) =
exception TODO1
exception TODO2
module Tabs =
struct
let () =
let tab_groups = select Dom_html.document ".why3-tab-group" in
List.iter
(fun tab_group ->
let labels = select tab_group ".why3-tab-label" in
List.iter (
(fun tab ->
tab ##. onclick :=
Dom.handler
(fun _ev ->
List.iter
(fun t ->
ignore (t ##. classList ## add (Js.string "why3-inactive")))
labels;
tab ##. classList ## remove (Js.string "why3-inactive");
Js._false))
) labels)
tab_groups
end
module Editor =
struct
type range
......@@ -327,6 +357,39 @@ let sendRequest r =
sendRequest (convert_request r)
module Panel =
struct
let main_panel = getElement AsHtml.div "why3-main-panel"
let tab_container = getElement AsHtml.div "why3-tab-container"
let resize_bar = getElement AsHtml.div "why3-resize-bar"
let reset () =
let edit_style = tab_container ##. style in
JSU.(set edit_style (Js.string "flexGrow") (Js.string "2"));
JSU.(set edit_style (Js.string "flexBasis") (Js.string ""))
let () =
let mouse_down = ref false in
resize_bar ##. onmousedown := Dom.handler (fun _ -> mouse_down := true; Js._false);
resize_bar ##. ondblclick := Dom.handler (fun _ -> reset (); Js._false);
main_panel ##. onmouseup := Dom.handler (fun _ -> mouse_down := false; Js._false);
main_panel ##. onmousemove :=
Dom.handler (fun e ->
if !mouse_down then begin
let offset =
(e ##. clientX) - (main_panel ##. offsetLeft)
in
let offset = Js.string ((string_of_int offset) ^ "px") in
let edit_style = tab_container ##. style in
JSU.(set edit_style (Js.string "flexGrow") (Js.string "0"));
JSU.(set edit_style (Js.string "flexBasis") offset);
Js._false
end
else Js._true)
end
module TaskList =
struct
......
<?xml version="1.0" encoding="UTF-8"?>
<!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
"http://why3.lri.fr/why3session.dtd">
<why3session shape_version="4">
<prover id="0" name="Alt-Ergo" version="0.99.1" timelimit="2" steplimit="1" memlimit="0"/>
<prover id="1" name="CVC4" version="1.4" timelimit="10" steplimit="1" memlimit="0"/>
<prover id="2" name="Alt-Ergo" version="1.01" timelimit="10" steplimit="1" memlimit="0"/>
<prover id="3" name="Z3" version="4.4.1" timelimit="1" steplimit="1" memlimit="0"/>
<file name="../demo-itp.mlw">
<theory name="Power" sum="578b01834fce822dc9327264318cf1d0">
<goal name="power_1">
<proof prover="3"><result status="valid" time="0.02"/></proof>
<transf name="introduce_premises" >
<goal name="power_1.0">
<transf name="replace" arg1="1" arg2="0+1" arg3="power_1">
<goal name="power_1.0.0">
<transf name="replace" arg1="1" arg2="(0+1)" arg3="power_1">
<goal name="power_1.0.0.0">
<proof prover="0"><result status="valid" time="0.00" steps="3"/></proof>
</goal>
<goal name="power_1.0.0.1">
</goal>
</transf>
<transf name="rewrite" arg1="power_s">
<goal name="power_1.0.0.0">
<transf name="rewrite" arg1="power_0">
<goal name="power_1.0.0.0.0">
<transf name="compute_in_goal" >
</transf>
</goal>
</transf>
</goal>
<goal name="power_1.0.0.1">
<transf name="compute_in_goal" >
</transf>
</goal>
</transf>
</goal>
<goal name="power_1.0.1">
<transf name="compute_in_goal" >
</transf>
</goal>
</transf>
</goal>
</transf>
</goal>
<goal name="sqrt4_256">
<proof prover="1"><result status="unknown" time="0.01"/></proof>
<proof prover="2"><result status="unknown" time="0.01"/></proof>
<proof prover="3" timelimit="10"><result status="timeout" time="10.00"/></proof>
<transf name="exists" arg1="4">
<goal name="sqrt4_256.0">
<proof prover="3"><result status="valid" time="0.03"/></proof>
</goal>
</transf>
</goal>
<goal name="power_sum">
<transf name="introduce_premises" >
<goal name="power_sum.0">
<transf name="induction" arg1="n" arg2="0">
<goal name="power_sum.0.0">
<proof prover="3"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="power_sum.0.1">
<proof prover="2" timelimit="1"><result status="valid" time="0.02" steps="11"/></proof>
<proof prover="3"><result status="timeout" time="0.99"/></proof>
</goal>
</transf>
</goal>
</transf>
</goal>
<goal name="power_0_left">
<transf name="introduce_premises" >
<goal name="power_0_left.0">
<transf name="induction" arg1="n" arg2="1">
<goal name="power_0_left.0.0">
<proof prover="3"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="power_0_left.0.1">
<proof prover="3"><result status="valid" time="0.01"/></proof>
</goal>
</transf>
</goal>
</transf>
</goal>
<goal name="little_fermat_3">
<transf name="introduce_premises" >
<goal name="little_fermat_3.0">
<transf name="induction" arg1="x" arg2="0">
<goal name="little_fermat_3.0.0">
<proof prover="1"><result status="unknown" time="0.01"/></proof>
<proof prover="2"><result status="timeout" time="10.01"/></proof>
<proof prover="3" timelimit="10"><result status="timeout" time="9.74"/></proof>
<transf name="exists" arg1="0">
<goal name="little_fermat_3.0.0.0">
<proof prover="2" timelimit="1"><result status="valid" time="0.00" steps="4"/></proof>
<proof prover="3"><result status="timeout" time="1.00"/></proof>
</goal>
</transf>
</goal>
<goal name="little_fermat_3.0.1">
<transf name="destruct" arg1="little_fermat_3">
<goal name="little_fermat_3.0.1.0">
<transf name="remove" arg1="little_fermat_31">
<goal name="little_fermat_3.0.1.0.0">
<transf name="exists" arg1="y+x*(x+1)">
<goal name="little_fermat_3.0.1.0.0.0">
<transf name="replace" arg1="power (x+1) 3" arg2="power (x+1) (0+1+1+1)" arg3="G">
<goal name="little_fermat_3.0.1.0.0.0.0">
<proof prover="1"><result status="unknown" time="0.00"/></proof>
<proof prover="2"><result status="timeout" time="10.00"/></proof>
<proof prover="3" timelimit="10"><result status="timeout" time="9.64"/></proof>
<transf name="replace" arg1="power x 3" arg2="power x (0+1+1+1)" arg3="little_fermat_3">
<goal name="little_fermat_3.0.1.0.0.0.0.0">
<proof prover="1"><result status="unknown" time="0.01"/></proof>
<proof prover="2"><result status="timeout" time="10.00"/></proof>
<proof prover="3" timelimit="10"><result status="timeout" time="9.68"/></proof>
<transf name="rewrite" arg1="power_s">
<goal name="little_fermat_3.0.1.0.0.0.0.0.0">
<proof prover="1"><result status="unknown" time="0.01"/></proof>
<proof prover="2"><result status="timeout" time="10.01"/></proof>
<proof prover="3" timelimit="10"><result status="timeout" time="9.65"/></proof>
<transf name="rewrite" arg1="power_s">
<goal name="little_fermat_3.0.1.0.0.0.0.0.0.0">
<transf name="rewrite" arg1="power_s">
<goal name="little_fermat_3.0.1.0.0.0.0.0.0.0.0">
<proof prover="1"><result status="timeout" time="10.91"/></proof>
<proof prover="2"><result status="timeout" time="10.01"/></proof>
<proof prover="3" timelimit="10"><result status="timeout" time="9.75"/></proof>
</goal>
<goal name="little_fermat_3.0.1.0.0.0.0.0.0.0.1">
</goal>
</transf>
</goal>
<goal name="little_fermat_3.0.1.0.0.0.0.0.0.1">
</goal>
</transf>
</goal>
<goal name="little_fermat_3.0.1.0.0.0.0.0.1">
</goal>
</transf>
</goal>
<goal name="little_fermat_3.0.1.0.0.0.0.1">
</goal>
</transf>
</goal>
<goal name="little_fermat_3.0.1.0.0.0.1">
<proof prover="3"><result status="valid" time="0.01"/></proof>
</goal>
</transf>
</goal>
</transf>
</goal>
</transf>
</goal>
</transf>
</goal>
</transf>
</goal>
</transf>
</goal>
</theory>
</file>
<file name="../../examples/isqrt.mlw">
<theory name="Square" sum="9d10f7a99e3dc8b97241d913352efc97">
<goal name="sqr_non_neg">
</goal>
<goal name="sqr_increasing">
</goal>
<goal name="sqr_sum">
</goal>
</theory>
<theory name="Simple" sum="3eedbf7f16a30c54f16ce00579ce34b2">
<goal name="WP_parameter isqrt">
</goal>
<goal name="WP_parameter main">
</goal>
</theory>
<theory name="NewtonMethod" sum="ea55a43436c4d177632e02b018206bd5">
<goal name="WP_parameter sqrt">
</goal>
</theory>
</file>
</why3session>
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment