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, 10 insertions, 0 deletions

diff --git a/ide/tags.ml b/ide/tags.ml
index a91905dcd..de3287720 100644
--- a/ide/tags.ml
+++ b/ide/tags.ml
@@ -28,9 +28,19 @@ struct
   let found = make_tag table ~name:"found" [`BACKGROUND "blue"; `FOREGROUND "white"]
   let sentence = make_tag table ~name:"sentence" []
   let tooltip = make_tag table ~name:"tooltip" [] (* debug:`BACKGROUND "blue" *)
+
   let all =
      [comment_sentence; error; error_bg; to_process; processed; unjustified;
      found; sentence; tooltip]
+
+  let edit_zone =
+    let t = make_tag table ~name:"edit_zone" [`UNDERLINE `SINGLE] in
+    t#set_priority (List.length all);
+    t
+  let all = edit_zone :: all
+  
+  let read_only = make_tag table ~name:"read_only" [`EDITABLE false ]
+
 end
 module Proof =
 struct