diff options
| author | Jim Fehrle | 2018-10-07 15:14:56 -0700 |
|---|---|---|
| committer | Jim Fehrle | 2018-12-20 13:01:46 -0800 |
| commit | 70a139733dfaa42d665a85736ee4324d926723ed (patch) | |
| tree | d1c78161e8f037a22ef799ff298304f1d65660b8 /printing/proof_diffs.ml | |
| parent | 2cad4dec40cef2aecb19c5a0e5a1368392be8d88 (diff) | |
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.
Diffstat (limited to 'printing/proof_diffs.ml')
| -rw-r--r-- | printing/proof_diffs.ml | 3 |
1 files changed, 2 insertions, 1 deletions
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 |