Merge PR #10394: [ide] chop sentences taking into account QUOTATION token

Ack-by: SkySkimmer
Ack-by: gares
Reviewed-by: ppedrot

1 files changed, 47 insertions, 0 deletions

diff --git a/ide/coq_lex.mll b/ide/coq_lex.mll
index 0010229f9b..b46ab49771 100644
--- a/ide/coq_lex.mll
+++ b/ide/coq_lex.mll
@@ -50,6 +50,41 @@ and comment = parse
   | utf8_extra_byte { incr utf8_adjust; comment lexbuf }
   | _ { comment lexbuf }
 
+and quotation o c n l = parse | eof { raise Unterminated } | _ {
+  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
+}
+
+and quotation_nesting o c n l v = parse | eof { raise Unterminated } | _ {
+  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
+}
+
+and quotation_closing o c n l v = parse | eof { raise Unterminated } | _ {
+  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
+}
+
+and quotation_start o c n = parse | eof { raise Unterminated } | _ {
+  let x = Lexing.lexeme lexbuf in
+  if x = o then quotation_start o c (n+1) lexbuf
+  else quotation o c n 1 lexbuf
+}
+
 (** NB : [mkiter] should be called on increasing offsets *)
 
 and sentence initial stamp = parse
@@ -83,6 +118,18 @@ 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;
+      sentence false stamp lexbuf
+    }
   | space+ {
        (* Parsing spaces is the only situation preserving initiality *)
        sentence initial stamp lexbuf