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

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

4 files changed, 116 insertions, 3 deletions

diff --git a/META.coq.in b/META.coq.in
index ef5de8da2b..f7922e0ac2 100644
--- a/META.coq.in
+++ b/META.coq.in
@@ -244,14 +244,12 @@ package "idetop" (
 
 )
 
-# XXX Depends on way less than toplevel
 package "ide" (
 
   description = "Coq IDE Libraries"
   version     = "8.10"
 
-# XXX Add GTK
-  requires    = "coq.toplevel"
+  requires    = "coq.lib, coq.ideprotocol, lablgtk3, lablgtk3-sourceview3"
   directory   = "ide"
 
   archive(byte)    = "ide.cma"
@@ -259,6 +257,19 @@ package "ide" (
 
 )
 
+package "ideprotocol" (
+
+  description = "Coq IDE protocol"
+  version     = "8.10"
+
+  requires    = "coq.toplevel"
+  directory   = "ide/protocol"
+
+  archive(byte)    = "ideprotocol.cma"
+  archive(native)  = "ideprotocol.cmxa"
+
+)
+
 package "plugins" (
 
   description = "Coq built-in plugins"
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
diff --git a/test-suite/Makefile b/test-suite/Makefile
index a48a71c159..ec61f60791 100644
--- a/test-suite/Makefile
+++ b/test-suite/Makefile
@@ -299,6 +299,11 @@ unit-tests/%.ml.log: unit-tests/%.ml unit-tests/src/$(UNIT_LINK)
 	$(HIDE)$(OCAMLBEST) -linkall -linkpkg -package coq.toplevel,oUnit \
 	     -I unit-tests/src $(UNIT_LINK) $< -o $<.test;
 	$(HIDE)./$<.test
+unit-tests/ide/%.ml.log: unit-tests/ide/%.ml unit-tests/src/$(UNIT_LINK)
+	$(SHOW) 'TEST      $<'
+	$(HIDE)$(OCAMLBEST) -linkall -linkpkg -package coq.ide,oUnit \
+	     -I unit-tests/src $(UNIT_LINK) $< -o $<.test;
+	$(HIDE)./$<.test
 
 #######################################################################
 # Other generic tests
diff --git a/test-suite/unit-tests/ide/lex_tests.ml b/test-suite/unit-tests/ide/lex_tests.ml
new file mode 100644
index 0000000000..3082acdf1f
--- /dev/null
+++ b/test-suite/unit-tests/ide/lex_tests.ml
@@ -0,0 +1,50 @@
+open Utest
+
+let log_out_ch = open_log_out_ch __FILE__
+
+let lex s =
+  let n =
+    let last = String.length s - 1 in
+    if s.[last] = '.' then Some last else None in
+  let stop = ref None in
+  let f i _ = assert(!stop = None); stop := Some i in
+  begin try Coq_lex.delimit_sentences f s
+  with Coq_lex.Unterminated -> () end;
+  if n <> !stop then begin
+    let p_opt = function None -> "None" | Some i -> "Some " ^ string_of_int i in
+    Printf.fprintf log_out_ch "ERROR: %S\nEXPECTED: %s\nGOT: %s\n" s (p_opt n) (p_opt !stop)
+  end;
+  n = !stop
+
+let i2s i = "test at line: " ^ string_of_int i
+
+let tests = [
+
+  mk_bool_test (i2s __LINE__) "no quotation" @@ lex
+  "foo.+1 bar."
+  ;
+  mk_bool_test (i2s __LINE__) "quotation" @@ lex
+  "foo constr:(xxx)."
+  ;
+  mk_bool_test (i2s __LINE__) "quotation with dot" @@ lex
+  "foo constr:(xxx. yyy)."
+  ;
+  mk_bool_test (i2s __LINE__) "quotation with dot double paren" @@ lex
+  "foo constr:((xxx. (foo.+1 ) \")\" yyy))."
+  ;
+  mk_bool_test (i2s __LINE__) "quotation with dot paren [" @@ lex
+  "foo constr:[xxx. (foo.+1 ) \")\" yyy]."
+  ;
+  mk_bool_test (i2s __LINE__) "quotation with dot double paren [" @@ lex
+  "foo constr:[[xxx. (foo.+1 ) \")\" yyy]]."
+  ;
+  mk_bool_test (i2s __LINE__) "quotation with dot triple paren [" @@ lex
+  "foo constr:[[[xxx. (foo.+1 @@ [] ) \"]])\" yyy]]]."
+  ;
+  mk_bool_test (i2s __LINE__) "quotation nesting {" @@ lex
+  "bar:{{ foo {{ hello. }} }}."
+  ;
+
+]
+
+let _ = run_tests __FILE__ log_out_ch tests