From 8f118b444db7693dcc16dda4c271d2528bfa949a Mon Sep 17 00:00:00 2001
From: Enrico Tassi
Date: Wed, 24 Sep 2014 17:37:10 +0200
Subject: 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".
---
 printing/ppvernac.ml | 5 ++++-
 1 file changed, 4 insertions(+), 1 deletion(-)

(limited to 'printing')

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... *)
-- 
cgit v1.2.3