X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=inline;f=helm%2Focaml%2Fcic_notation%2FgrafiteParser.ml;h=984635ec60cc44433df2b847ee3f877f1ff9edc6;hb=cd602bc57c4ceba6188b4cac0dbf5dad8f5df7b6;hp=8bd5cc04e3e976c62dcc2f07e4cecbdfc36ec0a7;hpb=e20f3963028a966fc93ba0d611c4aa8341d20e2c;p=helm.git

diff --git a/helm/ocaml/cic_notation/grafiteParser.ml b/helm/ocaml/cic_notation/grafiteParser.ml
index 8bd5cc04e..984635ec6 100644
--- 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: [