Commit ac0b6d6d authored by MARCHE Claude's avatar MARCHE Claude

issue #12 fixed: detached nodes are implemented

Any problems found should be reported as another specific issue
parent 7febc3ad
......@@ -789,10 +789,6 @@ end
(* Specific to auto-focus at initialization of itp_server *)
focus_on_label node;
P.notify (New_node (new_id, parent, node_type, node_name, node_detached));
(*
if node_type = NFile then
read_and_send node_name;
*)
get_node_proved new_id node;
new_id
......
......@@ -1328,8 +1328,8 @@ and save_detached_trans old_s s parent_id old_id =
let save_detached_theory parent_name old_s detached_theory s =
let goalsID =
save_detached_goals old_s detached_theory.theory_goals s (Theory detached_theory) in
(* List.map (fun _ -> gen_proofNodeID s) detached_theory.theory_goals in *)
save_detached_goals old_s detached_theory.theory_goals s (Theory detached_theory)
in
{ theory_name = detached_theory.theory_name;
theory_checksum = detached_theory.theory_checksum;
theory_is_detached = true;
......
......@@ -240,7 +240,7 @@ val remove_subtree: notification:notifier -> removed:notifier ->
whose proved state changes.
raises [RemoveError] when removal is forbidden, e.g. when called on
a theory, or a goal that is not detached
a file, a theory or a goal that is not detached
*)
(** {2 proved status} *)
......
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