Coqide coq lexer put one tag at the end of a sentence.

And that's all !
It erase the possibility of code folding...

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

5 files changed, 31 insertions, 174 deletions

diff --git a/ide/coq_lex.mll b/ide/coq_lex.mll
index c9a9a8260..fbcbbd788 100644
--- a/ide/coq_lex.mll
+++ b/ide/coq_lex.mll
@@ -7,129 +7,32 @@
 (************************************************************************)
 
 {
-  open Lexing
-
-  type token =
-    | Comment
-    | Keyword
-    | Declaration
-    | ProofDeclaration
-    | Qed
-    | String
-
-  (* Without this table, the automaton would be too big and
-     ocamllex would fail *)
-
-  let tag_of_ident =
-    let one_word_commands =
-      [ "Add" ; "Check"; "Eval"; "Extraction" ;
-	"Load" ; "Undo"; "Goal";
-	"Proof" ; "Print";"Save" ; "Restart";
-	"End" ; "Section"; "Chapter"; "Transparent"; "Opaque"; "Comments" ]
-    in
-    let one_word_declarations =
-      [ (* Definitions *)
-	"Definition" ; "Let" ; "Example" ; "SubClass" ;
-        "Fixpoint" ; "CoFixpoint" ; "Scheme" ; "Function" ;
-        (* Assumptions *)
-	"Hypothesis" ; "Variable" ; "Axiom" ; "Parameter" ; "Conjecture" ;
-	"Hypotheses" ; "Variables" ; "Axioms" ; "Parameters";
-        (* Inductive *)
-        "Inductive" ; "CoInductive" ; "Record" ; "Structure" ;
-        (* Other *)
-	"Ltac" ; "Instance"; "Include"; "Context"; "Class" ;
-	 "Arguments" ]
-    in
-    let proof_declarations =
-      [ "Theorem" ; "Lemma" ; " Fact" ; "Remark" ; "Corollary" ;
-        "Proposition" ; "Property" ]
-    in
-    let proof_ends =
-      [ "Qed" ; "Defined" ; "Admitted"; "Abort" ]
-    in
-    let constr_keywords =
-      [ "forall"; "fun"; "match"; "fix"; "cofix"; "with"; "for";
-	"end"; "as"; "let"; "in"; "if"; "then"; "else"; "return";
-	"Prop"; "Set"; "Type" ]
-    in
-    let h = Hashtbl.create 97 in (* for vernac *)
-    let h' = Hashtbl.create 97 in (* for constr *)
-    List.iter (fun s -> Hashtbl.add h s Keyword) one_word_commands;
-    List.iter (fun s -> Hashtbl.add h s Declaration) one_word_declarations;
-    List.iter (fun s -> Hashtbl.add h s ProofDeclaration) proof_declarations;
-    List.iter (fun s -> Hashtbl.add h s Qed) proof_ends;
-    List.iter (fun s -> Hashtbl.add h' s Keyword) constr_keywords;
-    (fun initial id -> Hashtbl.find (if initial then h else h') id)
-
   exception Unterminated
-
-  let here f lexbuf = f (Lexing.lexeme_start lexbuf) (Lexing.lexeme_end lexbuf)
-
 }
 
 let space =
   [' ' '\n' '\r' '\t' '\012'] (* '\012' is form-feed *)
 
-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 undotted_sep = [ '{' '}' '-' '+' '*' ]
 
 let dot_sep = '.' (space | eof)
 
-let multiword_declaration =
-  "Module" (space+ "Type")?
-| "Program" space+ ident
-| "Existing" space+ "Instance" "s"?
-| "Canonical" space+ "Structure"
-
-let locality = (space+ "Local")?
-
-let multiword_command =
-  ("Uns" | "S")" et" (space+ ident)*
-| (("Open" | "Close") locality | "Bind" | " Delimit" )
-    space+ "Scope"
-| (("Reserved" space+)? "Notation" | "Infix") locality space+
-| "Next" space+ "Obligation"
-| "Solve" space+ "Obligations"
-| "Require" space+ ("Import"|"Export")?
-| "Hint" locality space+ ident
-| "Reset" (space+ "Initial")?
-| "Tactic" space+ "Notation"
-| "Implicit" space+ "Type" "s"?
-| "Combined" space+ "Scheme"
-| "Extraction" space+ (("Language" space+ ("Ocaml"|"Haskell"|"Scheme"|"Toplevel"))|
-    ("Library"|"Inline"|"NoInline"|"Blacklist"))
-| "Recursive" space+ "Extraction" (space+ "Library")?
-| ("Print"|"Reset") space+ "Extraction" space+ ("Inline"|"Blacklist")
-| "Extract" space+ (("Inlined" space+) "Constant"| "Inductive")
-| "Typeclasses" space+ ("eauto" | "Transparent" | "Opaque")
-| ("Generalizable" space+) ("All" | "No")? "Variable" "s"?
-
-(* At least still missing: "Inline" + decl, variants of "Identity
-  Coercion", variants of Print, Add, ... *)
-
 rule coq_string = parse
-  | "\"\"" { coq_string lexbuf }
-  | "\"" { Lexing.lexeme_end lexbuf }
-  | eof { Lexing.lexeme_end lexbuf }
+  | "\\\"" { coq_string lexbuf }
+  | "\"" { () }
+  | eof { () }
   | _ { coq_string lexbuf }
 
 and comment = parse
   | "(*" { ignore (comment lexbuf); comment lexbuf }
-  | "\"" { ignore (coq_string lexbuf); comment lexbuf }
+  | "\"" { let () = coq_string lexbuf in comment lexbuf }
   | "*)" { (true, Lexing.lexeme_start lexbuf + 2) }
   | eof { (false, Lexing.lexeme_end lexbuf) }
   | _ { comment lexbuf }
 
-and sentence initial stamp = parse
+and sentence initial = parse
   | "(*" {
-      let comm_start = Lexing.lexeme_start lexbuf in
       let trully_terminated,comm_end = comment lexbuf in
-      stamp comm_start comm_end Comment;
       if not trully_terminated then raise Unterminated;
       (* A comment alone is a sentence.
 	 A comment in a sentence doesn't terminate the sentence.
@@ -137,47 +40,34 @@ and sentence initial stamp = parse
 	 as required when tagging a zone, hence the -1 to locate the
 	 ")" terminating the comment.
       *)
-      if initial then comm_end - 1 else sentence false stamp lexbuf
+      if initial then true, comm_end - 1 else sentence false lexbuf
     }
   | "\"" {
-      let str_start = Lexing.lexeme_start lexbuf in
-      let str_end = coq_string lexbuf in
-      stamp str_start str_end String;
-      sentence false stamp lexbuf
-    }
-  | multiword_declaration {
-      if initial then here stamp lexbuf Declaration;
-      sentence false stamp lexbuf
-    }
-  | multiword_command {
-      if initial then here stamp lexbuf Keyword;
-      sentence false stamp lexbuf
+      let () = coq_string lexbuf in
+      sentence false lexbuf
     }
-  | ident as id {
-      (try here stamp lexbuf (tag_of_ident initial id) with Not_found -> ());
-      sentence false stamp lexbuf }
   | ".." {
       (* We must have a particular rule for parsing "..", where no dot
 	 is a terminator, even if we have a blank afterwards
 	 (cf. for instance the syntax for recursive notation).
 	 This rule and the following one also allow to treat the "..."
 	 special case, where the third dot is a terminator. *)
-      sentence false stamp lexbuf
+      sentence false lexbuf
     }
-  | dot_sep { Lexing.lexeme_start lexbuf } (* The usual "." terminator *)
+  | dot_sep { false, Lexing.lexeme_start lexbuf } (* The usual "." terminator *)
   | undotted_sep {
       (* Separators like { or } and bullets * - + are only active
 	 at the start of a sentence *)
-      if initial then Lexing.lexeme_start lexbuf
-      else sentence false stamp lexbuf
+      if initial then false, Lexing.lexeme_start lexbuf
+      else sentence false lexbuf
     }
   | space+ {
        (* Parsing spaces is the only situation preserving initiality *)
-       sentence initial stamp lexbuf
+       sentence initial lexbuf
     }
   | _ {
       (* Any other characters *)
-      sentence false stamp lexbuf
+      sentence false lexbuf
     }
   | eof { raise Unterminated }
 
@@ -189,7 +79,7 @@ and sentence initial stamp = parse
       It will raise [Unterminated] when no end of sentence is found.
   *)
 
-  let delimit_sentence stamp slice =
-    sentence true stamp (Lexing.from_string slice)
+  let delimit_sentence slice =
+    sentence true (Lexing.from_string slice)
 
 }
diff --git a/ide/coqide.ml b/ide/coqide.ml
index 429c4c334..b94f09053 100644
--- a/ide/coqide.ml
+++ b/ide/coqide.ml
@@ -392,43 +392,23 @@ let with_file handler name ~f =
 (* For find_phrase_starting_at *)
 exception Stop of int
 
-let tag_of_sort = function
-  | Coq_lex.Comment -> Tags.Script.comment
-  | Coq_lex.Keyword -> Tags.Script.kwd
-  | Coq_lex.Declaration -> Tags.Script.decl
-  | Coq_lex.ProofDeclaration -> Tags.Script.proof_decl
-  | Coq_lex.Qed -> Tags.Script.qed
-  | Coq_lex.String -> failwith "No tag"
-
-let apply_tag (buffer:GText.buffer) orig off_conv from upto sort =
-  try
-    let tag = tag_of_sort sort in
-    let start = orig#forward_chars (off_conv from) in
-    let stop = orig#forward_chars (off_conv upto) in
-    buffer#apply_tag ~start ~stop tag
-  with _ -> ()
-
-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 ]
-
 (** Cut a part of the buffer in sentences and tag them.
     May raise [Coq_lex.Unterminated] when the zone ends with
     an unterminated sentence. *)
 
 let split_slice_lax (buffer:GText.buffer) from upto =
-  remove_tags buffer from upto;
+  buffer#remove_tag ~start:from ~stop:upto Tags.Script.comment_sentence;
   buffer#remove_tag ~start:from ~stop:upto Tags.Script.sentence;
   let slice = buffer#get_text ~start:from ~stop:upto () in
   let rec split_substring str =
     let off_conv = byte_offset_to_char_offset str in
     let slice_len = String.length str in
-    let end_off = Coq_lex.delimit_sentence (apply_tag buffer from off_conv) str
+    let is_comment,end_off = Coq_lex.delimit_sentence str
     in
     let start = from#forward_chars (off_conv end_off) in
     let stop = start#forward_char in
-    buffer#apply_tag ~start ~stop Tags.Script.sentence;
+    buffer#apply_tag ~start ~stop
+      (if is_comment then Tags.Script.comment_sentence else Tags.Script.sentence);
     let next = end_off + 1 in
     if next < slice_len then begin
       ignore (from#nocopy#forward_chars (off_conv next));
@@ -447,7 +427,7 @@ let rec backward_search cond (iter:GText.iter) =
   if iter#is_start || cond iter then iter
   else backward_search cond iter#backward_char
 
-let is_sentence_end s = s#has_tag Tags.Script.sentence
+let is_sentence_end s = s#has_tag Tags.Script.sentence || s#has_tag Tags.Script.comment_sentence
 let is_char s c = s#char = Char.code c
 
 (** Search backward the first character of a sentence, starting at [iter]
@@ -508,6 +488,7 @@ let force_retag buffer =
   try split_slice_lax buffer buffer#start_iter buffer#end_iter
   with Coq_lex.Unterminated -> ()
 
+(* GtkSource view should handle that one day !!!
 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,
@@ -527,6 +508,7 @@ let toggle_proof_visibility (buffer:GText.buffer) (cursor:GText.iter) =
   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)
+*)
 
 (** The arguments that will be passed to coqtop. No quoting here, since
     no /bin/sh when using create_process instead of open_process. *)
@@ -939,7 +921,7 @@ object(self)
     match sync get_next_phrase () with
       | None -> raise Unsuccessful
       | Some ((_,stop) as loc,phrase) ->
-	  if stop#backward_char#has_tag Tags.Script.comment
+	  if stop#backward_char#has_tag Tags.Script.comment_sentence
 	  then sync mark_processed Safe loc
           else try match self#send_to_coq ct verbosely phrase true true true with
             | Some safe -> sync mark_processed safe loc
@@ -1085,7 +1067,7 @@ object(self)
       else
 	let phrase = Stack.pop cmd_stack in
 	let stop = input_buffer#get_iter_at_mark phrase.stop in
-        if stop#backward_char#has_tag Tags.Script.comment
+        if stop#backward_char#has_tag Tags.Script.comment_sentence
 	  then n_pop n
 	  else n_pop (pred n)
     in
@@ -1120,7 +1102,7 @@ object(self)
         if i#compare stop >= 0 then n
 	else begin
 	  ignore (Stack.pop cmd_stack);
-          if stop#backward_char#has_tag Tags.Script.comment
+          if stop#backward_char#has_tag Tags.Script.comment_sentence
 	  then n_step n
 	  else n_step (succ n)
 	end
@@ -1158,7 +1140,7 @@ object(self)
           let phrase = Stack.pop cmd_stack in
 	  let stop = input_buffer#get_iter_at_mark phrase.stop in
 	  let count =
-	    if stop#backward_char#has_tag Tags.Script.comment then 0 else 1
+	    if stop#backward_char#has_tag Tags.Script.comment_sentence then 0 else 1
 	  in
 	  let finish where =
 	    input_buffer#place_cursor ~where;
@@ -2225,11 +2207,12 @@ let main files =
       GAction.add_action "Interrupt" ~label:"_Interrupt" ~stock:`STOP
 	~callback:(fun _ -> break ()) ~tooltip:"Interrupt computations"
 	~accel:(!current.modifier_for_navigation^"Break");
+(* wait for this available in GtkSourceView !
       GAction.add_action "Hide" ~label:"_Hide" ~stock:`MISSING_IMAGE
 	~callback:(fun _ -> let sess = session_notebook#current_term in
 		     toggle_proof_visibility sess.script#buffer
 		       sess.analyzed_view#get_insert) ~tooltip:"Hide proof"
-	~accel:(!current.modifier_for_navigation^"h");
+	~accel:(!current.modifier_for_navigation^"h");*)
       GAction.add_action "Previous" ~label:"_Previous" ~stock:`GO_BACK
 	~callback:(fun _ -> do_or_activate (fun a -> a#go_to_prev_occ_of_cur_word) ())
 	~tooltip:"Previous occurence" ~accel:(!current.modifier_for_navigation^"less");
diff --git a/ide/coqide_ui.ml b/ide/coqide_ui.ml
index 6b464348c..adfd9e668 100644
--- a/ide/coqide_ui.ml
+++ b/ide/coqide_ui.ml
@@ -82,7 +82,6 @@ let init () =
     <menuitem action='Start' />
     <menuitem action='End' />
     <menuitem action='Interrupt' />
-    <menuitem action='Hide' />
     <menuitem action='Previous' />
     <menuitem action='Next' />
   </menu>
@@ -145,7 +144,6 @@ let init () =
   <toolitem action='Start' />
   <toolitem action='End' />
   <toolitem action='Interrupt' />
-  <toolitem action='Hide' />
   <toolitem action='Previous' />
   <toolitem action='Next' />
   <toolitem action='Wizard' />
diff --git a/ide/tags.ml b/ide/tags.ml
index db1549e78..14a04f359 100644
--- a/ide/tags.ml
+++ b/ide/tags.ml
@@ -19,19 +19,12 @@ let processing_color = ref "light blue"
 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 comment_sentence = make_tag table ~name:"comment_sentence" []
   let error = make_tag table ~name:"error" [`UNDERLINE `DOUBLE ; `FOREGROUND "red"]
   let to_process = make_tag table ~name:"to_process" [`BACKGROUND !processing_color ;`EDITABLE false]
   let processed = make_tag table ~name:"processed" [`BACKGROUND !processed_color;`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 folded = make_tag table ~name:"locked" [`EDITABLE false; `BACKGROUND "light grey"]
   let sentence = make_tag table ~name:"sentence" []
 end
 module Proof =
diff --git a/ide/tags.mli b/ide/tags.mli
index 5a5356193..b51e85e25 100644
--- a/ide/tags.mli
+++ b/ide/tags.mli
@@ -9,19 +9,12 @@
 module Script :
 sig
   val table : GText.tag_table
-  val kwd : GText.tag
-  val qed : GText.tag
-  val decl : GText.tag
-  val proof_decl : GText.tag
-  val comment : GText.tag
-  val reserved : GText.tag
+  val comment_sentence : GText.tag
   val error : GText.tag
   val to_process : GText.tag
   val processed : GText.tag
   val unjustified : GText.tag
   val found : GText.tag
-  val hidden : GText.tag
-  val folded : GText.tag
   val sentence : GText.tag
 end