From 70a139733dfaa42d665a85736ee4324d926723ed Mon Sep 17 00:00:00 2001
From: Jim Fehrle
Date: Sun, 7 Oct 2018 15:14:56 -0700
Subject: Make diffs work for more input strings

Diff code uses the lexer to recognize tokens in the inputs, which can be
Pp.t's or strings.  To add the highlights in the Pp.t, the diff code
matches characters in the input to characters in the tokens.  Current
code fails for inputs containing quote marks or "(*" because the quote
marks and comments don't appear in the tokens.  This commit adds a "diff
mode" to the lexer to return those characters, making the diff routine
more robust.
---
 printing/proof_diffs.ml | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

(limited to 'printing/proof_diffs.ml')

diff --git a/printing/proof_diffs.ml b/printing/proof_diffs.ml
index b280ce909b..c1ea067567 100644
--- a/printing/proof_diffs.ml
+++ b/printing/proof_diffs.ml
@@ -88,7 +88,8 @@ let tokenize_string s =
   let st = CLexer.get_lexer_state () in
   try
     let istr = Stream.of_string s in
-    let lex = CLexer.lexer.Gramlib.Plexing.tok_func istr in
+    let lexer = CLexer.make_lexer ~diff_mode:true in
+    let lex = lexer.Gramlib.Plexing.tok_func istr in
     let toks = stream_tok [] (fst lex) in
     CLexer.set_lexer_state st;
     toks
-- 
cgit v1.2.3