diff options
Diffstat (limited to 'parsing')
| -rw-r--r-- | parsing/tok.ml | 18 | ||||
| -rw-r--r-- | parsing/tok.mli | 3 |
2 files changed, 17 insertions, 4 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 55fcd33272..5750096a28 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 |