diff options
| author |  letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2010-05-19 15:29:48 +0000 |
|---|---|---|
| committer | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2010-05-19 15:29:48 +0000 |
| commit | 1b089eb0231b4bd6d4cafb30f9e051bb53665978 (patch) | |
| tree | 489e0f8ce7b4a80db388c63219b9cf4380b7f185 /parsing/g_xml.ml4 | |
| parent | 259dde7928696593c2d3c6de474f5cf50fa4417d (diff) | |
Add (almost) compatibility with camlp4, without breaking support for camlp5
The choice between camlp4/5 is done during configure with flags
-usecamlp5 (default for the moment) vs. -usecamlp4.
Currently, to have a full camlp4 compatibility, you need to change
all "EXTEND" and "GEXTEND Gram" into "EXTEND Gram", and change "EOI"
into "`EOI" in grammar entries. I've a sed script that does that
(actually the converse), but I prefer to re-think it and check a few
things before branching this sed into the build mechanism.
lib/compat.ml4 is heavily used to hide incompatibilities between camlp4/5
and try to propose a common interface (cf LexerSig / GrammarSig).
A few incompatible quotations have been turned into underlying code
manually, in order to make the IFDEF CAMLP5 THEN ... ELSE ... END
parsable by both camlp4 and 5. See in particular the fate of
<:str_item< declare ... end >>
Stdpp isn't used anymore, but rather Ploc (hidden behind local module Loc).
This forces to use camlp5 > 5.01.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13019 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'parsing/g_xml.ml4')
| -rw-r--r-- | parsing/g_xml.ml4 | 7 |
1 files changed, 4 insertions, 3 deletions
diff --git a/parsing/g_xml.ml4 b/parsing/g_xml.ml4 index 901f7ff10..2e2796a22 100644 --- a/parsing/g_xml.ml4 +++ b/parsing/g_xml.ml4 @@ -18,6 +18,7 @@ open Libnames open Nametab open Detyping +open Tok (* Generic xml parser without raw data *) @@ -29,7 +30,7 @@ let check_tags loc otag ctag = user_err_loc (loc,"",str "closing xml tag " ++ str ctag ++ str "does not match open xml tag " ++ str otag ++ str ".") -let xml_eoi = (Gram.Entry.create "xml_eoi" : xml Gram.Entry.e) +let xml_eoi = (Gram.entry_create "xml_eoi" : xml Gram.entry) GEXTEND Gram GLOBAL: xml_eoi; @@ -273,5 +274,5 @@ let rec interp_xml_tactic_arg = function let parse_tactic_arg ch = interp_xml_tactic_arg - (Pcoq.Gram.Entry.parse xml_eoi - (Pcoq.Gram.parsable (Stream.of_channel ch))) + (Pcoq.Gram.entry_parse xml_eoi + (Pcoq.Gram.parsable (Stream.of_channel ch))) |