CoqIDE ported to the revides protocol

- the zone to be edited is now between the marks
  start_of_input and stop_of_input
- when -debug is given, the edit zone is underlined
- the cmd_stack is focused/unfocused according to the new protocol
- read only tag resurrected and used to block the "Qed" ending
  a focused zone

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16814 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 4 insertions, 0 deletions

diff --git a/ide/tags.mli b/ide/tags.mli
index ddd240d2a..f79ae1f11 100644
--- a/ide/tags.mli
+++ b/ide/tags.mli
@@ -18,7 +18,11 @@ sig
   val found : GText.tag
   val sentence : GText.tag
   val tooltip : GText.tag
+  val edit_zone : GText.tag (* for debugging *)
   val all : GText.tag list
+
+  (* Not part of the all list. Special tags! *)
+  val read_only : GText.tag
 end
 
 module Proof :