From 31d9916852b2e0281bb5dde503b6b6e557fe29f8 Mon Sep 17 00:00:00 2001 From: Claude Marche Date: Mon, 26 Mar 2012 16:09:27 +0200 Subject: [PATCH] updated DTD of sessions --- share/why3session.dtd | 14 +++++++++++++- src/ide/gconfig.ml | 2 ++ src/ide/gconfig.mli | 5 +++++ src/ide/gmain.ml | 4 +++- src/ide/replay.ml | 10 +++++----- src/session/session.ml | 11 ++++++----- src/session/session.mli | 2 +- src/why3session/why3session_copy.ml | 2 +- src/why3session/why3session_rm.ml | 2 +- 9 files changed, 37 insertions(+), 15 deletions(-) diff --git a/share/why3session.dtd b/share/why3session.dtd index 22f058fe5..823e7209a 100644 --- a/share/why3session.dtd +++ b/share/why3session.dtd @@ -11,10 +11,14 @@ - + + + + + @@ -23,12 +27,17 @@ + + + + + @@ -40,3 +49,6 @@ + + + diff --git a/src/ide/gconfig.ml b/src/ide/gconfig.ml index 4106e05f3..0e6f6b65a 100644 --- a/src/ide/gconfig.ml +++ b/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 () diff --git a/src/ide/gconfig.mli b/src/ide/gconfig.mli index d1584384e..9dc82ac9c 100644 --- a/src/ide/gconfig.mli +++ b/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" diff --git a/src/ide/gmain.ml b/src/ide/gmain.ml index 332f9b4b1..2971d8db7 100644 --- a/src/ide/gmain.ml +++ b/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 diff --git a/src/ide/replay.ml b/src/ide/replay.ml index 114c0c536..07c980b9f 100644 --- a/src/ide/replay.ml +++ b/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 diff --git a/src/session/session.ml b/src/session/session.ml index c26e4ec2c..5a7791fbb 100644 --- a/src/session/session.ml +++ b/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@[@,@]" s.Ident.lab_string + fprintf fmt "@\n@[@]" 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 "@\n"; - fprintf fmt "@\n"; + fprintf fmt "@\n" + (Filename.concat (Whyconf.datadir (Whyconf.get_main config)) "why3session.dtd"); fprintf fmt "@[" 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 *) diff --git a/src/session/session.mli b/src/session/session.mli index 4ae424d24..f6975f693 100644 --- a/src/session/session.mli +++ b/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} *) diff --git a/src/why3session/why3session_copy.ml b/src/why3session/why3session_copy.ml index 178100a62..152871668 100644 --- a/src/why3session/why3session_copy.ml +++ b/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 diff --git a/src/why3session/why3session_rm.ml b/src/why3session/why3session_rm.ml index 33c01eecf..ae365eb34 100644 --- a/src/why3session/why3session_rm.ml +++ b/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 () = -- GitLab