From 0976a670cf853c9bc61b3eee6dceae4a429e066f Mon Sep 17 00:00:00 2001
From: Enrico Tassi
Date: Wed, 19 Jun 2019 11:28:56 +0200
Subject: [test-suite] support for unit-tests/ide/ tests linking coq.ide

---
 test-suite/Makefile | 5 +++++
 1 file changed, 5 insertions(+)

(limited to 'test-suite')

diff --git a/test-suite/Makefile b/test-suite/Makefile
index ed4777608a..6949f9c386 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
-- 
cgit v1.2.3


From 71ea3ca8b4d3a6fa6b005e48ff7586176b06259e Mon Sep 17 00:00:00 2001
From: Enrico Tassi
Date: Wed, 19 Jun 2019 10:49:55 +0200
Subject: [test] unit tests for ide/coq_lex.ml

---
 test-suite/unit-tests/ide/lex_tests.ml | 50 ++++++++++++++++++++++++++++++++++
 1 file changed, 50 insertions(+)
 create mode 100644 test-suite/unit-tests/ide/lex_tests.ml

(limited to 'test-suite')

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
-- 
cgit v1.2.3