diff options
| author | Enrico Tassi | 2014-09-24 17:37:10 +0200 |
|---|---|---|
| committer | Enrico Tassi | 2014-09-29 21:54:31 +0200 |
| commit | 8f118b444db7693dcc16dda4c271d2528bfa949a (patch) | |
| tree | a01df0fd808a3d17b1e3d12d7710225c533bfe12 /printing | |
| 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 'printing')
| -rw-r--r-- | printing/ppvernac.ml | 5 |
1 files changed, 4 insertions, 1 deletions
diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml index 8ca05f2cad..b841c19cc3 100644 --- a/printing/ppvernac.ml +++ b/printing/ppvernac.ml @@ -344,7 +344,8 @@ let pr_syntax_modifier = function | SetEntryType (x,typ) -> str x ++ spc() ++ pr_set_entry_type typ | SetOnlyParsing Flags.Current -> str"only parsing" | SetOnlyParsing v -> str("compat \"" ^ Flags.pr_version v ^ "\"") - | SetFormat s -> str"format " ++ pr_located qs s + | SetFormat("text",s) -> str"format " ++ pr_located qs s + | SetFormat(k,s) -> str"format " ++ qs k ++ spc() ++ pr_located qs s let pr_syntax_modifiers = function | [] -> mt() @@ -571,6 +572,8 @@ let rec pr_vernac = function | VernacSyntaxExtension (_,(s,l)) -> str"Reserved Notation" ++ spc() ++ pr_located qs s ++ pr_syntax_modifiers l + | VernacNotationAddFormat(s,k,v) -> + str"Format Notation " ++ qs s ++ spc () ++ qs k ++ spc() ++ qs v (* Gallina *) | VernacDefinition (d,id,b) -> (* A verifier... *) |