GTK : display session and task

Makefile.in

@@ -205,7 +205,7 @@ LIB_WHYML = mlw_ty mlw_expr mlw_decl mlw_pretty mlw_wp mlw_module \
 
 LIB_SESSION = compress xml termcode session session_itp			\
               session_tools strategy strategy_parser	\
-              controller_itp session_scheduler
+              controller_itp session_scheduler session_user_interface
 
 LIBMODULES =  $(addprefix src/util/, $(LIB_UTIL)) \
 	      $(addprefix src/core/, $(LIB_CORE)) \

src/ide/why3ide.ml

@@ -40,12 +40,35 @@ let gconfig = try
     eprintf "%a@." Exn_printer.exn_printer e;
     exit 1
 
+let provers : Whyconf.config_prover Whyconf.Mprover.t =
+  Whyconf.get_provers gconfig.config
+
+let cont =
+  Session_user_interface.cont_from_files spec usage_str gconfig.env files provers
+
 let () =
   Debug.dprintf debug "[GUI] Init the GTK interface...@?";
   ignore (GtkMain.Main.init ());
   Debug.dprintf debug " done.@.";
   Gconfig.init ()
 
+
+(************)
+(* controller instance on the GTK scheduler *)
+
+
+module S = struct
+    let idle ~prio f =
+      let (_ : GMain.Idle.id) = GMain.Idle.add ~prio f in ()
+
+    let timeout ~ms f =
+      let (_ : GMain.Timeout.id) = GMain.Timeout.add ~ms ~callback:f in
+      ()
+end
+
+module C = Controller_itp.Make(S)
+
+
 (***************)
 (* Main window *)
 (***************)
@@ -122,8 +145,21 @@ let scrollview =
        gconfig.tree_width <- w)
   in sv
 
-(* temporary *)
-let _ = GMisc.label ~text:"scrollview" ~packing:scrollview#add ()
+(* view for the session tree *)
+let scrolled_session_view =
+  GBin.scrolled_window
+    ~hpolicy: `AUTOMATIC ~vpolicy: `AUTOMATIC
+    ~shadow_type:`ETCHED_OUT
+    ~packing:scrollview#add
+    ()
+
+let session_view =
+  GText.view ~editable:false ~cursor_visible:false
+             ~packing:scrolled_session_view#add ()
+
+let display_session () =
+  let s = Pp.string_of Controller_itp.print_session cont in
+  session_view#buffer#set_text s
 
 let vbox222 = GPack.vbox ~packing:hp#add ()
 
@@ -146,16 +182,40 @@ let task_view =
     ~packing:scrolled_task_view#add
     ()
 
-(* temporary *)
-let () =
-  task_view#source_buffer#set_text "this is the current proof task"
+(* TEMPORARY !!! *)
+let first_goal () =
+  Session_itp.get_task cont.Controller_itp.controller_session (Obj.magic 0)
 
-let command_entry =
-  let e = GEdit.entry ~packing:vbox222#add () in
-  let (_ : GtkSignal.id) =
-    e#connect#activate ~callback:
-      (fun () -> task_view#source_buffer#set_text e#text)
-  in e
+let command_entry = GEdit.entry ~packing:vbox222#add ()
+let message_zone =
+  GText.view ~editable:false ~cursor_visible:false
+             ~packing:vbox222#add ()
+
+let clear_command_entry () = command_entry#set_text ""
+
+let task_driver =
+  let main = Whyconf.get_main gconfig.config in
+  let d = Filename.concat (Whyconf.datadir main)
+                          (Filename.concat "drivers" "why3_itp.drv")
+  in
+  Driver.load_driver cont.Controller_itp.controller_env d []
+
+
+let interp cmd =
+  match cmd with
+    | "p" -> display_session (); clear_command_entry ()
+    | "g" -> clear_command_entry ();
+             let task = first_goal () in
+             let s = Pp.string_of
+                       (Driver.print_task ~cntexample:false task_driver)
+                       task
+             in task_view#source_buffer#set_text s
+
+    | _ -> message_zone#buffer#set_text ("unknown command '"^cmd^"'")
+
+let (_ : GtkSignal.id) =
+  command_entry#connect#activate
+    ~callback:(fun () -> interp command_entry#text)
 
 
 (* start the interface *)

src/printer/why3printer.ml

@@ -430,7 +430,7 @@ let print_sequent _args ?old:_ fmt =
            let tables = build_name_tables task in
            let ut = Task.used_symbols (Task.used_theories task) in
            let ld = Task.local_decls task ut in
-           fprintf fmt "@[<v 0>%a \n=================================================@]"
+           fprintf fmt "@[<v 0>%a@]"
                    (Pp.print_list Pp.newline (print_decl tables)) ld)))
 
 

src/why3shell/why3shell.ml

@@ -154,49 +154,11 @@ let return_prover fmt name =
 
 (* -- init controller -- *)
 
+let cont =
+  Session_user_interface.cont_from_files spec usage_str env files provers
+
 module C = Why3.Controller_itp.Make(Unix_scheduler)
 
-let cont_init () =
-  (* create controller *)
-  if Queue.is_empty files then Why3.Whyconf.Args.exit_with_usage spec usage_str;
-  let fname = Queue.peek files in
-  (* extract project directory, and create it if needed *)
-  let dir =
-    if Filename.check_suffix fname ".why" ||
-       Filename.check_suffix fname ".mlw"
-    then begin
-      let dir = Filename.chop_extension fname in
-      if not (Sys.file_exists dir) then
-        Unix.mkdir dir 0o777;
-      dir
-    end
-    else Filename.dirname fname
-  in
-  (* we load the session *)
-  let ses,use_shapes = Session_itp.load_session dir in
-  eprintf "using shapes: %a@." pp_print_bool use_shapes;
-  (* create the controller *)
-  let c = Controller_itp.create_controller env ses in
-  (* update the session *)
-  Controller_itp.reload_files c env ~use_shapes;
-  (* add files to controller *)
-  Queue.iter (fun fname -> Controller_itp.add_file c fname) files;
-  (* load provers drivers *)
-  Whyconf.Mprover.iter
-    (fun _ p ->
-       try
-         let d = Driver.load_driver env p.Whyconf.driver [] in
-         Whyconf.Hprover.add c.Controller_itp.controller_provers p.Whyconf.prover (p,d)
-       with e ->
-         let p = p.Whyconf.prover in
-         eprintf "Failed to load driver for %s %s: %a@."
-           p.Whyconf.prover_name p.Whyconf.prover_version
-           Exn_printer.exn_printer e)
-    provers;
-  (* return the controller *)
-  c
-
-let cont = cont_init ()
 
 (* --  -- *)