diff --git a/src/session/controller_itp.ml b/src/session/controller_itp.ml index 14ead8d1764f747d2424a66fa639b5bdab028373..8186d5dfae0a990a74fc5617d4f4e53f3fffa656 100644 --- a/src/session/controller_itp.ml +++ b/src/session/controller_itp.ml @@ -404,7 +404,7 @@ let reload_files (c : controller) ~use_shapes = let add_file c ?format fname = let theories = read_file c.controller_env ?format fname in - add_file_section ~use_shapes:false c.controller_session fname theories format + add_file_section c.controller_session fname theories format (* Update the proof_state according to new false state and then remove the subtree *) diff --git a/src/session/session_itp.ml b/src/session/session_itp.ml index 0b39cfc12e08f8a9f62bf0fbd723571aa8135748..a6b034c5f7f4f08da5b2a243659adfffcc867609 100644 --- a/src/session/session_itp.ml +++ b/src/session/session_itp.ml @@ -1295,7 +1295,7 @@ let merge_theory ~use_shapes env old_s old_th s th : unit = (* add a theory and its goals to a session. if a previous theory is provided in merge try to merge the new theory with the previous one *) -let make_theory_section ~use_shapes ?merge (s:session) parent_name (th:Theory.theory) +let make_theory_section ?merge (s:session) parent_name (th:Theory.theory) : theory = let add_goal parent goal id = let name,_expl,task = Termcode.goal_expl_task ~root:true goal in @@ -1312,21 +1312,21 @@ let make_theory_section ~use_shapes ?merge (s:session) parent_name (th:Theory.th List.iter2 (add_goal parent) tasks goalsID; begin match merge with - | Some (old_s, old_th, env) -> + | Some (old_s, old_th, env, use_shapes) -> merge_theory ~use_shapes env old_s old_th s theory | _ -> () end; theory (* add a why file to a session *) -let add_file_section ~use_shapes (s:session) (fn:string) +let add_file_section (s:session) (fn:string) (theories:Theory.theory list) format : unit = let fn = Sysutil.relativize_filename s.session_dir fn in if Hstr.mem s.session_files fn then Debug.dprintf debug "[session] file %s already in database@." fn else begin - let theories = List.map (make_theory_section ~use_shapes s fn) theories in + let theories = List.map (make_theory_section s fn) theories in let f = { file_name = fn; file_format = format; file_theories = theories; @@ -1356,10 +1356,10 @@ let merge_file_section ~use_shapes ~old_ses ~old_theories ~env (* if we found one, we remove it from the table and merge it *) let old_th = Hstr.find old_th_table theory_name in Hstr.remove old_th_table theory_name; - make_theory_section ~use_shapes ~merge:(old_ses,old_th,env) s fn th + make_theory_section ~merge:(old_ses,old_th,env,use_shapes) s fn th with Not_found -> (* if no theory was found we make a new theory section *) - make_theory_section ~use_shapes s fn th + make_theory_section s fn th in let theories = List.map add_theory theories in (* we save the remaining, detached *) diff --git a/src/session/session_itp.mli b/src/session/session_itp.mli index 977fdd16b0d8ef3d20041114780119f37b27a33d..40a10bf30296b4cb10e79ee3c2bfbb6cc2ab7dfe 100644 --- a/src/session/session_itp.mli +++ b/src/session/session_itp.mli @@ -108,9 +108,9 @@ val empty_session : ?shape_version:int -> string -> session argument *) val add_file_section : - use_shapes:bool -> session -> string -> (Theory.theory list) -> + session -> string -> (Theory.theory list) -> Env.fformat option -> unit -(** [add_file_section ~merge:(old_s,old_ths,env) s fn ths] adds a new +(** [add_file_section 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]. *)