[trywhy3]: * clean-up source-code highlighting

           * Preliminary implementation of a tabbed view with the Task pretty printed
           * General clean-up
           * Split theh css into a mandatory one and a customizable one.

src/trywhy3/editor_helper.js

 /* Global objects */
 var editor = ace.edit("editor");
+var task_editor = ace.edit("task-editor");
+var Range = ace.require('ace/range').Range;
 editor.setTheme("ace/theme/chrome");
 editor.getSession().setMode("ace/mode/why3");
 editor.$blockScrolling = Infinity;
 
+task_editor.setTheme("ace/theme/chrome");
+task_editor.getSession().setMode("ace/mode/why3");
+task_editor.$blockScrolling = Infinity;
+task_editor.setReadOnly(true);
+
 function openFile ()
 {
     document.getElementById("file-selector").click();

src/trywhy3/trywhy3.css

@@ -26,14 +26,27 @@
 /* ACE Editor */
 .error {
     position:absolute;
-    background:rgba(200,100,100,0.5);
-    z-index:40;
+    background:rgba(231,113,116,1);
+    z-index:70;
+}
+
+.loc-neg-premise {
+    position:absolute;
+    background:rgba(255,128,64,1);
+    z-index:60;
 }
-.hl-task {
+
+.loc-goal {
     position:absolute;
-    background:rgba(200,200,100,1);
+    background:rgba(64,191,255,1);
+    z-index:50;
+}
+.loc-premise {
+    position:absolute;
+    background:rgba(100,233,134,1);
     z-index:40;
 }
+
 /* Interface */
 body {
     padding:0;
@@ -53,6 +66,56 @@ body {
     width:100%;
 }
 
+.tab-header {
+    display:inline-block;
+    border-radius: 0.25em 0.25em 0 0;
+    vertical-align:middle;
+    text-align:center;
+    padding:0.25em 0.75em;
+    margin-top:0.25em;
+    margin-left:0.25em;
+    margin-right:0.25em;
+    background: #ddd;
+    height:1.5em;
+    line-height:1.5em;
+    font-size:14pt;
+    z-index:0;
+} /*total height 0.25 * 2 + 0.25 +1.5 = 2.25 em; */
+
+.tab-body {
+    display:block;
+    position:absolute;
+    background: #ddd;
+    bottom:0;
+    top:2.25em;
+    left:0;
+    right:0;
+    z-index: 0;
+}
+
+#task-editor {
+    height:100%;
+    width:100%;
+    font-size: large;
+    
+}
+
+.tab-header.alert {
+    color:red;
+    font-weight:bold;
+}
+.tab-header.active {
+    z-index:10;
+    background:#eee;
+}
+.tab-body.active
+ {
+    z-index:10;
+    bottom:0;
+    top:2.25em;
+    width:100%;
+    background:#eee;
+}
 
 #editor-panel.wide-view #editor {
     position:absolute;
@@ -61,18 +124,18 @@ body {
     width:48rem;
     height:100%;
 }
-#editor-panel.wide-view #console {
+#editor-panel.wide-view #tab-panel {
     position:absolute;
     left:48rem;
     right:0;
     height:100%;
 }
-#editor-panel.standard-view #editor {
+#editor-panel.standard-view #editor  {
     position:relative;
     width:100%;
     height:50%;
 }
-#editor-panel.standard-view #console {
+#editor-panel.standard-view #tab-panel {
     position:relative;
     width:100%;
     height:49%;
@@ -84,35 +147,27 @@ body {
     display:inline-block;
     margin: 0 ;
     padding:0;
-    z-index:0;
+    z-index:5;
     vertical-align:top;
     border-right: 1pt  #ddd solid;
     border-bottom: 1pt #ddd solid;
 }
 
-#console {
-    box-sizing: border-box;
-    overflow: auto;
-    position:relative;
-    display:inline-block;
-    margin:0 ;
-    padding:0.5em ;
-    vertical-align:top;
-}
-
 /* CSS MENU BAR */
 
 .menu-bar {
     position:absolute;
     top:0pt;
     margin:0;
-    z-index:10;
+    z-index:100;
     font-size:14pt;
     height:18pt;
     padding:0;
     width:100%;
 }
-
+.menu-bar * {
+    z-index:100;
+}
 .menu-bar:after {
     content:"";
     display:table;
@@ -125,7 +180,6 @@ body {
     list-style: none;
     position: relative;
     background-image: linear-gradient(to bottom, #eee, #ccc);
-    z-index:10;
     height:18pt;
     box-sizing:border-box;
     }
@@ -278,8 +332,8 @@ body {
     top:0;
     left:-1.5em;
     width:1.25em;
-    border-bottom: 2pt solid #ddd;
-    border-left: 2pt solid #ddd;
+    border-bottom: 2pt solid #aaa;
+    border-left: 2pt solid #aaa;
 }
 
 

src/trywhy3/trywhy3.html

@@ -12,6 +12,7 @@ yamlpp -l en src/trywhy3/index.prehtml -o src/trywhy3/index.en.html  -->
     </title>
     <meta http-equiv="Content-Type" content="text/html; charset=utf-8" />
     <link rel="stylesheet" type="text/css" href="trywhy3.css" />
+    <link rel="stylesheet" type="text/css" href="trywhy3_custom.css" />
     <!-- color customisation -->
     <style>
 
@@ -106,7 +107,14 @@ yamlpp -l en src/trywhy3/index.prehtml -o src/trywhy3/index.en.html  -->
     <div id="editor-panel" class="wide-view">
       <div id="editor" title="Editor" tabindex="-1" ></div><!--
       Don't leave white-spaces between editor and console div's
-     --><div title="Console" id="console">
+      --><div id="tab-panel">
+        <!-- First list all the tab headers in spans, with an id equal
+             to the id of the corresponding tab below, with the suffix     -tab
+             then list all the tab content in divs -->
+        <span id="console-tab" class="tab-header active">Task list</span>
+        <span id="task-view-tab" class="tab-header" >Task</span>
+        <div id="console" class="tab-body active"> </div>
+        <div id="task-view" class="tab-body"><div id="task-editor"></div></div>
       </div>
     </div>
     <script defer="true" src="ace-builds/src-noconflict/ace.js"

src/trywhy3/trywhy3.ml

@@ -20,16 +20,25 @@ module Editor =
   struct
     type range
     type marker
+
     let editor =
       let open Js.Unsafe in
       get global (Js.string "editor")
+    let task_editor =
+      let open Js.Unsafe in
+      get global (Js.string "task_editor")
 
-    let get_buffer_js () : Js.js_string Js.t =
+    let get_value ?(editor=editor) () : Js.js_string Js.t =
       let open Js.Unsafe in
       meth_call editor "getValue" [| |]
 
+    let set_value ?(editor=editor) str =
+      let open Js.Unsafe in
+      ignore (meth_call editor "setValue" [| inject (Js.string str); inject ~-1 |])
+
+
     let get_buffer () =
-      Js.to_string (get_buffer_js ())
+      Js.to_string (get_value ())
 
     let mk_range l1 c1 l2 c2 =
       let open Js.Unsafe in
@@ -88,11 +97,51 @@ module Editor =
 module Console =
   struct
 
+
+    let tabs =
+      let headers = Dom_html.document ## getElementsByClassName (Js.string "tab-header") in
+      List.fold_left (fun acc t ->
+                      let tab_id = t ## id in
+                      let i = tab_id ## lastIndexOf (Js.string "-tab") in
+                      let len = tab_id ## length in
+                      if i == len - 4 then
+                        try
+                          let tab = Dom_html.getElementById (Js.to_string (tab_id ## substring(0,i))) in
+                          (t, tab) :: acc
+                        with
+                          Not_found -> acc
+                      else acc
+                     )
+                     [] (Dom.list_of_nodeList headers)
+    let () =
+      List.iter (fun (th, tb) ->
+                 let cb = fun idh idb _ ->
+                   List.iter (fun (h,b) ->
+                              if Js.to_string (h ## id) = idh &&
+                                   Js.to_string (b ## id) = idb
+                              then begin
+                                  h ## classList ## add (Js.string "active");
+                                  b ## classList ## add (Js.string "active");
+                                end
+                              else begin
+                                  h ## classList ## remove (Js.string "active");
+                                  b ## classList ## remove (Js.string "active");
+                                end;
+                             ) tabs;
+                   th ## classList ## remove (Js.string "alert");
+                   Js._false
+
+                 in
+                 th ## onclick <- Dom.handler (cb (Js.to_string th ## id) (Js.to_string tb ## id)))
+                tabs
+
+
     let get_console () =
         get_opt (Dom_html.document ## getElementById (Js.string "console"))
 
     let clear () =
-      (get_console ()) ## innerHTML <- (Js.string "")
+      (get_console ()) ## innerHTML <- Js.string "";
+      Editor.set_value ~editor:Editor.task_editor ""
 
     let print cls msg =
         (get_console ()) ## innerHTML <-
@@ -154,10 +203,11 @@ module Console =
 
     let task_selection = Hashtbl.create 17
     let is_selected id = Hashtbl.mem task_selection id
-    let select_task id span loc =
+    let select_task id span loc pretty =
       (span ## classList) ## add (Js.string "task-selected");
-      let markers = List.map (Editor.add_marker "hl-task") loc in
-      Hashtbl.add task_selection id (span, loc, markers)
+      let markers = List.map (fun (cls, range) -> Editor.add_marker cls range) loc in
+      Hashtbl.add task_selection id (span, loc, markers);
+      Editor.set_value ~editor:Editor.task_editor pretty
 
     let deselect_task id =
       try
@@ -212,15 +262,15 @@ module Console =
       | Theory (th_id, th_name) ->
 	 attach_to_parent th_id "theory-list" th_name []
 
-      | Task (id, parent_id, expl, _code, loc) ->
+      | Task (id, parent_id, expl, _code, locs, pretty) ->
 	 begin
 	   try
 	     ignore (Dom_html.getElementById id)
 	   with Not_found ->
-		attach_to_parent id (parent_id ^ "_ul") expl loc;
+		attach_to_parent id (parent_id ^ "_ul") expl locs;
 		let span = Dom_html.getElementById (id ^ "_container") in
-                let buffer = Editor.get_buffer_js () in
-                let loc = List.map (Editor.why3_loc_to_range buffer) loc in
+                let buffer = Editor.get_value () in
+                let locs = List.map (fun (k, loc) -> k, Editor.why3_loc_to_range buffer loc) locs in
 		span ## onclick <-
 		  Dom.handler
 		    (fun ev ->
@@ -230,7 +280,7 @@ module Console =
 			 clear_task_selection ()
 		     else begin
 			 if not ctrl then clear_task_selection ();
-                         select_task id span loc
+                         select_task id span locs pretty
                        end;
 		     Js._false)
 	 end
@@ -341,7 +391,7 @@ let init_why3_worker () =
                   Console.print_why3_output msg;
                   let () =
                     match msg with
-                      Task (id,_,_,code,_) ->
+                      Task (id,_,_,code,_,_) ->
 		      log ("Got task " ^ id);
 		      push_task (Goal (id,code))
                     | _ -> ()

src/trywhy3/trywhy3_custom.css

+/* You can modify the values below to alter the default look of trywhy3 */
+
+/*** TASKS ***/
+
+/* Color of the icon used to show a task is being proved */
+.task-pending {
+    color: blue;
+}
+
+/* Color of the icon used to show a task is proved */
+.task-valid {
+    color:green;
+}
+
+/* Color of the icon used to show the status of a task is unproven */
+.task-unknown {
+    color:orange;
+}
+
+/* Color of the icon used to show the status of a task has been aborted */
+.task-abort {
+    color:black;
+}
+
+/* Style used to for selected tasks */
+.task-selected {
+    background:rgba(250,220,90,0.7);
+}
+
+/*** EDITOR ***/
+
+/*** Warning: for highlighting properties, do not
+    modify the position or z-index property.
+    You should not use alpha-transparency (either opacity < 1 or rgba colors)
+    since some highlight region overlaps. 
+
+/* Color used to highlight errors in the editor */
+.error {
+    background:rgb(231,113,116);
+}
+
+/* Color used to highlight negative premises of a task in the editor */
+.loc-neg-premise {
+    background:rgb(255,128,64);
+}
+
+/* Color used to highlight goals of a task in the editor */
+.loc-goal {
+    background:rgb(64,191,255);
+}
+
+/* Color used to highlight premises of a task in the editor */
+.loc-premise {
+    background:rgb(100,233,134);
+}
\ No newline at end of file

src/trywhy3/why3_worker.ml

@@ -54,6 +54,8 @@ let alt_ergo_driver : Driver.driver =
 let () = log_time ("Initialising why3 worker: end ")
 
 let split_trans = Trans.lookup_transform_l "split_goal_wp" env
+let intro_trans = Trans.lookup_transform "introduce_premises" env
+
 (* CF gmain.ml ligne 568 et suivante *)
 module W =
   struct
@@ -76,6 +78,7 @@ module Task =
 	mutable subtasks : id list;
 	loc : why3_loc list;
 	expl : string;
+        pretty : string;
       }
 
     let task_table : (id, task_info) Hashtbl.t = Hashtbl.create 17
@@ -91,35 +94,31 @@ module Task =
     let get_parent_id id = (get_info id).parent_id
 
     let mk_loc (_, a,b,c) = (a,b,c)
+    let premise_kind = function
+      | { Term. t_node = Term.Tnot _; t_loc = None } -> "loc-neg-premise"
+    | _ -> "loc-premise"
     let collect_locs t =
       (* from why 3 ide *)
       let locs = ref [] in
-      let rec get_locs f =
-        Opt.iter (fun loc -> locs := (mk_loc (Loc.get loc)) :: !locs) f.Term.t_loc;
-        Term.t_fold (fun () t -> get_locs t ) () f
+      let rec get_locs kind f =
+        Opt.iter (fun loc -> locs := (kind, mk_loc (Loc.get loc)) :: !locs) f.Term.t_loc;
+        Term.t_fold (fun () t -> get_locs kind t ) () f
       in
       let rec get_t_locs f =
         match f.Term.t_node with
         | Term.Tbinop (Term.Timplies,f1,f2) ->
-           get_locs f1;
+           get_locs (premise_kind f1) f1;
            get_t_locs f2
         | Term.Tlet (t,fb) ->
            let _,f1 = Term.t_open_bound fb in
-           get_locs t;
+           get_locs (premise_kind t) t;
            get_t_locs f1
         | Term.Tquant (Term.Tforall,fq) ->
            let _,_,f1 = Term.t_open_quant fq in
            get_t_locs f1
         | _ ->
-           get_locs f
+           get_locs "loc-goal" f
       in
-      (*
-      let rec merge_locs = function
-          [] | [ _ ] as l -> l
-          | ((l1, b1, e1) as h1) :: ((l2, b2, e2) as h2) :: ll ->
-             if l1 != l2 then h1 :: (merge_locs (h2 :: ll))
-             else
-       *)
       match t with
       | Some { Task.task_decl =
                  { Theory.td_node =
@@ -136,6 +135,9 @@ module Task =
       let c = ref 0 in
       fun () -> incr c; "id" ^ (string_of_int !c)
 
+    let task_text t =
+      Pp.string_of Pretty.print_task t
+
     let register_task parent_id task =
       let id = gen_id () in
       let vid, expl, _ = Termcode.goal_expl_task ~root:false task in
@@ -145,7 +147,7 @@ module Task =
       in
       let id_loc = match vid.Ident.id_loc with
           None -> []
-        | Some l -> [ mk_loc (Loc.get l) ]
+        | Some l -> [ ("loc-goal",mk_loc (Loc.get l)) ]
       in
       let task_info =
         { task = `Task(task);
@@ -153,7 +155,9 @@ module Task =
 	  status = `New;
 	  subtasks = [];
 	  loc = id_loc @  (collect_locs task);
-	  expl = expl }
+	  expl = expl;
+          pretty = task_text (Trans.apply intro_trans task); 
+        }
       in
       Hashtbl.add task_table id task_info;
       id
@@ -169,7 +173,9 @@ module Task =
 				      status = `New;
 				      subtasks = task_ids;
 				      loc = [];
-				      expl = th_name };
+				      expl = th_name;
+                                      pretty = "";
+                                    };
       th_id
 
     let get_task = function `Task t -> t
@@ -230,7 +236,7 @@ let rec why3_prove id =
   match t.subtasks with
     [] ->  t.status <- `Unknown;
 	  let task = get_task t.task in
-	  let msg = Task (id, t.parent_id, t.expl, task_to_string task, t.loc) in
+	  let msg = Task (id, t.parent_id, t.expl, task_to_string task, t.loc, t.pretty) in
 	  W.send msg;
 	  let l = set_status id `New in
           List.iter W.send l

src/trywhy3/worker_proto.ml

 type id = string
 type loc = int * int * int * int
-type why3_loc = int * int * int (* line, column, length *)
+type why3_loc = string * (int * int * int) (* kind, line, column, length *)
 type status = [`New | `Valid | `Unknown ]
 type why3_command =  ParseBuffer of string
               | ExecuteBuffer of string
@@ -10,7 +10,8 @@ type why3_command =  ParseBuffer of string
 type why3_output = Error of string (* msg *)
                  | ErrorLoc of (loc * string) (* loc * msg *)
                  | Theory of id * string (* Theory (id, name) *)
-                 | Task of (id * id * string * string * why3_loc list) (* id, parent id, expl, code, location list *)
+                 | Task of (id * id * string * string * why3_loc list * string)
+                 (* id, parent id, expl, code, location list, pretty *)
                  | Result of string list
                  | UpdateStatus of status * id