From 3da99625500e827f8c846e1e0acca9245b1282f2 Mon Sep 17 00:00:00 2001 From: Chet Murthy Date: Fri, 3 May 2024 17:56:30 -0700 Subject: [PATCH] minor change for camlp5 8.03.00 compat This breaks compat with previous versions of Camlp5 OCaml 5.2.0 supports raw identifiers, e.g. "\begin". The Camlp5 pretty-printer needs to know which "identifier-like" strings are keywords, so it can escape them as raw identifiers when pretty-printing. Since Camlp5 supports more than one syntax, that means different syntaxes can have different sets of identifiers. Hence, the lexer has to support exposing the set of keywords, and the pretty-printer has to support being parameterized by the keywords. matita creates a Camlp5 lexer, so it needs to be changed to have that keyword-table slot (even though it seems it doesn't use it). --- components/content_pres/cicNotationLexer.ml | 1 + 1 file changed, 1 insertion(+) diff --git a/components/content_pres/cicNotationLexer.ml b/components/content_pres/cicNotationLexer.ml index 070a88db..08589470 100644 --- a/components/content_pres/cicNotationLexer.ml +++ b/components/content_pres/cicNotationLexer.ml @@ -201,6 +201,7 @@ let mk_lexer token = Token.tok_match = Token.default_match; Token.tok_text = Token.lexer_text; Token.tok_comm = None; + Token.kwds = Hashtbl.create 23; } let expand_macro lexbuf =