Coqide: fixes and clarifications concerning sentence-terminators

 - New terminators { and } are now accepted only when followed
   by a blank or newline.

 - reorganisation of coq_lex.mll : in particular stop adding
   a fake " " when parsing a string.

 - fix the handling of copy-pasted string containing tags :
   we isolate this zone, untag it, and retag it properly.
   For that we don't monitor the "changed" event anymore,
   but wait for a "end_user_input" instead.

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

1 files changed, 89 insertions, 109 deletions

diff --git a/ide/coq_lex.mll b/ide/coq_lex.mll
index 4bb4b5beb..b605c13e5 100644
--- a/ide/coq_lex.mll
+++ b/ide/coq_lex.mll
@@ -19,61 +19,55 @@
 
   (* Without this table, the automaton would be too big and
      ocamllex would fail *)
-  let is_one_word_command =
-    let h = Hashtbl.create 97 in
-    List.iter (fun s -> Hashtbl.add h s ())
-      [  "Add" ; "Check"; "Eval"; "Extraction" ;
-	 "Load" ; "Undo"; "Goal";
-	 "Proof" ; "Print";"Save" ;
-	 "End" ; "Section"; "Chapter"; "Transparent"; "Opaque"; "Comments"
-      ];
-    Hashtbl.mem h
-
-  let is_constr_kw =
-    let h = Hashtbl.create 97 in
-      List.iter (fun s -> Hashtbl.add h s ())
-	[ "forall"; "fun"; "match"; "fix"; "cofix"; "with"; "for";
-	  "end"; "as"; "let"; "in"; "if"; "then"; "else"; "return";
-	  "Prop"; "Set"; "Type" ];
-      Hashtbl.mem h
 
-  (* Without this table, the automaton would be too big and
-     ocamllex would fail *)
-  let is_one_word_declaration =
-    let h = Hashtbl.create 97 in
-      List.iter (fun s -> Hashtbl.add h s ())
-	[ (* 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" ; "Typeclasses"; "Instance"; "Include"; "Context"; "Class"
-	];
-      Hashtbl.mem h
-
-  let is_proof_declaration =
-    let h = Hashtbl.create 97 in
-    List.iter (fun s -> Hashtbl.add h s ())
+  let tag_of_ident =
+    let one_word_commands =
+      [ "Add" ; "Check"; "Eval"; "Extraction" ;
+	"Load" ; "Undo"; "Goal";
+	"Proof" ; "Print";"Save" ;
+	"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" ; "Typeclasses"; "Instance"; "Include"; "Context"; "Class" ]
+    in
+    let proof_declarations =
       [ "Theorem" ; "Lemma" ; " Fact" ; "Remark" ; "Corollary" ;
-        "Proposition" ; "Property" ];
-    Hashtbl.mem h
+        "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 is_proof_end =
-    let h = Hashtbl.create 97 in
-    List.iter (fun s -> Hashtbl.add h s ())
-      [ "Qed" ; "Defined" ; "Admitted"; "Abort" ];
-    Hashtbl.mem h
-
-  let start = ref true
-  let last_leading_blank = ref 0
 }
 
 let space =
-  [' ' '\010' '\013' '\009' '\012']
+  [' ' '\n' '\r' '\t' '\012'] (* '\012' is form-feed *)
 
 let firstchar =
   ['$' 'A'-'Z' 'a'-'z' '_' '\192'-'\214' '\216'-'\246' '\248'-'\255']
@@ -81,9 +75,9 @@ let identchar =
   ['$' 'A'-'Z' 'a'-'z' '_' '\192'-'\214' '\216'-'\246' '\248'-'\255' '\'' '0'-'9']
 let ident = firstchar identchar*
 
-let sentence_sep = '.' [ ' ' '\r' '\n' '\t' ]
+let undotted_sep = [ '{' '}' ] (space | eof)
 
-let undotted_command = [ '{' '}' ]
+let dot_sep = '.' (space | eof)
 
 let multiword_declaration =
   "Module" (space+ "Type")?
@@ -131,81 +125,67 @@ rule coq_string = parse
 and comment = parse
   | "(*" { ignore (comment lexbuf); comment lexbuf }
   | "\"" { ignore (coq_string lexbuf); comment lexbuf }
-  | "*)" space? { (* See undotted_command rule to understand the space? *)
-      (true, Lexing.lexeme_start lexbuf + 2) }
+  | "*)" { (true, Lexing.lexeme_start lexbuf + 2) }
   | eof { (false, Lexing.lexeme_end lexbuf) }
   | _ { comment lexbuf }
 
-and sentence stamp = parse
-  | space+ {
-      if !start then last_leading_blank := Lexing.lexeme_end lexbuf;
-      sentence stamp lexbuf
-    }
+and sentence initial stamp = parse
   | "(*" {
       let comm_start = Lexing.lexeme_start lexbuf in
       let trully_terminated,comm_end = comment lexbuf in
       stamp comm_start comm_end Comment;
-	(* A comment alone is a sentence.
-	   A comment in a sentence doesn't terminate the sentence.
-	*)
-      if not !start then sentence stamp lexbuf
-      else if not trully_terminated then raise Not_found
+      if not trully_terminated then raise Unterminated;
+      (* A comment alone is a sentence.
+	 A comment in a sentence doesn't terminate the sentence.
+         Note: comm_end is the first position _after_ the comment,
+	 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
     }
   | "\"" {
       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
+      sentence false stamp lexbuf
     }
   | multiword_declaration {
-      if !start then begin
-        start := false;
-        stamp (Lexing.lexeme_start lexbuf) (Lexing.lexeme_end lexbuf) Declaration
-      end;
-      sentence stamp lexbuf
+      if initial then here stamp lexbuf Declaration;
+      sentence false stamp lexbuf
     }
   | multiword_command {
-      if !start then begin
-        start := false;
-        stamp (Lexing.lexeme_start lexbuf) (Lexing.lexeme_end lexbuf) Keyword
-      end;
-      sentence stamp lexbuf }
+      if initial then here stamp lexbuf Keyword;
+      sentence false stamp lexbuf
+    }
   | ident as id {
-      if !start then begin
-        start := false;
-        if id <> "Time" then begin
-            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
-              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
-	  stamp (Lexing.lexeme_start lexbuf) (Lexing.lexeme_end lexbuf) Keyword
-      end;
-      sentence stamp lexbuf }
-  | ".."
-  | _    { sentence stamp lexbuf}
-  | undotted_command space? { (* the space? here is a awful consequence of
-				 the way lexing is asked by Coqide.split_slice_lax:
-				 a training whitespace is add at the end of text
-				 and then dropped. This space has consequently to be
-				 part of the sentence *)
-      if not !start then sentence stamp lexbuf (* in the middle of a command our token
-						  aren't command *)}
-  | sentence_sep { }
-  | eof { raise Not_found }
+      (try here stamp lexbuf (tag_of_ident initial id) with Not_found -> ());
+      sentence false stamp lexbuf }
+  | dot_sep { Lexing.lexeme_start lexbuf } (* The usual "." terminator *)
+  | ".." dot_sep { Lexing.lexeme_start lexbuf + 2 } (* The "..." special case *)
+  | undotted_sep {
+      (* Separators like { or } are only active at the start of a sentence *)
+      if initial then Lexing.lexeme_start lexbuf
+      else sentence false stamp lexbuf
+    }
+  | space+ {
+       (* Parsing spaces is the only situation preserving initiality *)
+       sentence initial stamp lexbuf
+    }
+  | _ {
+      (* Any other characters (for instance bullets "-" "*" "+") *)
+      sentence false stamp lexbuf
+    }
+  | eof { raise Unterminated }
 
 {
-  let find_end_offset stamp slice =
-    let lb = Lexing.from_string slice in
-    start := true;
-    last_leading_blank := 0;
-    sentence stamp lb;
-    !last_leading_blank,Lexing.lexeme_end lb
+
+  (** Parse a sentence in string [slice], tagging relevant parts with
+      function [stamp], and returning the position of the first
+      sentence delimitor (either "." or "{" or "}" or the end of a comment).
+      It will raise [Unterminated] when no end of sentence is found.
+  *)
+
+  let delimit_sentence stamp slice =
+    sentence true stamp (Lexing.from_string slice)
+
 }