diff options
| author |  Enrico Tassi <Enrico.Tassi@inria.fr> | 2015-04-02 15:47:52 +0200 |
|---|---|---|
| committer | Enrico Tassi <Enrico.Tassi@inria.fr> | 2015-04-02 15:57:45 +0200 |
| commit | 20457cbff0b851ac9099847c91f74d48c5fe5be6 (patch) | |
| tree | 6e3277c4fa6148303f6596e320b42bb94068722b /ide/session.ml | |
| parent | fe87c2cab20335b2d5dff61054700597e515f8a1 (diff) | |
CoqIDE: simpler way of reopening/reclosing a proof (Close: 4168)
No "read-only" terminator. If no terminator is present the UI
complains. If the terminator is different, STM warns but
continues. The STM warns that the "check the document" button
will not honor the terminator change, and what to do to avoid
that.
Technically, one cannot turn (a posteriori) an axiom into a theorem
and vice versa. Could be done, but not with a small patch.
Diffstat (limited to 'ide/session.ml')
| -rw-r--r-- | ide/session.ml | 4 |
1 files changed, 0 insertions, 4 deletions
diff --git a/ide/session.ml b/ide/session.ml index e0466b7e3..12b779663 100644 --- a/ide/session.ml +++ b/ide/session.ml @@ -156,8 +156,6 @@ let set_buffer_handlers let () = update_prev it in if it#has_tag Tags.Script.to_process then cancel_signal "Altering the script being processed in not implemented" - else if it#has_tag Tags.Script.read_only then - cancel_signal "Altering read_only text not allowed" else if it#has_tag Tags.Script.processed then call_coq_or_cancel_action (coqops#go_to_mark (`MARK text_mark)) else if it#has_tag Tags.Script.error_bg then begin @@ -175,8 +173,6 @@ let set_buffer_handlers if min_iter#equal max_iter then () else if min_iter#has_tag Tags.Script.to_process then cancel_signal "Altering the script being processed in not implemented" - else if min_iter#has_tag Tags.Script.read_only then - cancel_signal "Altering read_only text not allowed" else if min_iter#has_tag Tags.Script.processed then call_coq_or_cancel_action (coqops#go_to_mark (`MARK text_mark)) else if min_iter#has_tag Tags.Script.error_bg then |