diff options
| author | Gaëtan Gilbert | 2020-05-10 21:39:00 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2020-05-17 13:22:09 +0200 |
| commit | 7da245bd2db7496628645a43965e5df966234fd5 (patch) | |
| tree | 18401628f36c56ac72ab7529232e014cd52c55de /test-suite | |
| parent | 4c69c4a870f5ef340536798dcdf1025e61a375f9 (diff) | |
Revert "[test] unit tests for ide/coq_lex.ml" + makefile support
This reverts commits 71ea3ca8b4d3a6fa6b005e48ff7586176b06259e and
0976a670cf853c9bc61b3eee6dceae4a429e066f.
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, 0 insertions, 55 deletions
diff --git a/test-suite/Makefile b/test-suite/Makefile index a0a2367236..9935c4eed0 100644 --- a/test-suite/Makefile +++ b/test-suite/Makefile @@ -315,11 +315,6 @@ 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 deleted file mode 100644 index 3082acdf1f..0000000000 --- a/test-suite/unit-tests/ide/lex_tests.ml +++ /dev/null @@ -1,50 +0,0 @@ -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 |