2 files changed, 41 insertions, 15 deletions

diff --git a/test-suite/unit-tests/lib/pp_big_vect.ml b/test-suite/unit-tests/lib/pp_big_vect.ml
new file mode 100644
index 0000000000..e1cdd290e2
--- /dev/null
+++ b/test-suite/unit-tests/lib/pp_big_vect.ml
@@ -0,0 +1,14 @@
+open OUnit
+open Pp
+
+let pr_big_vect =
+  let n = "pr_big_vect" in
+  n >:: (fun () ->
+      let v = Array.make (1 lsl 20) () in
+      let pp = prvecti_with_sep spc (fun _ _ -> str"x") v in
+      let str = string_of_ppcmds pp in
+      ignore(str))
+
+let tests = [pr_big_vect]
+
+let () = Utest.run_tests __FILE__ (Utest.open_log_out_ch __FILE__) tests
diff --git a/test-suite/unit-tests/printing/proof_diffs_test.ml b/test-suite/unit-tests/printing/proof_diffs_test.ml
index 526cefec44..d0b8d21b69 100644
--- a/test-suite/unit-tests/printing/proof_diffs_test.ml
+++ b/test-suite/unit-tests/printing/proof_diffs_test.ml
@@ -51,26 +51,38 @@ let t () =
   assert_equal ~msg:"has `Removed" ~printer:string_of_bool true has_removed
 let _ = add_test "diff_str add/remove" t
 
-(* example of a limitation, not really a test *)
-let t () =
-  try
-    let _ = diff_str "a" ">" in
-    assert_failure "unlexable string gives an exception"
-  with _ -> ()
-let _ = add_test "diff_str unlexable" t
-
-(* problematic examples for tokenize_string:
-   comments omitted
-   quoted string loses quote marks (are escapes supported/handled?)
-   char constant split into 2
+(* lexer tweaks:
+   comments are lexed as multiple tokens
+   strings tokens include begin/end quotes and embedded ""
+   single multibyte characters returned even if they're not keywords
+
+   inputs that give a lexer failure (but no use case needs them yet):
+     ".12"
+     unterminated string
+     invalid UTF-8 sequences
    *)
 let t () =
-  List.iter (fun x -> cprintf "'%s' " x) (tokenize_string "(* comment *) \"string\" 'c' xx");
-  cprintf "\n"
-let _ = add_test "tokenize_string examples" t
+  let str = "(* comment.field *) ?id () \"str\"\"ing\" \\ := Ж > ∃ 'c' xx" in
+  let toks = tokenize_string str in
+  (*List.iter (fun x -> cprintf "'%s' " x) toks;*)
+  (*cprintf "\n";*)
+  let str_no_white = String.concat "" (String.split_on_char ' ' str) in
+  assert_equal ~printer:(fun x -> x) str_no_white (String.concat "" toks);
+  List.iter (fun s ->
+    assert_equal ~msg:("'" ^ s ^ "' is a single token") ~printer:string_of_bool true (List.mem s toks))
+    [ "(*"; "()"; ":="]
+
+let _ = add_test "tokenize_string/diff_mode in lexer" t
 
 open Pp
 
+(* example that was failing from #8922 *)
+let t () =
+  Proof_diffs.write_diffs_option "removed";
+  ignore (diff_str "X : ?Goal" "X : forall x : ?Goal0, ?Goal1");
+  Proof_diffs.write_diffs_option "on"
+let _ = add_test "shorten_diff_span failure from #8922" t
+
 (* note pp_to_string concatenates adjacent strings, could become one token,
 e.g. str " a" ++ str "b " will give a token "ab" *)
 (* checks background is present and correct *)