diff options
| author | Pierre-Marie Pédrot | 2015-02-26 17:23:58 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2015-02-26 17:23:58 +0100 |
| commit | 93db616a6cbebf37f2f4f983963a87a4f66972e7 (patch) | |
| tree | 94577e8d2128fd35c449acb017a637e81a701ed5 /ide | |
| parent | 31c8c317affc8fb0ae818336c70ba210208249cc (diff) | |
| parent | bc7d29e4c0f53d5c8e654157c4137c7e82910a7a (diff) | |
Merge branch 'v8.5'
Diffstat (limited to 'ide')
| -rw-r--r-- | ide/coqOps.ml | 6 |
1 files changed, 5 insertions, 1 deletions
diff --git a/ide/coqOps.ml b/ide/coqOps.ml index 8ba1c8ecd2..1800cb8fe8 100644 --- a/ide/coqOps.ml +++ b/ide/coqOps.ml @@ -662,10 +662,14 @@ object(self) buffer#remove_tag Tags.Script.unjustified ~start ~stop; buffer#remove_tag Tags.Script.tooltip ~start ~stop; buffer#remove_tag Tags.Script.to_process ~start ~stop; + buffer#remove_tag Tags.Script.read_only ~start ~stop; + buffer#remove_tag Tags.Script.error ~start ~stop; + buffer#remove_tag Tags.Script.error_bg ~start ~stop; buffer#move_mark ~where:start (`NAME "start_of_input") end; List.iter (fun { start } -> buffer#delete_mark start) seg; - List.iter (fun { stop } -> buffer#delete_mark stop) seg + List.iter (fun { stop } -> buffer#delete_mark stop) seg; + self#print_stack (** Wrapper around the raw undo command *) method private backtrack_to_id ?(move_insert=true) (to_id, unfocus_needed) = |
