Commit fa011cd3 authored by MARCHE Claude's avatar MARCHE Claude

Properly mark a file node as detached in case of parsing/typing error

parent 8a999dee
......@@ -244,11 +244,11 @@ let reload_files (c : controller) ~use_shapes =
*)
let add_file c ?format fname =
let theories,errors =
try Some (Session_itp.read_file c.controller_env ?format fname), None
with e -> None, Some e
let file_is_detached,theories,errors =
try false,(Session_itp.read_file c.controller_env ?format fname), None
with e -> true,[], Some e
in
let (_ : file) = add_file_section c.controller_session fname theories format in
let (_ : file) = add_file_section c.controller_session fname ~file_is_detached theories format in
errors
......
......@@ -1539,8 +1539,8 @@ let make_theory_section ?merge ~detached (s:session) parent_name (th:Theory.theo
theory
(* add a why file to a session *)
let add_file_section (s:session) (fn:string)
(theories:Theory.theory list option) format : file =
let add_file_section (s:session) (fn:string) ~file_is_detached
(theories:Theory.theory list) format : file =
let fn = Sysutil.relativize_filename s.session_dir fn in
Debug.dprintf debug "[Session_itp.add_file_section] fn = %s@." fn;
if Hstr.mem s.session_files fn then
......@@ -1550,33 +1550,23 @@ let add_file_section (s:session) (fn:string)
exit 2
end
else
match theories with
| None ->
let f = { file_name = fn;
file_format = format;
file_is_detached = true;
file_theories = [] }
in
Hstr.add s.session_files fn f;
f
| Some ths ->
let f = { file_name = fn;
file_format = format;
file_is_detached = false;
file_theories = [] }
in
Hstr.add s.session_files fn f;
let theories = List.map (make_theory_section ~detached:false s fn) ths in
f.file_theories <- theories;
f
let f = { file_name = fn;
file_format = format;
file_is_detached = file_is_detached;
file_theories = [] }
in
Hstr.add s.session_files fn f;
let theories = List.map (make_theory_section ~detached:false s fn) theories in
f.file_theories <- theories;
f
(* add a why file to a session and try to merge its theories with the
provided ones with matching names *)
let merge_file_section ~use_shapes ~old_ses ~old_theories ~env
let merge_file_section ~use_shapes ~old_ses ~old_theories ~file_is_detached ~env
(s:session) (fn:string) (theories:Theory.theory list) format
: unit =
Debug.dprintf debug_merge "[Session_itp.merge_file_section] fn = %s@." fn;
let f = add_file_section s fn (Some []) format in
let f = add_file_section s fn ~file_is_detached [] format in
let fn = f.file_name in
let theories,detached =
let old_th_table = Hstr.create 7 in
......@@ -1638,12 +1628,12 @@ let merge_file ~use_shapes env (ses : session) (old_ses : session) file =
try
let new_theories = read_file env file_name ?format in
merge_file_section
ses ~use_shapes ~old_ses ~old_theories
ses ~use_shapes ~old_ses ~old_theories ~file_is_detached:false
~env file_name new_theories format;
None
with e -> (* TODO: capture only parsing and typing errors *)
merge_file_section
ses ~use_shapes ~old_ses ~old_theories
ses ~use_shapes ~old_ses ~old_theories ~file_is_detached:true
~env file_name [] format;
Some e
......
......@@ -155,7 +155,7 @@ val empty_session : ?from:session -> string -> session
argument *)
val add_file_section :
session -> string -> Theory.theory list option ->
session -> string -> file_is_detached:bool -> Theory.theory list->
Env.fformat option -> file
(** [add_file_section s fn ths] adds a new
'file' section in session [s], named [fn], containing fresh theory
......
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