changes to do (does not compile yet)

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 session_user_interface itp_server
+	      session_scheduler itp_server
 
 LIBMODULES =  $(addprefix src/util/, $(LIB_UTIL)) \
 	      $(addprefix src/core/, $(LIB_CORE)) \

src/ide/why3ide.ml

@@ -120,7 +120,7 @@ let () =
   Debug.dprintf debug " done.@.";
   Gconfig.init ()
 
-open Session_user_interface.History
+open Itp_server.History
 
 (********************************)
 (* Source language highlighting *)

src/ide/why3web.ml

@@ -33,6 +33,7 @@ let interp_request args =
 
 let print_message_notification fmt n =
   match n with
+  | Error s -> ()
   | Proof_error(nid,s) -> ()
   | Transf_error(nid,s) -> ()
   | Strat_error(nid,s) -> ()
@@ -102,4 +103,35 @@ let stdin_handler s =
     | "q" -> exit 0
     | _ -> printf "unknown command '%s'@." s
 
-let () = Wserver.main_loop None 6789 handler stdin_handler
+(************************)
+(* parsing command line *)
+(************************)
+
+let files : string Queue.t = Queue.create ()
+
+let opt_parser = ref None
+
+let spec = Arg.align [
+  "-F", Arg.String (fun s -> opt_parser := Some s),
+      "<format> select input format (default: \"why\")";
+  "--format", Arg.String (fun s -> opt_parser := Some s),
+      " same as -F";
+(*
+  "-f",
+   Arg.String (fun s -> input_files := s :: !input_files),
+   "<file> add file to the project (ignored if it is already there)";
+*)
+  Termcode.arg_extra_expl_prefix
+]
+
+let usage_str = sprintf
+  "Usage: %s [options] [<file.why>|<project directory>]..."
+  (Filename.basename Sys.argv.(0))
+
+
+let () =
+  Whyconf.Args.parse spec (fun f -> Queue.add f files) usage_str;
+  if Queue.is_empty files then
+     Whyconf.Args.exit_with_usage spec usage_str;
+  Queue.iter (fun f -> P.push_request (Itp_server.Open_req f, Itp_server.root_node)) files;
+  Wserver.main_loop None 6789 handler stdin_handler

src/session/controller_itp.ml

@@ -71,12 +71,33 @@ type controller =
     controller_provers : (Whyconf.config_prover * Driver.driver) Whyconf.Hprover.t;
   }
 
-let create_controller env = {
+exception LoadDriverFailure of Whyconf.config_prover * exn
+
+let create_controller env provers =
+  let c = {
     controller_session = Session_itp.dummy_session;
     proof_state = init_proof_state ();
     controller_env = env;
     controller_provers = Whyconf.Hprover.create 7;
-}
+    }
+  in
+  (* load provers drivers *)
+  Whyconf.Mprover.iter
+    (fun _ p ->
+       try
+         let d = Driver.load_driver env p.Whyconf.driver [] in
+         Whyconf.Hprover.add c.controller_provers p.Whyconf.prover (p,d)
+       with e -> raise (LoadDriverFailure(p,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;
+  c
+
 
 let init_controller s c =
   c.controller_session <- s
@@ -302,7 +323,7 @@ let read_file env ?format fn =
     find a corresponding new theory resp. old goal are kept, with
     tasks associated to them *)
 
-let merge_file (old_ses : session) (c : controller) env ~use_shapes _ file =
+let merge_file (old_ses : session) (c : controller) ~use_shapes _ file =
   let format = file.file_format in
   let old_theories = file.file_theories in
   let file_name = Filename.concat (get_dir old_ses) file.file_name in
@@ -313,16 +334,17 @@ let merge_file (old_ses : session) (c : controller) env ~use_shapes _ file =
       []
   in
   merge_file_section
-    c.controller_session ~use_shapes ~old_ses ~old_theories ~env file_name new_theories format;
+    c.controller_session ~use_shapes ~old_ses ~old_theories
+    ~env:c.controller_env file_name new_theories format;
   Stdlib.Hstr.iter
     (fun _ f -> List.iter (reload_theory_proof_state c) f.file_theories)
     (get_files c.controller_session)
 
 
-let reload_files (c : controller) (env : Env.env) ~use_shapes =
+let reload_files (c : controller) ~use_shapes =
   let old_ses = c.controller_session in
   c.controller_session <- empty_session ~shape_version:(get_shape_version old_ses) (get_dir old_ses);
-  Stdlib.Hstr.iter (merge_file old_ses c env ~use_shapes) (get_files old_ses)
+  Stdlib.Hstr.iter (merge_file old_ses c ~use_shapes) (get_files old_ses)
 
 let add_file c ?format fname =
   let theories = read_file c.controller_env ?format fname in

src/session/controller_itp.mli

@@ -78,8 +78,13 @@ type controller = private
     controller_provers : (Whyconf.config_prover * Driver.driver) Whyconf.Hprover.t;
   }
 
-val create_controller: Env.env -> controller
+exception LoadDriverFailure of Whyconf.config_prover * exn
+val create_controller:
+  Env.env -> Whyconf.config_prover Whyconf.Mprover.t -> controller
+(** creates a controller with an empty session *)
+
 val init_controller: Session_itp.session -> controller -> unit
+(** adds a session to a controller *)
 
 (** Used to find if a proof/trans node or theory is proved or not *)
 val tn_proved: controller -> Session_itp.transID -> bool
@@ -89,7 +94,7 @@ val file_proved: controller -> Session_itp.file -> bool
 
 val print_session : Format.formatter -> controller -> unit
 
-val reload_files : controller -> Env.env -> use_shapes:bool -> unit
+val reload_files : controller -> use_shapes:bool -> unit
 (** reload the files of the given session:
 
   - each file is parsed again and theories/goals extracted from it. If

src/session/itp_server.mli

@@ -7,18 +7,20 @@ type strategy = string
 type node_ID = int
 val root_node : node_ID
 
-(* --------------------------- types to be expanded if needed --------------------------------- *)
 
-type node_type =
-  | NRoot
-  | NFile
-  | NTheory
-  | NTransformation
-  | NGoal
-  | NProofAttempt of Call_provers.prover_answer option * bool
+module type History_type = sig
+  type history
+
+  val create_history: unit -> history
+  val print_next_command: history -> string option
+  val print_prev_command: history -> string option
+  val add_command: history -> string -> unit
+
+end
+
+module History : History_type
 
-type node_info = { proved : bool; (* TODO: add more *)
-                   name   : string }
+(* --------------------------- types to be expanded if needed --------------------------------- *)
 
 (* Global information known when server process has started and that can be
    shared with the IDE through communication *)
@@ -51,12 +53,28 @@ type message_notification =
   (* An error happened that could not be identified in server *)
   | Error        of string
 
+type node_type =
+  | NRoot
+  | NFile
+  | NTheory
+  | NTransformation
+  | NGoal
+  | NProofAttempt (* of Call_provers.prover_answer option * bool *)
+
+type update_info =
+  | Proved of bool
+  | Proof_status_change of
+      Controller_itp.proof_attempt_status
+      * bool   (* obsolete or not *)
+      * Call_provers.resource_limit
+   (* or 3 constructors if better *)
+
 type notification =
-  | Node_change  of node_ID * node_info
-  (* inform that the data of the given node changed *)
-  | New_node     of node_ID * node_ID * node_type * node_info
+  | New_node     of node_ID * node_ID * node_type * string
   (* Notification of creation of new_node:
-     New_node (new_node, parent_node, new_node_type, new_node_content). *)
+     New_node (new_node, parent_node, node_type, name). *)
+  | Node_change  of node_ID * update_info
+  (* inform that the data of the given node changed *)
   | Remove       of node_ID
   (* the given node was removed *)
   | Initialized  of global_information
@@ -67,10 +85,8 @@ type notification =
   (* an informative message, can be an error message *)
   | Dead         of string
   (* server exited *)
-  | Proof_update of node_ID * Controller_itp.proof_attempt_status
-  (* update proof attempt *)
   | Task         of node_ID * string
-  (* te node_ID's task *)
+  (* the node_ID's task *)
 
 type request_type =
   | Command_req       of string