Merge PR #13097: Modify how quotations handle whole sentences.

Reviewed-by: gares

2 files changed, 60 insertions, 53 deletions

diff --git a/ide/coqide/coq_lex.mll b/ide/coqide/coq_lex.mll
index a65954d566..5d5e5f0e14 100644
--- a/ide/coqide/coq_lex.mll
+++ b/ide/coqide/coq_lex.mll
@@ -50,52 +50,40 @@ and comment = parse
   | utf8_extra_byte { incr utf8_adjust; comment lexbuf }
   | _ { comment lexbuf }
 
-and quotation o c n l = parse
+and quotation n l = parse
 | eof { raise Unterminated }
-| utf8_extra_byte { incr utf8_adjust; quotation o c n l lexbuf }
-| _ {
-  let x = Lexing.lexeme lexbuf in
-  if x = o then quotation_nesting o c n l 1 lexbuf
-  else if x = c then
-    if n = 1 && l = 1 then ()
-    else quotation_closing o c n l 1 lexbuf
-  else quotation o c n l lexbuf
-}
+| utf8_extra_byte { incr utf8_adjust; quotation n l lexbuf }
+| "{" { quotation_nesting n l 1 lexbuf }
+| "}" { quotation_closing n l 1 lexbuf }
+| _ { quotation n l lexbuf }
 
-and quotation_nesting o c n l v = parse
+and quotation_nesting n l v = parse
 | eof { raise Unterminated }
-| utf8_extra_byte { incr utf8_adjust; quotation o c n l lexbuf }
-| _ {
-  let x = Lexing.lexeme lexbuf in
-  if x = o then
-    if n = v+1 then quotation o c n (l+1) lexbuf
-    else quotation_nesting o c n l (v+1) lexbuf
-  else if x = c then quotation_closing o c n l 1 lexbuf
-  else quotation o c n l lexbuf
+| utf8_extra_byte { incr utf8_adjust; quotation n l lexbuf }
+| "{" {
+  if n = v+1 then quotation n (l+1) lexbuf
+  else quotation_nesting n l (v+1) lexbuf
 }
+| "}" { quotation_closing n l 1 lexbuf }
+| _ { quotation n l lexbuf }
 
-and quotation_closing o c n l v = parse
+and quotation_closing n l v = parse
 | eof { raise Unterminated }
-| utf8_extra_byte { incr utf8_adjust; quotation o c n l lexbuf }
-| _ {
-  let x = Lexing.lexeme lexbuf in
-  if x = c then
-    if n = v+1 then
-      if l = 1 then ()
-      else quotation o c n (l-1) lexbuf
-    else quotation_closing o c n l (v+1) lexbuf
-  else if x = o then quotation_nesting o c n l 1 lexbuf
-  else quotation o c n l lexbuf
+| utf8_extra_byte { incr utf8_adjust; quotation n l lexbuf }
+| "}" {
+  if n = v+1 then
+    if l = 1 then ()
+    else quotation n (l-1) lexbuf
+  else quotation_closing n l (v+1) lexbuf
 }
+| "{" { quotation_nesting n l 1 lexbuf }
+| _ { quotation n l lexbuf }
 
-and quotation_start o c n = parse
+and quotation_start n = parse
 | eof { raise Unterminated }
-| utf8_extra_byte { incr utf8_adjust; quotation o c n 1 lexbuf }
-| _ {
-  let x = Lexing.lexeme lexbuf in
-  if x = o then quotation_start o c (n+1) lexbuf
-  else quotation o c n 1 lexbuf
-}
+| utf8_extra_byte { incr utf8_adjust; quotation n 1 lexbuf }
+| "{" { quotation_start (n+1) lexbuf }
+| _ { quotation n 1 lexbuf }
 
 (** NB : [mkiter] should be called on increasing offsets *)
 
@@ -130,16 +118,8 @@ and sentence initial stamp = parse
       if initial then stamp (utf8_lexeme_start lexbuf + String.length (Lexing.lexeme lexbuf) - 1) Tags.Script.sentence;
       sentence initial stamp lexbuf
     }
-  | ['a'-'z' 'A'-'Z'] ":{" {
-      quotation_start "{" "}" 1 lexbuf;
-      sentence false stamp lexbuf
-    }
-  | ['a'-'z' 'A'-'Z'] ":[" {
-      quotation_start "[" "]" 1 lexbuf;
-      sentence false stamp lexbuf
-    }
-  | ['a'-'z' 'A'-'Z'] ":(" {
-      quotation_start "(" ")" 1 lexbuf;
+  | ['a'-'z' 'A'-'Z'] ":{{" {
+      quotation_start 2 lexbuf;
       sentence false stamp lexbuf
     }
   | space+ {
diff --git a/parsing/cLexer.ml b/parsing/cLexer.ml
index a98cf3b7de..f485970eec 100644
--- a/parsing/cLexer.ml
+++ b/parsing/cLexer.ml
@@ -512,6 +512,12 @@ and progress_utf8 loc last nj n c tt cs =
 and progress_from_byte loc last nj tt cs c =
   progress_utf8 loc last nj (utf8_char_size loc cs c) c tt cs
 
+let blank_or_eof cs =
+  match Stream.peek cs with
+    | None -> true
+    | Some (' ' | '\t' | '\n' |'\r') -> true
+    | _ -> false
+
 type marker = Delimited of int * char list * char list | ImmediateAsciiIdent
 
 let peek_marker_len b e s =
@@ -542,6 +548,11 @@ let parse_quotation loc bp s =
       in
       get_buff len, set_loc_pos loc bp (Stream.count s)
   | Delimited (lenmarker, bmarker, emarker) ->
+      let dot_gobbling =
+        (* only quotations starting with two curly braces can gobble sentences *)
+        match bmarker with
+        | '{' :: '{' :: _ -> true
+        | _ -> false in
       let b = Buffer.create 80 in
       let commit1 c = Buffer.add_char b c; Stream.junk s in
       let commit l = List.iter commit1 l in
@@ -557,6 +568,10 @@ let parse_quotation loc bp s =
               commit1 '\n';
               let loc = bump_loc_line_last loc (Stream.count s) in
               quotation loc depth
+        | '.' :: _ ->
+              commit1 '.';
+              if not dot_gobbling && blank_or_eof s then raise Stream.Failure;
+              quotation loc depth
         | c :: cs ->
               commit1 c;
               quotation loc depth
@@ -565,8 +580,26 @@ let parse_quotation loc bp s =
       let loc = quotation loc 0 in
       Buffer.contents b, set_loc_pos loc bp (Stream.count s)
 
+let peek_string v s =
+  let l = String.length v in
+  let rec aux i =
+    if Int.equal i l then true
+    else
+      let l' = Stream.npeek (i + 1) s in
+      match List.nth l' i with
+      | c -> Char.equal c v.[i] && aux (i + 1)
+      | exception _ -> false (* EOF *) in
+  aux 0
 
 let find_keyword loc id bp s =
+  if peek_string ":{{" s then
+    begin
+      (* "xxx:{{" always starts a sentence-gobbling quotation, whether registered or not *)
+      Stream.junk s;
+      let txt, loc = parse_quotation loc bp s in
+      QUOTATION (id ^ ":", txt), loc
+    end
+  else
   let tt = ttree_find !token_tree id in
   match progress_further loc tt.node 0 tt s with
   | None -> raise Not_found
@@ -645,12 +678,6 @@ let parse_after_qmark ~diff_mode loc bp s =
           | AsciiChar | Utf8Token _ | EmptyStream ->
             fst (process_chars ~diff_mode loc bp '?' s)
 
-let blank_or_eof cs =
-  match Stream.peek cs with
-    | None -> true
-    | Some (' ' | '\t' | '\n' |'\r') -> true
-    | _ -> false
-
 (* Parse a token in a char stream *)
 
 let rec next_token ~diff_mode loc s =