- synced notation pretty printing with parsing syntax

[helm.git] / helm / ocaml / cic_notation / grafiteParser.ml

diff --git a/helm/ocaml/cic_notation/grafiteParser.ml b/helm/ocaml/cic_notation/grafiteParser.ml
index 8bd5cc04e3e976c62dcc2f07e4cecbdfc36ec0a7..984635ec60cc44433df2b847ee3f877f1ff9edc6 100644 (file)
--- a/helm/ocaml/cic_notation/grafiteParser.ml
+++ b/helm/ocaml/cic_notation/grafiteParser.ml
@@ -30,6 +30,9 @@ let grammar = CicNotationParser.level2_ast_grammar
 let term = CicNotationParser.term
 let statement = Grammar.Entry.create grammar "statement"
 
+let add_raw_attribute ?context ~text term =
+  CicNotationPt.AttributedTerm (`Raw (text, context), term)
+
 EXTEND
   GLOBAL: term statement;
   arg: [
@@ -358,11 +361,15 @@ EXTEND
       IDENT "for";
       p2 = 
         [ blob = UNPARSED_AST ->
-            CicNotationParser.parse_level2_ast (Stream.of_string blob)
+            add_raw_attribute ~context:`Ast ~text:blob
+              (CicNotationParser.parse_level2_ast (Stream.of_string blob))
         | blob = UNPARSED_META ->
-            CicNotationParser.parse_level2_meta (Stream.of_string blob) ]
-      ->
-        (CicNotationParser.parse_level1_pattern (Stream.of_string s), assoc, prec, p2)
+            add_raw_attribute ~context:`Meta ~text:blob
+              (CicNotationParser.parse_level2_meta (Stream.of_string blob))
+        ] ->
+          (add_raw_attribute ~text:s
+            (CicNotationParser.parse_level1_pattern (Stream.of_string s)),
+           assoc, prec, p2)
     ]
   ];
   level3_term: [