tags refactoring

all tags are isolated in tags.ml, and all tags are accessed directly,
not through their names.

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

4 files changed, 112 insertions, 64 deletions

diff --git a/ide/coqide.ml b/ide/coqide.ml
index ed52262af..8954c154c 100644
--- a/ide/coqide.ml
+++ b/ide/coqide.ml
@@ -161,8 +161,6 @@ let notebook_page_of_session {script=script;tab_label=bname;proof_view=proof;mes
     state_paned#set_position 1;
     (Some session_tab#coerce,None,session_paned#coerce)
 
-
-
 let session_notebook =
   Typed_notebook.create notebook_page_of_session ~border_width:2 ~show_border:false ~scrollable:true ()
 
@@ -833,8 +831,7 @@ object(self)
                   match Coq.get_current_goals () with 
                       [] -> Util.anomaly "show_goals_full"
                     | ((hyps,concl)::r) as s ->
-                        let last_shown_area = 
-                          proof_buffer#create_tag [`BACKGROUND "light green"]
+                        let last_shown_area = Tags.Proof.highlight
                         in
                         let goal_nb = List.length s in
                           proof_buffer#insert (Printf.sprintf "%d subgoal%s\n" 
@@ -956,7 +953,7 @@ object(self)
                  let i = self#get_start_of_input in 
                  let starti = i#forward_chars start in
                  let stopi = i#forward_chars stop in
-                   input_buffer#apply_tag_by_name "error"
+                   input_buffer#apply_tag Tags.Script.error
                      ~start:starti
                      ~stop:stopi;
                    input_buffer#place_cursor starti) in
@@ -1030,22 +1027,22 @@ object(self)
         | Some(start,stop) ->
             prerr_endline "process_next_phrase : to_process highlight";
             if do_highlight then begin
-              input_buffer#apply_tag_by_name ~start ~stop "to_process";
+              input_buffer#apply_tag Tags.Script.to_process ~start ~stop;
               prerr_endline "process_next_phrase : to_process applied";
             end;
             prerr_endline "process_next_phrase : getting phrase";
             Some((start,stop),start#get_slice ~stop) in
     let remove_tag (start,stop) =
       if do_highlight then begin
-        input_buffer#remove_tag_by_name ~start ~stop "to_process" ;
+        input_buffer#remove_tag Tags.Script.to_process ~start ~stop;
         input_view#set_editable true;
         pop_info ();
       end in
     let mark_processed reset_info is_complete (start,stop) ast =
       let b = input_buffer in
         b#move_mark ~where:stop (`NAME "start_of_input");
-        b#apply_tag_by_name 
-          (if is_complete then "processed" else "unjustified") ~start ~stop;
+        b#apply_tag 
+          (if is_complete then Tags.Script.processed else Tags.Script.unjustified) ~start ~stop;
         if (self#get_insert#compare) stop <= 0 then 
           begin
             b#place_cursor stop;
@@ -1079,8 +1076,8 @@ object(self)
         else input_buffer#insert ~iter:stop ("\n"^insertphrase); 
         let start = self#get_start_of_input in
           input_buffer#move_mark ~where:stop (`NAME "start_of_input");
-          input_buffer#apply_tag_by_name 
-            (if is_complete then "processed" else "unjustified") ~start ~stop;
+          input_buffer#apply_tag 
+            (if is_complete then Tags.Script.processed else Tags.Script.unjustified) ~start ~stop;
              if (self#get_insert#compare) stop <= 0 then 
                input_buffer#place_cursor stop;
              let start_of_phrase_mark = `MARK (input_buffer#create_mark start) in
@@ -1126,7 +1123,7 @@ object(self)
     let start = self#get_start_of_input#copy in
     let start' = `OFFSET start#offset in
       sync (fun _ ->
-              input_buffer#apply_tag_by_name ~start ~stop "to_process";
+              input_buffer#apply_tag Tags.Script.to_process ~start ~stop;
               input_view#set_editable false) ();
       push_info "Coq is computing";
       let get_current () =
@@ -1149,7 +1146,7 @@ object(self)
                 (* Start and stop might be invalid if an eol was added at eof *)
                 let start = input_buffer#get_iter start' in
                 let stop =  input_buffer#get_iter stop' in
-                  input_buffer#remove_tag_by_name ~start ~stop "to_process" ;
+                  input_buffer#remove_tag Tags.Script.to_process ~start ~stop;
                   input_view#set_editable true) ();
         pop_info()
 
@@ -1163,8 +1160,8 @@ object(self)
                  let start = input_buffer#get_iter_at_mark inf.start in
                  let stop = input_buffer#get_iter_at_mark inf.stop in
                    input_buffer#move_mark ~where:start (`NAME "start_of_input");
-                   input_buffer#remove_tag_by_name "processed" ~start ~stop;
-                   input_buffer#remove_tag_by_name "unjustified" ~start ~stop;
+                   input_buffer#remove_tag Tags.Script.processed ~start ~stop;
+                   input_buffer#remove_tag Tags.Script.unjustified ~start ~stop;
                    input_buffer#delete_mark inf.start;
                    input_buffer#delete_mark inf.stop;
               ) 
@@ -1202,14 +1199,14 @@ object(self)
                       if Stack.is_empty cmd_stack then input_buffer#start_iter 
                       else input_buffer#get_iter_at_mark (Stack.top cmd_stack).stop in
                       prerr_endline "Removing (long) processed tag...";
-                      input_buffer#remove_tag_by_name 
+                      input_buffer#remove_tag 
+                        Tags.Script.processed
                         ~start 
-                        ~stop:self#get_start_of_input
-                        "processed";
-                      input_buffer#remove_tag_by_name 
+                        ~stop:self#get_start_of_input;
+                      input_buffer#remove_tag 
+                        Tags.Script.unjustified
                         ~start 
-                        ~stop:self#get_start_of_input
-                        "unjustified";
+                        ~stop:self#get_start_of_input;
                       prerr_endline "Moving (long) start_of_input...";
                       input_buffer#move_mark ~where:start (`NAME "start_of_input");
                       self#show_goals;
@@ -1243,14 +1240,14 @@ object(self)
           let start = input_buffer#get_iter_at_mark last_command.start in
           let update_input () =
             prerr_endline "Removing processed tag...";
-            input_buffer#remove_tag_by_name 
+            input_buffer#remove_tag
+              Tags.Script.processed
               ~start
-              ~stop:(input_buffer#get_iter_at_mark last_command.stop) 
-              "processed";
-            input_buffer#remove_tag_by_name 
+              ~stop:(input_buffer#get_iter_at_mark last_command.stop);
+            input_buffer#remove_tag
+              Tags.Script.unjustified
               ~start
-              ~stop:(input_buffer#get_iter_at_mark last_command.stop) 
-              "unjustified";
+              ~stop:(input_buffer#get_iter_at_mark last_command.stop);
             prerr_endline "Moving start_of_input";
             input_buffer#move_mark
               ~where:start
@@ -1420,12 +1417,12 @@ object(self)
 
   method toggle_proof_visibility (cursor:GText.iter) =
     let start_keywords = ["Theorem";"Lemma";"Corollary";"Remark";"Proposition";"Fact";"Property"] in
-    let has_tag_by_name (it:GText.iter) name =
+  (*  let has_tag_by_name (it:GText.iter) name =
       let tt = new GText.tag_table (input_buffer#tag_table) in
         match tt#lookup name with
           | Some named_tag -> it#has_tag (new GText.tag named_tag)
           | _ -> false
-    in
+    in*)
       try
         let rec find_stmt_start from =
           let cand_start = find_nearest_backward from start_keywords in
@@ -1438,19 +1435,19 @@ object(self)
         let proof_end =
           find_next_sentence (find_nearest_forward stmt_end ["Qed";"Defined";"Admitted"])
         in
-          if has_tag_by_name stmt_start "locked"
+          if stmt_start#has_tag Tags.Script.locked
           then self#unhide_proof stmt_start stmt_end proof_end
           else self#hide_proof stmt_start stmt_end proof_end
       with
           Not_found -> ()
 
   method hide_proof (stmt_start:GText.iter) (stmt_end:GText.iter) (proof_end:GText.iter) =
-    input_buffer#apply_tag_by_name "hidden" ~start:stmt_end ~stop:proof_end;
-    input_buffer#apply_tag_by_name "locked" ~start:stmt_start ~stop:stmt_end
+    input_buffer#apply_tag Tags.Script.hidden ~start:stmt_end ~stop:proof_end;
+    input_buffer#apply_tag Tags.Script.locked ~start:stmt_start ~stop:stmt_end
 
   method unhide_proof (stmt_start:GText.iter) (stmt_end:GText.iter) (proof_end:GText.iter) =
-    input_buffer#remove_tag_by_name "hidden" ~start:stmt_end ~stop:proof_end;
-    input_buffer#remove_tag_by_name "locked" ~start:stmt_start ~stop:stmt_end
+    input_buffer#remove_tag Tags.Script.hidden ~start:stmt_end ~stop:proof_end;
+    input_buffer#remove_tag Tags.Script.locked ~start:stmt_start ~stop:stmt_end
 
   initializer 
     ignore (message_buffer#connect#insert_text
@@ -1470,14 +1467,14 @@ object(self)
                            if (start#compare self#get_start_of_input)>=0
                            then 
                              begin
-                               input_buffer#remove_tag_by_name 
+                               input_buffer#remove_tag 
+                                 Tags.Script.processed
                                  ~start
-                                 ~stop
-                                 "processed";
-                               input_buffer#remove_tag_by_name 
+                                 ~stop;
+                               input_buffer#remove_tag 
+                                 Tags.Script.unjustified
                                  ~start
                                  ~stop
-                                 "unjustified"
                              end
               )
     );
@@ -1507,10 +1504,10 @@ object(self)
                                ~x:(Gdk.Rectangle.x r + Gdk.Rectangle.width r)
                                ~y:(Gdk.Rectangle.y r + Gdk.Rectangle.height r)
                            in
-                             input_buffer#remove_tag_by_name 
+                             input_buffer#remove_tag
+                               Tags.Script.error
                                ~start:self#get_start_of_input
-                               ~stop
-                               "error";
+                               ~stop;
                              Highlight.highlight_around_current_line
                                input_buffer 
               )
@@ -1558,8 +1555,6 @@ object(self)
 
 end
 
-
-
 let last_make = ref "";;
 let last_make_index = ref 0;;
 let search_compile_error_regexp =
@@ -1586,11 +1581,17 @@ let search_next_error () =
 
 let create_session () =
   let script =
-    Undo.undoable_view ~buffer:(GText.buffer ()) ~wrap_mode:`NONE () in
+    Undo.undoable_view
+      ~buffer:(GText.buffer ~tag_table:Tags.Script.table ())
+      ~wrap_mode:`NONE () in
   let proof =
-    GText.view ~editable:false ~wrap_mode:`CHAR () in
+    GText.view
+      ~buffer:(GText.buffer ~tag_table:Tags.Proof.table ())
+      ~editable:false ~wrap_mode:`CHAR () in
   let message =
-    GText.view ~editable:false ~wrap_mode:`WORD () in
+    GText.view
+      ~buffer:(GText.buffer ~tag_table:Tags.Message.table ())
+      ~editable:false ~wrap_mode:`WORD () in
   let basename =
     GMisc.label ~text:"*scratch*" () in
   let stack =
@@ -1599,7 +1600,7 @@ let create_session () =
     new analyzed_view script proof message stack in
   let _ =
     script#buffer#create_mark ~name:"start_of_input" script#buffer#start_iter in
-  let _ =
+ (* let _ =
     List.map (fun (n,p) -> script#buffer#create_tag ~name:n p)
       ["kwd",[`FOREGROUND "blue"];
        "decl",[`FOREGROUND "orange red"];
@@ -1615,7 +1616,7 @@ let create_session () =
        "locked",[`EDITABLE false; `BACKGROUND "light grey"]
       ] in
   let _ =
-    message#buffer#create_tag ~name:"error" [`FOREGROUND "red"] in
+    message#buffer#create_tag ~name:"error" [`FOREGROUND "red"] in*)
   let _ =
     proof#buffer#create_mark ~name:"end_of_conclusion" proof#buffer#start_iter in
   let _ =
@@ -2265,7 +2266,7 @@ let main files =
 				  let start = b#get_iter_at_mark start
 				  and stop = b#get_iter_at_mark stop
 				  in
-				    b#remove_tag_by_name ~start ~stop "found";
+				    b#remove_tag Tags.Script.found ~start ~stop;
 				    last_found:=None;
 				    start,stop
 			  in
@@ -2292,7 +2293,7 @@ let main files =
 			  with
 			    | None -> ()
 			    | Some(start,stop) ->
-				b#apply_tag_by_name "found" ~start ~stop;
+				b#apply_tag Tags.Script.found ~start ~stop;
 				let start = `MARK (b#create_mark start)
 				and stop = `MARK (b#create_mark stop)
 				in
@@ -3000,7 +3001,7 @@ with _ := Induction for _ Sort _.\n",61,10, Some GdkKeysyms._S);
 						  *)
 						let starti = input_buffer#get_iter_at_byte ~line:(line-1) start in
 						let stopi = input_buffer#get_iter_at_byte ~line:(line-1) stop in
-						  input_buffer#apply_tag_by_name "error"
+						  input_buffer#apply_tag Tags.Script.error
    						    ~start:starti
 						    ~stop:stopi;
 						  input_buffer#place_cursor starti;
diff --git a/ide/highlight.mll b/ide/highlight.mll
index 4b36414d6..44018ff09 100644
--- a/ide/highlight.mll
+++ b/ide/highlight.mll
@@ -12,7 +12,7 @@
 
   open Lexing
 
-  type color = string
+  type color = GText.tag
 
   type highlight_order = int * int * color
 
@@ -106,17 +106,17 @@ rule next_starting_order = parse
   | "(*" { comment_start := lexeme_start lexbuf; comment lexbuf }
   | space+ { next_starting_order lexbuf }
   | multiword_declaration
-      { starting:=false; lexeme_start lexbuf, lexeme_end lexbuf, "decl" }
+      { starting:=false; lexeme_start lexbuf, lexeme_end lexbuf, Tags.Script.decl }
   | multiword_command
-      { starting:=false; lexeme_start lexbuf, lexeme_end lexbuf, "kwd" }
+      { starting:=false; lexeme_start lexbuf, lexeme_end lexbuf, Tags.Script.kwd }
   | ident as id 
       { if id = "Time" then next_starting_order lexbuf else
 	begin
 	  starting:=false; 
           if is_one_word_command id then 
-	    lexeme_start lexbuf, lexeme_end lexbuf, "kwd" 
+	    lexeme_start lexbuf, lexeme_end lexbuf, Tags.Script.kwd 
 	  else if is_one_word_declaration id then
-	    lexeme_start lexbuf, lexeme_end lexbuf, "decl"
+	    lexeme_start lexbuf, lexeme_end lexbuf, Tags.Script.decl
 	  else
 	    next_interior_order lexbuf
 	end
@@ -129,7 +129,7 @@ and next_interior_order = parse
       { comment_start := lexeme_start lexbuf; comment lexbuf }
   | ident as id 
       { if is_constr_kw id then
-	  lexeme_start lexbuf, lexeme_end lexbuf, "kwd"
+	  lexeme_start lexbuf, lexeme_end lexbuf, Tags.Script.kwd
         else
 	  next_interior_order lexbuf }
   | "." (" "|"\n"|"\t") { starting := true; next_starting_order lexbuf }
@@ -137,7 +137,7 @@ and next_interior_order = parse
   | eof  { raise End_of_file }
 
 and comment = parse
-  | "*)" { !comment_start,lexeme_end lexbuf,"comment" }
+  | "*)" { !comment_start,lexeme_end lexbuf,Tags.Script.comment }
   | "(*" { ignore (comment lexbuf); comment lexbuf }
   | "\"" { string_in_comment lexbuf }
   | _    { comment lexbuf }
@@ -160,10 +160,10 @@ and string_in_comment = parse
     else begin
       highlighting := true;
       prerr_endline "Highlighting slice now";
-      input_buffer#remove_tag_by_name ~start ~stop "error";
-      input_buffer#remove_tag_by_name ~start ~stop "kwd";
-      input_buffer#remove_tag_by_name ~start ~stop "decl";
-      input_buffer#remove_tag_by_name ~start ~stop "comment";
+      input_buffer#remove_tag ~start ~stop Tags.Script.error;
+      input_buffer#remove_tag ~start ~stop Tags.Script.kwd;
+      input_buffer#remove_tag ~start ~stop Tags.Script.decl;
+      input_buffer#remove_tag ~start ~stop Tags.Script.comment;
 
       (try begin
 	let offset = start#offset in
@@ -179,7 +179,7 @@ and string_in_comment = parse
 	    let b,e = convert_pos b,convert_pos e in
 	    let start = input_buffer#get_iter_at_char (offset + b) in
 	    let stop = input_buffer#get_iter_at_char (offset + e) in
-	    input_buffer#apply_tag_by_name ~start ~stop o 
+	    input_buffer#apply_tag ~start ~stop o 
 	  done
 	with End_of_file -> ()
       end
diff --git a/ide/ide.mllib b/ide/ide.mllib
index 152331747..73c1d0735 100644
--- a/ide/ide.mllib
+++ b/ide/ide.mllib
@@ -7,6 +7,7 @@ Configwin_ihm
 Configwin
 Editable_cells
 Config_parser
+Tags
 Typed_notebook
 Config_lexer
 Utf8_convert
diff --git a/ide/tags.ml b/ide/tags.ml
new file mode 100644
index 000000000..89adad2c1
--- /dev/null
+++ b/ide/tags.ml
@@ -0,0 +1,46 @@
+
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+(* $Id$ *)
+
+
+let make_tag (tt:GText.tag_table) ~name prop =
+  let new_tag = GText.tag ~name () in
+  new_tag#set_properties prop;
+  tt#add new_tag#as_tag;
+  new_tag
+
+module Script =
+struct
+  let table = GText.tag_table ()
+  let kwd = make_tag table ~name:"kwd" [`FOREGROUND "blue"]
+  let decl = make_tag table ~name:"decl" [`FOREGROUND "orange red"]
+  let comment = make_tag table ~name:"comment" [`FOREGROUND "brown"]
+  let reserved = make_tag table ~name:"reserved" [`FOREGROUND "dark red"]
+  let error = make_tag table ~name:"error" [`UNDERLINE `DOUBLE ; `FOREGROUND "red"]
+  let to_process = make_tag table ~name:"to_process" [`BACKGROUND "light blue" ;`EDITABLE false]
+  let processed = make_tag table ~name:"processed" [`BACKGROUND "light green" ;`EDITABLE false]
+  let unjustified = make_tag table ~name:"unjustified" [`UNDERLINE `SINGLE; `FOREGROUND "red"; `BACKGROUND "gold";`EDITABLE false]
+  let found = make_tag table ~name:"found" [`BACKGROUND "blue"; `FOREGROUND "white"]
+  let hidden = make_tag table ~name:"hidden" [`INVISIBLE true; `EDITABLE false]
+  let locked = make_tag table ~name:"locked" [`EDITABLE false; `BACKGROUND "light grey"]
+end
+module Proof =
+struct
+  let table = GText.tag_table ()
+  let highlight = make_tag table ~name:"highlight" [`BACKGROUND "light green"]
+  let hypothesis = make_tag table ~name:"hypothesis" []
+  let goal = make_tag table ~name:"goal" []
+end
+module Message = 
+struct
+  let table = GText.tag_table ()
+  let error = make_tag table ~name:"error" [`FOREGROUND "red"]
+end
+