From 20457cbff0b851ac9099847c91f74d48c5fe5be6 Mon Sep 17 00:00:00 2001
From: Enrico Tassi
Date: Thu, 2 Apr 2015 15:47:52 +0200
Subject: 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.
---
 ide/session.ml | 4 ----
 1 file changed, 4 deletions(-)

(limited to 'ide/session.ml')

diff --git a/ide/session.ml b/ide/session.ml
index e0466b7e3a..12b7796633 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
-- 
cgit v1.2.3