updated DTD of sessions

share/why3session.dtd

@@ -11,10 +11,14 @@
 <!ATTLIST file verified CDATA #REQUIRED>
 <!ATTLIST file expanded CDATA #IMPLIED>
 
-<!ELEMENT theory (goal*)>
+<!ELEMENT theory (label*,goal*)>
 <!ATTLIST theory name CDATA #REQUIRED>
 <!ATTLIST theory verified CDATA #REQUIRED>
 <!ATTLIST theory expanded CDATA #IMPLIED>
+<!ATTLIST theory locfile CDATA #IMPLIED>
+<!ATTLIST theory loclnum CDATA #IMPLIED>
+<!ATTLIST theory loccnumb CDATA #IMPLIED>
+<!ATTLIST theory loccnume CDATA #IMPLIED>
 
 <!ELEMENT goal (proof*, transf*)>
 <!ATTLIST goal name CDATA #REQUIRED>
@@ -23,12 +27,17 @@
 <!ATTLIST goal sum CDATA #REQUIRED>
 <!ATTLIST goal shape CDATA #IMPLIED>
 <!ATTLIST goal expanded CDATA #IMPLIED>
+<!ATTLIST goal locfile CDATA #IMPLIED>
+<!ATTLIST goal loclnum CDATA #IMPLIED>
+<!ATTLIST goal loccnumb CDATA #IMPLIED>
+<!ATTLIST goal loccnume CDATA #IMPLIED>
 
 <!ELEMENT proof (result|undone)>
 <!ATTLIST proof prover CDATA #REQUIRED>
 <!ATTLIST proof timelimit CDATA #REQUIRED>
 <!ATTLIST proof edited CDATA #IMPLIED>
 <!ATTLIST proof obsolete CDATA #IMPLIED>
+<!ATTLIST proof archived CDATA #IMPLIED>
 
 <!ELEMENT result EMPTY>
 <!ATTLIST result status (valid|invalid|unknown|timeout|failure) #REQUIRED>
@@ -40,3 +49,6 @@
 <!ATTLIST transf name CDATA #REQUIRED>
 <!ATTLIST transf proved CDATA #REQUIRED>
 <!ATTLIST transf expanded CDATA #IMPLIED>
+
+<!ELEMENT label EMPTY>
+<!ATTLIST label name CDATA #REQUIRED>

src/ide/gconfig.ml

@@ -753,6 +753,7 @@ an alternative?" Whyconf.print_prover unknown in
     c.altern_provers <- Mprover.add unknown !prover_choosed c.altern_provers;
   !prover_choosed
 
+(**)
 let replace_prover c to_be_removed to_be_copied =
   if not to_be_removed.Session.proof_obsolete &&
     c.replace_prover = CRP_Not_Obsolete
@@ -776,6 +777,7 @@ let replace_prover c to_be_removed to_be_copied =
     | `DELETE_EVENT | `Keep -> false in
   dialog#destroy ();
   res
+(**)
 
 let read_config conf_file extra_files = read_config conf_file extra_files; init ()
 

src/ide/gconfig.mli

@@ -105,8 +105,13 @@ val show_about_window : unit -> unit
 val preferences : t -> unit
 val unknown_prover :
   t -> 'key Session.env_session -> Whyconf.prover -> Whyconf.prover option
+
+(**)
 val replace_prover :
   t -> 'key Session.proof_attempt -> 'key Session.proof_attempt -> bool
+(**)
+
+
 (*
 Local Variables:
 compile-command: "unset LANG; make -C ../.. bin/why3ide.byte"

src/ide/gmain.ml

@@ -669,7 +669,9 @@ let init =
 
 let unknown_prover = Gconfig.unknown_prover gconfig
 
+(**)
 let replace_prover = Gconfig.replace_prover gconfig
+(**)
 
    end)
 
@@ -945,7 +947,7 @@ let (_ : GMenu.image_menu_item) =
 let save_session () =
   if !session_needs_saving then begin
     eprintf "[Info] saving session@.";
-    S.save_session (env_session()).S.session;
+    S.save_session gconfig.config (env_session()).S.session;
     session_needs_saving := false;
   end
 

src/ide/replay.ml

@@ -288,7 +288,7 @@ let same_result r1 r2 =
     | Call_provers.Failure _, Call_provers.Failure _-> true
     | _ -> false
 
-let add_to_check_no_smoke found_obs env_session sched =
+let add_to_check_no_smoke config found_obs env_session sched =
       let session = env_session.S.session in
       let callback report =
         eprintf "@.";
@@ -318,7 +318,7 @@ session NOT updated)@." n m
             if found_obs && (n=m || !opt_force) then
               begin
                 eprintf "Updating obsolete session...@?";
-                S.save_session session;
+                S.save_session config session;
                 eprintf " done@."
               end;
             exit 0
@@ -354,9 +354,9 @@ let add_to_check_smoke env_session sched =
   in
   M.check_all ~callback env_session sched
 
-let add_to_check found_obs =
+let add_to_check config found_obs =
   match !opt_smoke with
-    | SD_None -> add_to_check_no_smoke found_obs;
+    | SD_None -> add_to_check_no_smoke config found_obs;
     | _ -> assert (not found_obs); add_to_check_smoke
 
 let transform_smoke env_session =
@@ -389,7 +389,7 @@ let () =
     end;
     (* M.smoke_detector := !opt_smoke; *)
     eprintf " done.";
-    add_to_check found_obs env_session sched;
+    add_to_check config found_obs env_session sched;
     main_loop (); 
     eprintf "main replayer exited unexpectedly@."; 
     exit 1

src/session/session.ml

@@ -358,7 +358,7 @@ let save_ident fmt id =
         file lnum cnumb cnume
 
 let save_label fmt s =
-  fprintf fmt "@\n@[<v 1><label@ name=\"%s\">@,</label>@]" s.Ident.lab_string
+  fprintf fmt "@\n@[<v 1><label@ name=\"%s\"/>@]" s.Ident.lab_string
 
 let rec save_goal provers fmt g =
   assert (g.goal_shape <> "");
@@ -403,11 +403,12 @@ name=\"%s\"@ version=\"%s\"%a/>@]"
     p.C.prover_altern;
   Mprover.add p id provers, id+1
 
-let save fname session =
+let save fname config session =
   let ch = open_out fname in
   let fmt = formatter_of_out_channel ch in
   fprintf fmt "<?xml version=\"1.0\" encoding=\"UTF-8\"?>@\n";
-  fprintf fmt "<!DOCTYPE why3session SYSTEM \"why3session.dtd\">@\n";
+  fprintf fmt "<!DOCTYPE why3session SYSTEM \"%s\">@\n"
+    (Filename.concat (Whyconf.datadir (Whyconf.get_main config)) "why3session.dtd");
   fprintf fmt "@[<v 1><why3session@ name=\"%s\">" fname;
   let provers,_ = Sprover.fold (save_prover fmt) (get_used_provers session)
     (Mprover.empty,0) in
@@ -416,10 +417,10 @@ let save fname session =
   fprintf fmt "@.";
   close_out ch
 
-let save_session session =
+let save_session config session =
   let f = Filename.concat session.session_dir db_filename in
   Sysutil.backup_file f;
-  save f session
+  save f config session
 
 (*******************************)
 (*          explanations       *)

src/session/session.mli

@@ -155,7 +155,7 @@ val read_session : string -> notask session
 (** Read a session stored on the disk. It returns a session without any
     task attached to goals *)
 
-val save_session : 'key session -> unit
+val save_session : Whyconf.config -> 'key session -> unit
 (** Save a session on disk *)
 
 (** {2 Context of a session} *)

src/why3session/why3session_copy.ml

@@ -170,7 +170,7 @@ let run_one ~action env config filters pk fname =
           | Mod when to_prover <> SameProver -> remove_external_proof pr
           | _ -> ()
   ) s;
-  save_session env_session.session
+  save_session config env_session.session
 
 let read_to_prover config =
   match !opt_to_prover with

src/why3session/why3session_rm.ml

@@ -76,7 +76,7 @@ let run_one env config filters fname =
         | Interactive -> interactive pr
         | Not_valid -> not (proof_verified pr) in
       if remove then remove_external_proof pr) env_session.session;
-  save_session env_session.session
+  save_session config env_session.session
 
 
 let run () =