handled difference associativity for the same level of the extensible grammar

[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 984635ec60cc44433df2b847ee3f877f1ff9edc6..908ad007f79cc5fd8a863c09e7dfe84e9f0c9a7f 100644 (file)
--- a/helm/ocaml/cic_notation/grafiteParser.ml
+++ b/helm/ocaml/cic_notation/grafiteParser.ml
@@ -30,8 +30,10 @@ 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)
+let add_raw_attribute ~text t = CicNotationPt.AttributedTerm (`Raw text, t)
+
+let default_precedence = 50
+let default_associativity = Gramext.NonA
 
 EXTEND
   GLOBAL: term statement;
@@ -361,12 +363,22 @@ EXTEND
       IDENT "for";
       p2 = 
         [ blob = UNPARSED_AST ->
-            add_raw_attribute ~context:`Ast ~text:blob
+            add_raw_attribute ~text:(sprintf "@{%s}" blob)
               (CicNotationParser.parse_level2_ast (Stream.of_string blob))
         | blob = UNPARSED_META ->
-            add_raw_attribute ~context:`Meta ~text:blob
+            add_raw_attribute ~text:(sprintf "${%s}" blob)
               (CicNotationParser.parse_level2_meta (Stream.of_string blob))
         ] ->
+          let assoc =
+            match assoc with
+            | None -> default_associativity
+            | Some assoc -> assoc
+          in
+          let prec =
+            match prec with
+            | None -> default_precedence
+            | Some prec -> prec
+          in
           (add_raw_attribute ~text:s
             (CicNotationParser.parse_level1_pattern (Stream.of_string s)),
            assoc, prec, p2)