diff options
| author | Pierre-Marie Pédrot | 2019-06-24 10:51:41 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2019-06-24 10:51:41 +0200 |
| commit | 95ff3c577233bfa012464658110da6eadb89baa2 (patch) | |
| tree | d73b363f9535cbac8ac4c87c649f32b54f2756ca /test-suite | |
| parent | e7ae7950bb50923e005898d18158593754108725 (diff) | |
| parent | 71ea3ca8b4d3a6fa6b005e48ff7586176b06259e (diff) | |
Merge PR #10394: [ide] chop sentences taking into account QUOTATION token
Ack-by: SkySkimmer
Ack-by: gares
Reviewed-by: ppedrot
Diffstat (limited to 'test-suite')
| -rw-r--r-- | test-suite/Makefile | 5 | ||||
| -rw-r--r-- | test-suite/unit-tests/ide/lex_tests.ml | 50 |
2 files changed, 55 insertions, 0 deletions
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 |