aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
-rw-r--r--ide/coqOps.ml4
-rw-r--r--ide/document.ml4
2 files changed, 5 insertions, 3 deletions
diff --git a/ide/coqOps.ml b/ide/coqOps.ml
index eb09d3bbb..59c399842 100644
--- a/ide/coqOps.ml
+++ b/ide/coqOps.ml
@@ -553,7 +553,8 @@ object(self)
(* finds the state_id and if it an unfocus is needed to reach it *)
method private find_id until =
- try Doc.find_id document (fun id { start;stop } -> until (Some id) start stop)
+ try
+ Doc.find_id document (fun id { start;stop } -> until (Some id) start stop)
with Not_found -> initial_state, Doc.focused document
method private cleanup seg =
@@ -586,6 +587,7 @@ object(self)
buffer#remove_tag Tags.Script.tooltip ~start ~stop;
buffer#remove_tag Tags.Script.processed ~start ~stop;
buffer#remove_tag Tags.Script.to_process ~start ~stop;
+ buffer#remove_tag Tags.Script.unjustified ~start ~stop;
self#show_goals in
Coq.bind (Coq.lift opening) (fun () ->
let rec undo to_id unfocus_needed =
diff --git a/ide/document.ml b/ide/document.ml
index fab318f18..deb780739 100644
--- a/ide/document.ml
+++ b/ide/document.ml
@@ -123,11 +123,11 @@ let assign_tip_id d id =
let cut_at d id =
let aux (n, zone) { state_id; data } =
- if stateid_opt_equal state_id (Some id) then CSig.Stop (n, List.rev zone)
+ if stateid_opt_equal state_id (Some id) then CSig.Stop (n, zone)
else CSig.Cont (n + 1, data :: zone) in
let n, zone = CList.fold_left_until aux (0, []) d.stack in
for i = 1 to n do ignore(pop d) done;
- zone
+ List.rev zone
let find_id d f =
let top, focus, bot = to_lists d in