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.
---
 parsing/cLexer.mli | 11 +++++++++++
 1 file changed, 11 insertions(+)

(limited to 'parsing/cLexer.mli')

diff --git a/parsing/cLexer.mli b/parsing/cLexer.mli
index c0ebdd45ef..af3fd7f318 100644
--- a/parsing/cLexer.mli
+++ b/parsing/cLexer.mli
@@ -56,3 +56,14 @@ val set_lexer_state : lexer_state -> unit
 val get_lexer_state : unit -> lexer_state
 val drop_lexer_state : unit -> unit
 val get_comment_state : lexer_state -> ((int * int) * string) list
+
+(** Create a lexer.  true enables alternate handling for computing diffs.
+It ensures that, ignoring white space, the concatenated tokens equal the input
+string.  Specifically:
+- for strings, return the enclosing quotes as tokens and treat the quoted value
+as if it was unquoted, possibly becoming multiple tokens
+- for comments, return the "(*" as a token and treat the contents of the comment as if
+it was not in a comment, possibly becoming multiple tokens
+- return any unrecognized Ascii or UTF-8 character as a string
+*)
+val make_lexer : diff_mode:bool -> Tok.t Gramlib.Plexing.lexer
-- 
cgit v1.2.3