From f374c2562b9522bd90330f6f17f0a7e41c723e8b Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Fri, 21 Feb 2020 12:46:22 -0500
Subject: [parsing] Move `coq_parsable` custom logic to Grammar.

Latest refactorings allow us to make the signature Coq parser a
standard `Grammar.S` one; the only bit needed is to provide the extra
capabilities to the `Lexer` signature w.r.t. to comments state.

The handling of Lexer state is still a bit ad-hoc, in particular it is
global whereas it should be fully attached to the parsable. This may
work ok in batch mode but the current behavior may be buggy in the
interactive context.

This PR doesn't solve that but it is a step towards a more functional
solution.
---
 printing/proof_diffs.ml | 7 +++----
 1 file changed, 3 insertions(+), 4 deletions(-)

(limited to 'printing')

diff --git a/printing/proof_diffs.ml b/printing/proof_diffs.ml
index fb91ea7b5c..9d75341795 100644
--- a/printing/proof_diffs.ml
+++ b/printing/proof_diffs.ml
@@ -98,18 +98,17 @@ let tokenize_string s =
     else
       stream_tok ((Tok.extract_string true e) :: acc) str
   in
-  let st = CLexer.get_lexer_state () in
+  let st = CLexer.Lexer.State.get () in
   try
     let istr = Stream.of_string s in
     let lex = CLexer.LexerDiff.tok_func istr in
     let toks = stream_tok [] (fst lex) in
-    CLexer.set_lexer_state st;
+    CLexer.Lexer.State.set st;
     toks
   with exn ->
-    CLexer.set_lexer_state st;
+    CLexer.Lexer.State.set st;
     raise (Diff_Failure "Input string is not lexable");;
 
-
 type hyp_info = {
   idents: string list;
   rhs_pp: Pp.t;
-- 
cgit v1.2.3