aboutsummaryrefslogtreecommitdiff
path: root/test-suite/unit-tests/ide
diff options
context:
space:
mode:
Diffstat (limited to 'test-suite/unit-tests/ide')
-rw-r--r--test-suite/unit-tests/ide/lex_tests.ml50
1 files changed, 0 insertions, 50 deletions
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