diff options
| author | Jim Fehrle | 2018-11-29 20:17:22 -0800 |
|---|---|---|
| committer | Jim Fehrle | 2018-12-10 16:10:10 -0800 |
| commit | c00506b3fdde0ce4d2c0607dd097463de21301af (patch) | |
| tree | 2302d6d733eea2748ea025449c6468b44f2b3100 | |
| parent | 43ecefe2805e2178fa3c113c4889b7720676c905 (diff) | |
For diffs, return exactly the characters that make up STRING and FIELD tokens
| -rw-r--r-- | parsing/tok.ml | 18 | ||||
| -rw-r--r-- | parsing/tok.mli | 3 | ||||
| -rw-r--r-- | printing/proof_diffs.ml | 2 |
3 files changed, 18 insertions, 5 deletions
diff --git a/parsing/tok.ml b/parsing/tok.ml index 91b4f25ba3..c0d5b6742d 100644 --- a/parsing/tok.ml +++ b/parsing/tok.ml @@ -36,12 +36,24 @@ let equal t1 t2 = match t1, t2 with | EOI, EOI -> true | _ -> false -let extract_string = function +let extract_string diff_mode = function | KEYWORD s -> s | IDENT s -> s - | STRING s -> s + | STRING s -> + if diff_mode then + let escape_quotes s = + let len = String.length s in + let buf = Buffer.create len in + for i = 0 to len-1 do + let ch = String.get s i in + Buffer.add_char buf ch; + if ch = '"' then Buffer.add_char buf '"' else () + done; + Buffer.contents buf + in + "\"" ^ (escape_quotes s) ^ "\"" else s | PATTERNIDENT s -> s - | FIELD s -> s + | FIELD s -> if diff_mode then "." ^ s else s | INT s -> s | LEFTQMARK -> "?" | BULLET s -> s diff --git a/parsing/tok.mli b/parsing/tok.mli index 9b8c008555..93307db760 100644 --- a/parsing/tok.mli +++ b/parsing/tok.mli @@ -22,7 +22,8 @@ type t = | EOI val equal : t -> t -> bool -val extract_string : t -> string +(* pass true for diff_mode *) +val extract_string : bool -> t -> string val to_string : t -> string (* Needed to fit Camlp5 signature *) val print : Format.formatter -> t -> unit diff --git a/printing/proof_diffs.ml b/printing/proof_diffs.ml index 508e939df8..b5f9da30a3 100644 --- a/printing/proof_diffs.ml +++ b/printing/proof_diffs.ml @@ -83,7 +83,7 @@ let tokenize_string s = if Tok.(equal e EOI) then List.rev acc else - stream_tok ((Tok.extract_string e) :: acc) str + stream_tok ((Tok.extract_string true e) :: acc) str in let st = CLexer.get_lexer_state () in try |