new gmain using generic session manager

Makefile.in

@@ -420,7 +420,7 @@ install_local: bin/why3config
 
 ifeq (@enable_ide@,yes)
 
-IDE_FILES = gconfig db gmain
+IDE_FILES = gconfig db session gmain 
 
 IDEMODULES = $(addprefix src/ide/, $(IDE_FILES))
 

ROADMAP

@@ -10,6 +10,10 @@
 * Jessie3
 * traceability: Partially done
   (Claude)
+  TODO: traceability des hyp comme path dans le prog (depuis
+  Frama-C en particulier)
+  afficher les explications dans les outils en ligne de
+  commande why3 et why3bench + le path
 * Coq plugin
 * Coq realization of theories
   (Andrei)
@@ -28,6 +32,14 @@
   (?)
 * BD : se passer de sqlite3
   (Claude)
+  Solution: un unique fichier XML, qui est ecrit mais pas
+  tres souvent (pas plus d'une fois par seconde)
+  ne pas oublier neanmoins de mettre une action dans Timeout
+  qui enregistre au bout d'un moment
+  pb: n'est pas independant de l'IDE, peut-on faire un module
+  independant de l'IDE ? qui serait utilisé par why3bench ?
+  
+
 * IDE: avoir des transformations non codees en dur
   (Claude d'abord)
 
@@ -68,6 +80,8 @@
 * IDE: debug "hide proved goals" feature
   ** suggested solution: replace model + filter_model by a custom model
 
+* IDE: debug "remove" et "clean" qui provoquent des segfaults !!
+ 
 * IDE: ajouter "invalid" comme cas de resultats de preuve
   (utiliser call_provers.proof_result dans gmain)
   DONE

src/ide/session.mli

@@ -18,13 +18,35 @@
 (**************************************************************************)
 
 
-open Why3
+open Why
+
+type prover_data = private
+    { prover_id : string;
+      prover_name : string;
+      prover_version : string;
+      command : string;
+      driver_name : string;
+      driver : Driver.driver;
+      mutable editor : string;
+    }
+
+type proof_attempt_status = private
+    | Undone
+    | Scheduled (** external proof attempt is scheduled *)
+    | Running (** external proof attempt is in progress *)
+    | Done of Call_provers.prover_result (** external proof done *)
+    | InternalFailure of exn (** external proof aborted by internal error *)
 
 module type OBSERVER = sig
+
   type key
   val create: ?parent:key -> unit -> key
   val notify: key -> unit
   val remove: key -> unit
+
+  val timeout: ms:int -> (unit -> bool) -> unit
+  val idle: (unit -> bool) -> unit
+
 end
 
 module Make(O: OBSERVER) : sig
@@ -35,13 +57,6 @@ module Make(O: OBSERVER) : sig
 (*                           *)
 (*****************************)
 
-  type proof_attempt_status =
-    | Undone
-    | Scheduled (** external proof attempt is scheduled *)
-    | Running (** external proof attempt is in progress *)
-    | Done of Call_provers.prover_result (** external proof done *)
-    | InternalFailure of exn (** external proof aborted by internal error *)
-
   type proof_attempt = private
       { prover : prover_data;
         proof_goal : goal;
@@ -52,11 +67,12 @@ module Make(O: OBSERVER) : sig
       }
 
   and goal_parent =
-    | Theory of theory
-    | Transf of transf
+    | Parent_theory of theory
+    | Parent_transf of transf
 
   and goal = private
       { goal_name : string;
+	goal_expl : string option;
 	parent : goal_parent;
         task: Task.task;
         goal_key : O.key;
@@ -108,22 +124,6 @@ module Make(O: OBSERVER) : sig
         Opening a session must be done prior to any other actions.
         And it cannot be done twice.
 
-        TODO: some scheduling functions might be needed as argument, e.g
-
-        add_idle: (unit -> bool) -> unit
-
-        that will allow to install a handler when context is idle
-
-        add_timeout: ms:int -> (unit -> bool) -> unit
-
-        that will allow to install a handler when a timeout of ms
-        milliseconds occurs
-
-        in both cases, the bool returned indicates whether the handler
-        should be removed or not
-
-        the parameter OBSERVER could also be used for that purpose
-
     *)
 
     (* 
@@ -132,13 +132,16 @@ module Make(O: OBSERVER) : sig
        this is not necessary since the session manager handles this itself
        using add_timeout *)
 
-  val add_file : string -> unit
-    (** adds a new file in the proof session
-    *)
+  val add_file : string -> Theory.theory Theory.Mnm.t -> unit
+    (** [add_file f ths] adds a new file in the proof session, that is
+	a collection of name [f] of theories [ths] *)
+
 
-  val reload_files : unit -> unit 
-    (** reloads all the files in the state, and performs the proper
-        mergind of old proof attemps and transformations *)
+  (*
+    val reload_files : unit -> unit 
+  (** reloads all the files in the state, and performs the proper
+    merging of old proof attemps and transformations *)
+*)
 
 (*****************************)
 (*                           *)
@@ -146,25 +149,26 @@ module Make(O: OBSERVER) : sig
 (*                           *)
 (*****************************)
 
-(* attempt a new proof using an external prover *)
 
-  val add_proof_attempt : goal  -> unit
-    (** TODO: proper arguments missing *)
+  val run_prover : context_unproved_goals_only:bool -> 
+    prover_data -> any -> unit
+    (** [run_prover p a] runs prover [p] on all goals under [a] *)
 
-  val add_transformation : goal -> unit
-    (** TODO: proper arguments missing *)
+  val replay : context_unproved_goals_only:bool -> any -> unit
+    (** [replay a] reruns all valid but obsolete proofs under [a] *)
 
-  val remove_proof_attempf : proof_attempt -> unit
+(*
+
+  val remove_proof_attempt : proof_attempt -> unit
 
   val remove_transformation : transf -> unit
 
   val clean : any -> unit
     (** [clean a] removes failed attempts below [a] where
-        other successful attempts exist *)
-
-  val redo_obsolete : any -> unit
-    (** [redo_obsolete a] rerun obsolete proofs below [a] *)
+        there at least one successful attempt or transformation *)
 
+    *) 
+end