diff options
| author |  Enrico Tassi <Enrico.Tassi@inria.fr> | 2014-09-24 17:37:10 +0200 |
|---|---|---|
| committer | Enrico Tassi <Enrico.Tassi@inria.fr> | 2014-09-29 21:54:31 +0200 |
| commit | 8f118b444db7693dcc16dda4c271d2528bfa949a (patch) | |
| tree | a01df0fd808a3d17b1e3d12d7710225c533bfe12 /parsing | |
| parent | ec49447d078da25959d617ae23e55a668fdd1646 (diff) | |
Notation: option to attach extra pretty printing rules to notations
so that one can retrieve them and pass them to third party tools (i.e.
print the AST with the notations attached to the nodes concerned).
Available syntax:
- all in one:
Notation "a /\ b" := ... (format "...", format "latex" "#1 \wedge #2").
- a posteriori:
Format Notation "a /\ b" "latex" "#1 \wedge #2".
Diffstat (limited to 'parsing')
| -rw-r--r-- | parsing/g_vernac.ml4 | 8 |
1 files changed, 7 insertions, 1 deletions
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4 index 955179ba0..cabb09dc3 100644 --- a/parsing/g_vernac.ml4 +++ b/parsing/g_vernac.ml4 @@ -1026,6 +1026,8 @@ GEXTEND Gram modl = [ "("; l = LIST1 syntax_modifier SEP ","; ")" -> l | -> [] ]; sc = OPT [ ":"; sc = IDENT -> sc ] -> VernacNotation (local,c,(s,modl),sc) + | IDENT "Format"; IDENT "Notation"; n = STRING; s = STRING; fmt = STRING -> + VernacNotationAddFormat (n,s,fmt) | IDENT "Tactic"; IDENT "Notation"; n = tactic_level; pil = LIST1 production_item; ":="; t = Tactic.tactic @@ -1072,7 +1074,11 @@ GEXTEND Gram SetOnlyParsing Flags.Current | IDENT "compat"; s = STRING -> SetOnlyParsing (Coqinit.get_compat_version s) - | IDENT "format"; s = [s = STRING -> (!@loc,s)] -> SetFormat s + | IDENT "format"; s1 = [s = STRING -> (!@loc,s)]; + s2 = OPT [s = STRING -> (!@loc,s)] -> + begin match s1, s2 with + | (_,k), Some s -> SetFormat(k,s) + | s, None -> SetFormat ("text",s) end | x = IDENT; ","; l = LIST1 [id = IDENT -> id ] SEP ","; "at"; lev = level -> SetItemLevel (x::l,lev) | x = IDENT; "at"; lev = level -> SetItemLevel ([x],lev) |