new handling for lexical structures.

Sentence extraction and proof folding is now done with tags. The lexer
has been modified to use a callback to "stamp" the lexical constructs
that must be distinguished.

new funcs in ide/coqide.ml :

  apply_tag : GText.buffer -> GText.iter -> (int -> int) ->
                int -> int -> CoqLex.token -> unit

  remove_tags : GText.buffer -> GText.iter -> GText.iter -> unit

  tag_slice : GText.buffer -> GText.iter -> GText.iter ->
                (GText.buffer -> GText.iter -> GText.iter) -> unit

  get_sentence_bounds : GText.iter -> GText.iter * GText.iter

  end_tag_present : GText.iter -> bool

  tag_on_insert : GText.buffer -> unit

  force_retag : GText.buffer -> unit

  toggle_proof_visibility : GText.buffer -> GText.iter -> unit

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

5 files changed, 175 insertions, 162 deletions

diff --git a/ide/syntaxTokens.mll b/ide/coqLex.mll
index 1939d801d..03ce950fd 100644
--- a/ide/syntaxTokens.mll
+++ b/ide/coqLex.mll
@@ -11,9 +11,13 @@
 {
   open Lexing
 
-  type markup =
-    | Keyword of (int*int)
-    | Declaration of (int*int)
+  type token =
+    | Comment
+    | Keyword
+    | Declaration
+    | ProofDeclaration
+    | Qed
+    | String
 
   (* Without this table, the automaton would be too big and
      ocamllex would fail *)
@@ -22,7 +26,7 @@
     List.iter (fun s -> Hashtbl.add h s ())
       [  "Add" ; "Check"; "Eval"; "Extraction" ;
 	 "Load" ; "Undo"; "Goal";
-	 "Proof" ; "Print"; "Qed" ; "Defined" ; "Save" ;
+	 "Proof" ; "Print";"Save" ;
 	 "End" ; "Section"; "Chapter"; "Transparent"; "Opaque"; "Comments"
       ];
     Hashtbl.mem h
@@ -40,10 +44,7 @@
   let is_one_word_declaration =
     let h = Hashtbl.create 97 in
       List.iter (fun s -> Hashtbl.add h s ())
-	[ (* Theorems *)
-          "Theorem" ; "Lemma" ; "Fact" ; "Remark" ; "Corollary" ;
-	  "Proposition" ; "Property" ;
-          (* Definitions *)
+	[ (* Definitions *)
 	  "Definition" ; "Let" ; "Example" ; "SubClass" ;
           "Fixpoint" ; "CoFixpoint" ; "Scheme" ; "Function" ;
           (* Assumptions *)
@@ -56,17 +57,33 @@
 	];
       Hashtbl.mem h
 
-  let starting = ref true
+  let is_proof_declaration =
+    let h = Hashtbl.create 97 in
+    List.iter (fun s -> Hashtbl.add h s ())
+      [ "Theorem" ; "Lemma" ; " Fact" ; "Remark" ; "Corollary" ;
+        "Proposition" ; "Property" ];
+    Hashtbl.mem h
+
+  let is_proof_end =
+    let h = Hashtbl.create 97 in
+    List.iter (fun s -> Hashtbl.add h s ())
+      [ "Qed" ; "Defined" ; "Admitted" ];
+    Hashtbl.mem h
+
+  let start = ref true
 }
 
 let space =
   [' ' '\010' '\013' '\009' '\012']
+
 let firstchar =
   ['$' 'A'-'Z' 'a'-'z' '_' '\192'-'\214' '\216'-'\246' '\248'-'\255']
 let identchar =
   ['$' 'A'-'Z' 'a'-'z' '_' '\192'-'\214' '\216'-'\246' '\248'-'\255' '\'' '0'-'9']
 let ident = firstchar identchar*
 
+let sentence_sep = '.' [ ' ' '\n' '\t' ]
+
 let multiword_declaration =
   "Module" (space+ "Type")?
 | "Program" space+ ident
@@ -106,53 +123,72 @@ let multiword_command =
 
 rule coq_string = parse
   | "\"\"" { coq_string lexbuf }
-  | "\"" { }
+  | "\"" { Lexing.lexeme_end lexbuf }
+  | eof { Lexing.lexeme_end lexbuf }
   | _ { coq_string lexbuf }
-  | eof { }
 
 and comment = parse
-  | "(*" { comment lexbuf; comment lexbuf }
-  | "*)" { }
-  | "\"" { coq_string lexbuf; comment lexbuf }
+  | "(*" { ignore (comment lexbuf); comment lexbuf }
+  | "\"" { ignore (coq_string lexbuf); comment lexbuf }
+  | "*)" { Lexing.lexeme_end lexbuf }
+  | eof { Lexing.lexeme_end lexbuf }
   | _ { comment lexbuf }
-  | eof { }
 
-and sentence tag_cb = parse
-  | "(*" { comment lexbuf; sentence tag_cb lexbuf }
-  | "\"" { coq_string lexbuf; start := false; sentence tag_cb lexbuf }
-  | space+ { sentence tag_cb lexbuf }
+and sentence stamp = parse
+  | space+ { sentence stamp lexbuf }
+  | "(*" {
+      let comm_start = Lexing.lexeme_start lexbuf in
+      let comm_end = comment lexbuf in
+      stamp comm_start comm_end Comment;
+      sentence stamp lexbuf
+    }
+  | "\"" {
+      let str_start = Lexing.lexeme_start lexbuf in
+      let str_end = coq_string lexbuf in
+      stamp str_start str_end String;
+      start := false;
+      sentence stamp lexbuf
+    }
   | multiword_declaration {
       if !start then begin
         start := false;
-        tag_cb Declaration (lexeme_start lexbuf) (lexeme_end lexbuf)
+        stamp (Lexing.lexeme_start lexbuf) (Lexing.lexeme_end lexbuf) Declaration
       end;
-      inside_sentence lexbuf }
+      sentence stamp lexbuf
+    }
   | multiword_command {
       if !start then begin
         start := false;
-        tag_cb Keyword (lexeme_start lexbuf) (lexeme_end lexbuf)
+        stamp (Lexing.lexeme_start lexbuf) (Lexing.lexeme_end lexbuf) Keyword
       end;
-      sentence tag_cb lexbuf }
+      sentence stamp lexbuf }
   | ident as id {
       if !start then begin
         start := false;
         if id <> "Time" then begin
-            if is_one_word_command id then
-              tag_cb Keyword (lexeme_start lexbuf) (lexeme_end lexbuf)
+            if is_proof_end id then
+              stamp (Lexing.lexeme_start lexbuf) (Lexing.lexeme_end lexbuf) Qed
+            else if is_one_word_command id then
+              stamp (Lexing.lexeme_start lexbuf) (Lexing.lexeme_end lexbuf) Keyword
             else if is_one_word_declaration id then
-              tag_cb Declaration (lexeme_start lexbuf) (lexeme_end lexbuf)
+              stamp (Lexing.lexeme_start lexbuf) (Lexing.lexeme_end lexbuf) Declaration
+            else if is_proof_declaration id then
+              stamp (Lexing.lexeme_start lexbuf) (Lexing.lexeme_end lexbuf) ProofDeclaration
         end
       end else begin
         if is_constr_kw id then
-	  tag_cb Keyword (lexeme_start lexbuf) (lexeme_end lexbuf);
+	  stamp (Lexing.lexeme_start lexbuf) (Lexing.lexeme_end lexbuf) Keyword
       end;
-      sentence tag_cb lexbuf }
-  | _    { sentence tag_cb lexbuf}
-  | eof { }
+      sentence stamp lexbuf }
+  | ".."
+  | _    { sentence stamp lexbuf}
+  | sentence_sep { }
+  | eof { raise Not_found }
 
 {
-  let parse tag_cb slice =
-    let lb = from_string slice in
+  let find_end_offset stamp slice =
+    let lb = Lexing.from_string slice in
     start := true;
-    sentence tag_cb lb
+    sentence stamp lb;
+    Lexing.lexeme_end lb
 }
diff --git a/ide/coqide.ml b/ide/coqide.ml
index fb7b92d71..f74d63051 100644
--- a/ide/coqide.ml
+++ b/ide/coqide.ml
@@ -96,10 +96,6 @@ object('self)
   method undo_last_step : unit
   method help_for_keyword : unit -> unit
   method complete_at_offset : int -> bool
-
-  method toggle_proof_visibility : GText.iter -> unit
-  method hide_proof : GText.iter -> GText.iter -> GText.iter -> unit
-  method unhide_proof : GText.iter -> GText.iter -> GText.iter -> unit
 end
 
 
@@ -522,6 +518,98 @@ let warning msg =
 	     img#coerce)
     msg
 
+let apply_tag (buffer:GText.buffer) orig off_conv from upto sort =
+  let conv_and_apply start stop tag =
+    let start = orig#forward_chars (off_conv from) in
+    let stop = orig#forward_chars (off_conv upto) in
+    buffer#apply_tag ~start ~stop tag
+  in match sort with
+    | CoqLex.Comment ->
+        conv_and_apply from upto Tags.Script.comment
+    | CoqLex.Keyword ->
+        conv_and_apply from upto Tags.Script.kwd
+    | CoqLex.Declaration ->
+        conv_and_apply from upto Tags.Script.decl
+    | CoqLex.ProofDeclaration ->
+        conv_and_apply from upto Tags.Script.proof_decl
+    | CoqLex.Qed ->
+        conv_and_apply from upto Tags.Script.qed
+    | CoqLex.String -> ()
+
+let remove_tags (buffer:GText.buffer) from upto =
+  List.iter (buffer#remove_tag ~start:from ~stop:upto)
+    [ Tags.Script.comment; Tags.Script.kwd; Tags.Script.decl;
+      Tags.Script.proof_decl; Tags.Script.qed; Tags.Script.sentence_end ]
+
+let tag_slice (buffer:GText.buffer) from upto on_fail =
+  remove_tags buffer from upto;
+  buffer#remove_tag ~start:from ~stop:upto Tags.Script.sentence_end;
+  let slice = buffer#get_text ~start:from ~stop:upto () in
+  let rec tag_substring str =
+    let off_conv = byte_offset_to_char_offset str in
+    let slice_len = String.length str in
+    let tag_cnt = CoqLex.find_end_offset (apply_tag buffer from off_conv) str in
+
+    let stop = from#forward_chars (off_conv tag_cnt) in
+    let start = stop#backward_char in
+    buffer#apply_tag ~start ~stop Tags.Script.sentence_end;
+
+    if tag_cnt <> slice_len then begin
+      ignore (from#nocopy#forward_chars (off_conv tag_cnt));
+      tag_substring (String.sub str tag_cnt (slice_len - tag_cnt))
+    end
+  in
+  try tag_substring slice with Not_found -> on_fail buffer from upto
+
+let get_sentence_bounds (iter:GText.iter) =
+  let start = iter#backward_to_tag_toggle (Some Tags.Script.sentence_end) in
+  (if start#has_tag Tags.Script.sentence_end then ignore (
+    start#nocopy#forward_to_tag_toggle (Some Tags.Script.sentence_end)));
+  let stop = start#forward_to_tag_toggle (Some Tags.Script.sentence_end) in
+  (if stop#has_tag Tags.Script.sentence_end then ignore (
+    stop#nocopy#forward_to_tag_toggle (Some Tags.Script.sentence_end)));
+  start,stop
+
+let end_tag_present end_iter =
+  end_iter#backward_char#has_tag Tags.Script.sentence_end
+
+let tag_on_insert =
+  let skip_last = ref (ref true) in (* ref to the mutable flag created on last call *)
+  fun buffer ->
+    let start,stop = get_sentence_bounds (buffer#get_iter_at_mark `INSERT) in
+    let skip_curr = ref true in (* shall the callback be skipped ? by default yes*)
+    let on_tag_fail buffer start _ =
+      skip_curr := false; (* tagging failed, we go to rescue mode *)
+      ignore (Glib.Timeout.add ~ms:1500
+                ~callback:(fun () -> if not !skip_curr then begin
+                             tag_slice buffer start buffer#end_iter (fun _ _ _ -> ());
+                           end; false))
+    in
+    (!skip_last) := true; (* skip the previously created callback *)
+    skip_last := skip_curr;
+    tag_slice buffer start stop on_tag_fail
+
+let force_retag buffer =
+  tag_slice buffer buffer#start_iter buffer#end_iter (fun _ _ _ -> ())
+
+let toggle_proof_visibility (buffer:GText.buffer) (cursor:GText.iter) =
+  (* move back twice if not into proof_decl,
+   * once if into proof_decl and back_char into_proof_decl,
+   * don't move if into proof_decl and back_char not into proof_decl *)
+  if not (cursor#has_tag Tags.Script.proof_decl) then
+    ignore (cursor#nocopy#backward_to_tag_toggle (Some Tags.Script.proof_decl));
+  if cursor#backward_char#has_tag Tags.Script.proof_decl then
+    ignore (cursor#nocopy#backward_to_tag_toggle (Some Tags.Script.proof_decl));
+  let decl_start = cursor in
+  let prf_end = decl_start#forward_to_tag_toggle (Some Tags.Script.qed) in
+  let _,decl_end = get_sentence_bounds decl_start in
+  let _,prf_end = get_sentence_bounds prf_end in
+  if decl_start#has_tag Tags.Script.folded then (
+    buffer#remove_tag ~start:decl_start ~stop:decl_end Tags.Script.folded;
+    buffer#remove_tag ~start:decl_end ~stop:prf_end Tags.Script.hidden)
+  else (
+    buffer#apply_tag ~start:decl_start ~stop:decl_end Tags.Script.folded;
+    buffer#apply_tag ~start:decl_end ~stop:prf_end Tags.Script.hidden)
 
 class analyzed_view (_script:Undo.undoable_view) (_pv:GText.view) (_mv:GText.view) _cs =
 object(self)
@@ -590,7 +678,7 @@ object(self)
                   input_buffer#set_modified false;
                   pop_info ();
                   flash_info "Buffer reverted";
-                  Highlight.highlight_all input_buffer;
+                  force_retag input_buffer;
             with _  ->
               pop_info ();
               flash_info "Warning: could not revert buffer";
@@ -979,11 +1067,10 @@ object(self)
         None
 
   method find_phrase_starting_at (start:GText.iter) =
-    try
-      let end_iter = find_next_sentence start in
+    let _,end_iter = get_sentence_bounds start in
+    if end_tag_present end_iter then
         Some (start,end_iter)
-    with
-      | Not_found -> None
+    else None
 
   method complete_at_offset (offset:int) =
     prerr_endline ("Completion at offset : " ^ string_of_int offset);
@@ -1413,42 +1500,6 @@ object(self)
 
     browse_keyword (self#insert_message) (get_current_word ())
 
-
-
-  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 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*)
-      try
-        let rec find_stmt_start from =
-          let cand_start = find_nearest_backward from start_keywords in
-          let cand_end = find_word_end cand_start in
-          let cand_word = input_buffer#get_text ~start:cand_start ~stop:cand_end () in
-            if List.mem cand_word start_keywords then cand_start else find_stmt_start cand_start
-        in
-        let stmt_start = find_stmt_start cursor in
-        let stmt_end = find_next_sentence stmt_start in
-        let proof_end =
-          find_next_sentence (find_nearest_forward stmt_end ["Qed";"Defined";"Admitted"])
-        in
-          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 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 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
               ~callback:(fun it s -> ignore
@@ -1508,7 +1559,7 @@ object(self)
                                Tags.Script.error
                                ~start:self#get_start_of_input
                                ~stop;
-                             Highlight.highlight_around_current_line
+                             tag_on_insert
                                input_buffer
               )
     );
@@ -1586,23 +1637,6 @@ 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 _ =
-    List.map (fun (n,p) -> script#buffer#create_tag ~name:n p)
-      ["kwd",[`FOREGROUND "blue"];
-       "decl",[`FOREGROUND "orange red"];
-       "comment",[`FOREGROUND "brown"];
-       "reserved",[`FOREGROUND "dark red"];
-       "error",[`UNDERLINE `DOUBLE ; `FOREGROUND "red"];
-       "to_process",[`BACKGROUND "light blue" ;`EDITABLE false];
-       "processed",[`BACKGROUND "light green" ;`EDITABLE false];
-       "unjustified",[`UNDERLINE `SINGLE; `FOREGROUND "red";
-                      `BACKGROUND "gold";`EDITABLE false];
-       "found",[`BACKGROUND "blue"; `FOREGROUND "white"];
-       "hidden",[`INVISIBLE true; `EDITABLE false];
-       "locked",[`EDITABLE false; `BACKGROUND "light grey"]
-      ] in
-  let _ =
-    message#buffer#create_tag ~name:"error" [`FOREGROUND "red"] in*)
   let _ =
     proof#buffer#create_mark ~name:"end_of_conclusion" proof#buffer#start_iter in
   let _ =
@@ -1876,7 +1910,6 @@ let main files =
 		      prerr_endline ("Loading: switch to view "^ string_of_int index);
 		      session_notebook#goto_page index;
 		      prerr_endline "Loading: highlight";
-		      Highlight.highlight_all input_buffer;
 		      input_buffer#set_modified false;
 		      prerr_endline "Loading: clear undo";
 		      session.script#clear_undo;
@@ -2074,7 +2107,7 @@ let main files =
 		  let rehighlight_m = file_factory#add_item "Reh_ighlight" ~key:GdkKeysyms._L in
 		    ignore (rehighlight_m#connect#activate
 			      (fun () ->
-				 Highlight.highlight_all
+				 force_retag
 				   session_notebook#current_term.script#buffer;
 				 session_notebook#current_term.analyzed_view#recenter_insert));
 
@@ -2548,8 +2581,9 @@ let main files =
                                     ~tooltip:"Hide proof"
                                     ~key:GdkKeysyms._h
                                     ~callback:(fun x ->
-                                                 let cav = session_notebook#current_term.analyzed_view in
-                                                   cav#toggle_proof_visibility cav#get_insert)
+                                                 let sess = session_notebook#current_term in
+                                                 toggle_proof_visibility sess.script#buffer
+                                                   sess.analyzed_view#get_insert)
                                     `MISSING_IMAGE;
 
 				  (* Tactics Menu *)
diff --git a/ide/ide.mllib b/ide/ide.mllib
index 73c1d0735..a235039b9 100644
--- a/ide/ide.mllib
+++ b/ide/ide.mllib
@@ -13,9 +13,9 @@ Config_lexer
 Utf8_convert
 Preferences
 Ideutils
+CoqLex
 Gtk_parsing
 Undo
-Highlight
 Coq
 Coq_commands
 Coq_tactics
diff --git a/ide/syntaxBlocks.mll b/ide/syntaxBlocks.mll
deleted file mode 100644
index 415ef6359..000000000
--- a/ide/syntaxBlocks.mll
+++ /dev/null
@@ -1,60 +0,0 @@
-(************************************************************************)
-(*  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$ *)
-
-{
-type markup =
-  | Comment of (int*int)
-  | String of (int*int)
-  | SentenceEnd of int
-
-}
-
-let ws = [' ' '\010' '\013' '\009' '\012']
-
-let sentence_sep = '.' [ ' ' '\n' '\t']
-
-rule coq_string = parse
-  | "\"\"" { coq_string lexbuf }
-  | "\"" { Lexing.lexeme_end lexbuf }
-  | _ { coq_string lexbuf }
-  | eof { Lexing.lexeme_end lexbuf }
-
-and comment = parse
-  | "(*" { ignore (comment lexbuf); comment lexbuf }
-  | "*)" { Lexing.lexeme_end lexbuf }
-  | "\"" { ignore (coq_string lexbuf); comment lexbuf }
-  | _ { comment lexbuf }
-  | eof { Lexing.lexeme_end lexbuf }
-
-and sentence tag_cb = parse
-  | ws+ { sentence tag_cb lexbuf }
-  | _ { sentence tag_cb lexbuf }
-  | ".." { sentence tag_cb lexbuf }
-  | "(*" {
-      let comm_start = Lexing.lexeme_start lexbuf in
-      let comm_end = comment lexbuf in
-      tag_cb (Comment (comm_start,comm_end));
-      sentence tag_cb lexbuf }
-  | "\"" {
-      let str_start = Lexing.lexeme_start lexbuf in
-      let str_end = coq_string lexbuf in
-      tag_cb (String (str_start,str_end));
-      sentence tag_cb lexbuf }
-  | eof { raise Not_found } 
-  | sentence_sep {
-        tag_cb (SentenceEnd (Lexing.lexeme_end lexbuf))
-    }
-
-{
-  let parse tag_cb slice =
-    let lb = Lexing.from_string slice in
-    sentence tag_cb lb;
-    Lexing.lexeme_end lb
-}
diff --git a/ide/tags.ml b/ide/tags.ml
index 826fcd962..beb24071f 100644
--- a/ide/tags.ml
+++ b/ide/tags.ml
@@ -20,7 +20,9 @@ module Script =
 struct
   let table = GText.tag_table ()
   let kwd = make_tag table ~name:"kwd" [`FOREGROUND "blue"]
+  let qed = make_tag table ~name:"qed" [`FOREGROUND "blue"]
   let decl = make_tag table ~name:"decl" [`FOREGROUND "orange red"]
+  let proof_decl = make_tag table ~name:"proof_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"]
@@ -29,8 +31,9 @@ struct
   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"]
+  let folded = make_tag table ~name:"locked" [`EDITABLE false; `BACKGROUND "light grey"]
   let paren = make_tag table ~name:"paren" [`BACKGROUND "purple"]
+  let sentence_end = make_tag table ~name:"sentence_end" []
 end
 module Proof =
 struct