Commit 7023491c authored by Guillaume Melquiond's avatar Guillaume Melquiond

Do not discard prover ids when reloading the session.

parent b1cc2e11
......@@ -224,8 +224,7 @@ let print_session fmt c =
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);
c.controller_session <- empty_session ~from:old_ses (get_dir old_ses);
try
merge_files ~use_shapes c.controller_env c.controller_session old_ses
with e ->
......
......@@ -179,8 +179,6 @@ let get_files s = s.session_files
let get_file s name = Hstr.find s.session_files name
let get_dir s = s.session_dir
let get_shape_version s = s.session_shape_version
(*
let get_node (s : session) (n : int) =
let _ = Hint.find s.proofNode_table n in n
......@@ -497,10 +495,11 @@ let _print_session fmt s =
fprintf fmt "%a@." (print_s s) l;;
let empty_session ?shape_version dir =
let shape_version = match shape_version with
| Some v -> v
| None -> Termcode.current_shape_version
let empty_session ?from dir =
let prover_ids, shape_version =
match from with
| Some v -> v.session_prover_ids, v.session_shape_version
| None -> Hprover.create 7, Termcode.current_shape_version
in
{ proofAttempt_table = Hint.create 97;
next_proofAttemptID = 0;
......@@ -511,7 +510,7 @@ let empty_session ?shape_version dir =
session_dir = dir;
session_files = Hstr.create 3;
session_shape_version = shape_version;
session_prover_ids = Hprover.create 7;
session_prover_ids = prover_ids;
session_raw_tasks = Hpn.create 97;
session_tasks = Hpn.create 97;
file_state = Hstr.create 3;
......
......@@ -56,7 +56,6 @@ val get_files : session -> file Stdlib.Hstr.t
val get_file: session -> string -> file
(* Get directory containing the session *)
val get_dir : session -> string
val get_shape_version : session -> int
(** File *)
val file_name : file -> string
......@@ -146,7 +145,7 @@ val fold_all_session: session -> ('a -> any -> 'a) -> 'a -> 'a
(** {2 session operations} *)
val empty_session : ?shape_version:int -> string -> session
val empty_session : ?from:session -> string -> session
(** create an empty_session in the directory specified by the
argument *)
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment