- complete reload function

- add session directory and restore old session file mechanism

src/session/controller_itp.ml

@@ -335,30 +335,30 @@ let read_file env ?format fn =
 
 let add_file c ?format fname =
   let theories = read_file c.controller_env ?format fname in
-  add_file_section c.controller_session fname theories format (empty_session ()) []
+  add_file_section c.controller_session fname theories format
 
 (** reload files, associating old proof attempts and transformations
     to the new goals.  old theories and old goals for which we cannot
     find a corresponding new theory resp. old goal are kept, with
     tasks associated to them *)
 
-let _merge_file (old_ses : session) (c : controller) _ file =
+let merge_file (old_ses : session) (c : controller) env _ 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
   let new_theories =
     try
-      read_file c.controller_env file.file_name ?format
+      read_file c.controller_env file_name ?format
     with _ -> (* TODO: filter only syntax error and typing errors *)
       []
   in
   add_file_section
-    c.controller_session file.file_name new_theories format old_ses old_theories
+    c.controller_session ~merge:(old_ses,old_theories,env) file_name new_theories format
 
 
-let reload_files (c : controller)  =
+let reload_files (c : controller) (env : Env.env) =
   let old_ses = c.controller_session in
-  c.controller_session <- empty_session ();
-  Stdlib.Hstr.iter (fun _ f -> add_file c f.file_name) (get_files old_ses)
-  (* Stdlib.Hstr.iter (merge_file old_ses c) (get_files old_ses) *)
+  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) (get_files old_ses)
 
 end

src/session/controller_itp.mli

@@ -124,10 +124,10 @@ val run_strategy_on_goal :
     inform of the progress *)
 
 val add_file : controller -> ?format:Env.fformat -> string -> unit
-(** [add_file_to_session cont ?fmt fname] parses the source file
+(** [add_fil cont ?fmt fname] parses the source file
     [fname] and add the resulting theories to the session of [cont] *)
 
-val reload_files : controller -> unit
+val reload_files : controller -> Env.env -> unit
 (** reload the files of the given session:
 
   - each file is parsed again and theories/goals extracted from it. If
@@ -167,9 +167,13 @@ val reload_files : controller -> unit
     generated subgoals are in turn matched to the old sub-goals, in
     the same manner as for goals in a theory
 
+    . an old sub-goals without a match is kept with all its former
+      proof attempts and transformations, but no task is associated to
+      it, neither to its subgoals.
+
   - TODO: the presence of obsolete goals should be returned somehow by
     that function, as the presence of unmatch old theories or goals
 
- *)
+*)
 
 end

src/session/session_itp.mli

@@ -31,14 +31,18 @@ type theory
 
 val theory_name : theory -> Ident.ident
 val theory_goals : theory -> proofNodeID list
+val theory_detached_goals : theory -> proofNodeID list
 
 type file = private {
-  file_name     : string;
-  file_format   : string option;
-  file_theories : theory list;
+  file_name              : string;
+  file_format            : string option;
+  file_theories          : theory list;
+  file_detached_theories : theory list;
 }
 
 val get_files : session -> file Stdlib.Hstr.t
+val get_dir : session -> string
+val get_shape_version : session -> int
 
 (** {2 Proof trees}
 
@@ -53,7 +57,7 @@ type proof_attempt = {
   limit               : Call_provers.resource_limit;
   mutable proof_state : Call_provers.prover_result option;
   (* None means that the call was not done or never returned *)
-  proof_obsolete      : bool;
+  mutable proof_obsolete      : bool;
   proof_script        : string option;  (* non empty for external ITP *)
 }
 
@@ -102,10 +106,10 @@ val print_trans_node : session -> Format.formatter -> transID -> unit
 
 val print_session : Format.formatter -> session -> unit
 
-(* val get_proof_attempts : session -> proofNodeID -> proof_attempt Whyconf.Hprover.t *)
 val get_transformations : session -> proofNodeID -> transID list
 val get_proof_attempts : session -> proofNodeID -> proof_attempt list
 val get_sub_tasks : session -> transID -> proofNodeID list
+val get_detached_sub_tasks : session -> transID -> proofNodeID list
 
 val get_transf_args : session -> transID -> string list
 val get_transf_name : session -> transID -> string
@@ -115,18 +119,20 @@ val get_proof_name : session -> proofNodeID -> Ident.ident
 val get_proof_parent : session -> proofNodeID -> proof_parent
 val get_trans_parent : session -> transID -> proofNodeID
 
-val empty_session : ?shape_version:int -> unit -> session
+val empty_session : ?shape_version:int -> string -> session
+(** create an empty_session in the directory specified by the
+    argument *)
 
 val add_file_section :
-  session -> string -> (Theory.theory list) -> Env.fformat option ->
-  session -> theory list -> unit
-(** [add_file_section s fn ths old_s old_ths] adds a new 'file'
-    section in session [s], named [fn], containing fresh theory
+  ?merge:session*theory list*Env.env -> session -> string ->
+  (Theory.theory list) -> Env.fformat option -> unit
+(** [add_file_section ~merge:(old_s,old_ths,env) s fn ths] adds a new
+    'file' section in session [s], named [fn], containing fresh theory
     subsections corresponding to theories [ths]. The tasks of each
     theory nodes generated are computed using [Task.split_theory]. For
     each theory whose name is identical to one theory of old_ths, it
-    is attempted to associate the old goals, proof_attempts and transformations
-    to the goals of the new theory *)
+    is attempted to associate the old goals, proof_attempts and
+    transformations to the goals of the new theory *)
 
 val graft_proof_attempt : session -> proofNodeID -> Whyconf.prover ->
   timelimit:int -> unit
@@ -155,9 +161,9 @@ val remove_transformation : session -> transID -> unit
 (** [remove_transformation s id] removes the transformation [id]
     from the session [s] *)
 
-val save_session : string -> session -> unit
-(** [save_session f s] Save the session [s] in file [f] *)
+val save_session : session -> unit
+(** [save_session s] Save the session [s] *)
 
 val load_session : string -> session
-(** [load_session f] load a session from a file [f]; all the tasks are
-    initialised to None *)
+(** [load_session dir] load a session in directory [dir]; all the
+    tasks are initialised to None *)

src/why3shell/why3shell.ml

@@ -159,17 +159,25 @@ 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.pop files in
-  let ses =
-    if Filename.check_suffix fname ".xml" then
-      Session_itp.load_session fname
-    else
-      begin
-        Queue.push fname files;
-        Session_itp.empty_session ()
-      end
+  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 = Session_itp.load_session dir in
+  (* create the controller *)
   let c = Controller_itp.create_controller env ses in
+  (* update the session *)
+  C.reload_files c env;
   (* add files to controller *)
   Queue.iter (fun fname -> C.add_file c fname) files;
   (* load provers drivers *)
@@ -371,10 +379,11 @@ let nearest_goal () =
 (* -------------------- printing --------------------------------------- *)
 
 let print_proof_attempt fmt pa =
-  fprintf fmt "%a tl=%d %a"
+  fprintf fmt "%a tl=%d %a obsolete=%a"
           Whyconf.print_prover pa.prover
           pa.limit.Call_provers.limit_time
           (Pp.print_option Call_provers.print_prover_result) pa.proof_state
+          pp_print_bool pa.proof_obsolete
 
 let rec print_proof_node s (fmt: Format.formatter) p =
   let parent = match get_proof_parent s p with
@@ -405,28 +414,34 @@ and print_trans_node s fmt id =
   let name = get_transf_name s id in
   let args = get_transf_args s id in
   let l = get_sub_tasks s id in
+  let ll = get_detached_sub_tasks s id in
   let parent = (get_proof_name s (get_trans_parent s id)).Ident.id_string in
   if Controller_itp.tn_proved cont id then
     fprintf fmt "P";
-  fprintf fmt "@[<hv 2>{ Trans=%s;@ args=%a;@ parent=%s;@ [%a] }@]" name (Pp.print_list Pp.semi pp_print_string) args parent
+  fprintf fmt "@[<hv 2>{ Trans=%s;@ args=%a;@ parent=%s;@ [%a];@ detached[%a] }@]" name
+    (Pp.print_list Pp.semi pp_print_string) args parent
     (Pp.print_list Pp.semi (print_proof_node s)) l
+    (Pp.print_list Pp.semi (print_proof_node s)) ll
 
 let print_theory s fmt th : unit =
   if Controller_itp.th_proved cont (theory_name th) then
     fprintf fmt "P";
-  fprintf fmt "@[<hv 1> Theory %s;@ [%a]@]" (theory_name th).Ident.id_string
-    (Pp.print_list Pp.semi (fun fmt a -> print_proof_node s fmt a)) (theory_goals th)
+  fprintf fmt "@[<hv 1> Theory %s;@ [%a];@ detached[%a]@]" (theory_name th).Ident.id_string
+    (Pp.print_list Pp.semi (print_proof_node s)) (theory_goals th)
+    (Pp.print_list Pp.semi (print_proof_node s)) (theory_detached_goals th)
 
-let print_file s fmt (file, thl) =
-  fprintf fmt "@[<hv 1> File %s;@ [%a]@]" file.file_name
+let print_file s fmt (file, thl, detached) =
+  fprintf fmt "@[<hv 1> File %s;@ [%a];@ detached[%a]@]" file.file_name
     (Pp.print_list Pp.semi (print_theory s)) thl
+    (Pp.print_list Pp.semi (print_theory s)) detached
 
 let print_s s fmt =
   fprintf fmt "@[%a@]" (Pp.print_list Pp.semi (print_file s))
 
 let print_session fmt s =
-  let l = Stdlib.Hstr.fold (fun _ f acc -> (f,f.file_theories) :: acc) (get_files s) [] in
-  fprintf fmt "%a@." (print_s s) l;;
+  let l = Stdlib.Hstr.fold
+      (fun _ f acc -> (f,f.file_theories,f.file_detached_theories) :: acc) (get_files s) [] in
+  fprintf fmt "folder %a %a@." pp_print_string (Session_itp.get_dir s) (print_s s) l;;
 
 let dump_session_raw fmt _args =
   fprintf fmt "%a@." print_session cont.Controller_itp.controller_session
@@ -512,17 +527,12 @@ let apply_transform fmt args =
 
 (*******)
 
-let test_save_session _fmt args =
-  match args with
-  | file :: _ ->
-    Session_itp.save_session (file ^ ".xml") cont.Controller_itp.controller_session;
-    printf "session saved@."
-  | [] ->
-    printf "missing session file name@."
+let test_save_session _fmt _args =
+  Session_itp.save_session cont.Controller_itp.controller_session
 
 let test_reload fmt _args =
   fprintf fmt "Reloading... @?";
-  C.reload_files cont;
+  C.reload_files cont env;
   zipper_init ();
   fprintf fmt "done @."
 
@@ -624,7 +634,7 @@ let commands =
     "st", "<c> apply the strategy whose shortcut is 'c'", run_strategy;
     "g", "prints the current goal", test_print_goal;
     "r", "reload the session (test only)", test_reload;
-    "s", "<file> save the current session in <file>.xml", test_save_session;
+    "s", "save the current session", test_save_session;
     "ng", "go to the next goal", then_print (move_to_goal_ret_p next_node);
     "pg", "go to the prev goal", then_print (move_to_goal_ret_p prev_node);
     "gu", "go to the goal up",  then_print (move_to_goal_ret_p zipper_up);