diff options
| author | Jim Fehrle | 2018-07-01 13:02:02 -0700 |
|---|---|---|
| committer | Jim Fehrle | 2018-07-23 20:13:29 -0700 |
| commit | 97069f69ab3a58cc4ccbaa1a835912c6c31dde4d (patch) | |
| tree | 8b762a723d1ff829724c4a912f6a34997ef463c5 /printing/proof_diffs.ml | |
| parent | 8de046df97b1ea391a3f3879c20c74d53c9fba48 (diff) | |
Make tokenize_string an optional parameter for diff methods in pp_diffs.
Remove forward reference to lexer.
Diffstat (limited to 'printing/proof_diffs.ml')
| -rw-r--r-- | printing/proof_diffs.ml | 5 |
1 files changed, 1 insertions, 4 deletions
diff --git a/printing/proof_diffs.ml b/printing/proof_diffs.ml index 5043759d32..7131ced15b 100644 --- a/printing/proof_diffs.ml +++ b/printing/proof_diffs.ml @@ -89,7 +89,6 @@ let cprintf s = cfprintf !log_out_ch s module StringMap = Map.Make(String);; -(* placed here so that pp_diff.ml can access the lexer through dependency injection *) let tokenize_string s = (* todo: cLexer changes buff as it proceeds. Seems like that should be saved, too. But I don't understand how it's used--it looks like things get appended to it but @@ -112,8 +111,6 @@ let tokenize_string s = CLexer.set_lexer_state st; raise (Diff_Failure "Input string is not lexable");; -let _ = Pp_diff.tokenize_string := tokenize_string - type hyp_info = { idents: string list; @@ -152,7 +149,7 @@ let diff_hyps o_line_idents o_map n_line_idents n_map = let (o_line, o_pp) = setup old_ids o_map in let (n_line, n_pp) = setup new_ids n_map in - let hyp_diffs = diff_str o_line n_line in + let hyp_diffs = diff_str ~tokenize_string o_line n_line in let (has_added, has_removed) = has_changes hyp_diffs in if show_removed () && has_removed then begin let o_entry = StringMap.find (List.hd old_ids) o_map in |