snapshot

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

diff --git a/helm/ocaml/cic_notation/cicNotationParser.ml b/helm/ocaml/cic_notation/cicNotationParser.ml
index 681dfd5e50b83b0369445b7e75280ad35620e38f..4dcc772975b9e28287d3840b90bd640de4a067cf 100644 (file)
--- a/helm/ocaml/cic_notation/cicNotationParser.ml
+++ b/helm/ocaml/cic_notation/cicNotationParser.ml
@@ -37,6 +37,16 @@ let min_precedence = 0
 let max_precedence = 100
 let default_precedence = 50
 
+let let_in_prec = 10
+let binder_prec = 20
+let apply_prec = 70
+let simple_prec = 90
+
+let let_in_assoc = Gramext.NonA
+let binder_assoc = Gramext.RightA
+let apply_assoc = Gramext.LeftA
+let simple_assoc = Gramext.NonA
+
 let level1_pattern = Grammar.Entry.create grammar "level1_pattern"
 let level2_pattern = Grammar.Entry.create grammar "level2_pattern"
 let level3_term = Grammar.Entry.create grammar "level3_term"
@@ -320,14 +330,15 @@ EXTEND
       | SYMBOL "\\ROOT"; index = SELF; SYMBOL "\\OF"; arg = SELF ->
           return_term loc (Layout (Root (arg, index)));
       | SYMBOL "\\HBOX"; DELIM "\\["; p = l1_pattern; DELIM "\\]" ->
-          return_term loc (Layout (Box (H, p)))
+          return_term loc (Layout (Box ((H, false, false), p)))
       | SYMBOL "\\VBOX"; DELIM "\\["; p = l1_pattern; DELIM "\\]" ->
-          return_term loc (Layout (Box (V, p)))
+          return_term loc (Layout (Box ((V, false, false), p)))
       | SYMBOL "\\HVBOX"; DELIM "\\["; p = l1_pattern; DELIM "\\]" ->
-          return_term loc (Layout (Box (HV, p)))
+          return_term loc (Layout (Box ((HV, false, false), p)))
       | SYMBOL "\\HOVBOX"; DELIM "\\["; p = l1_pattern; DELIM "\\]" ->
-          return_term loc (Layout (Box (HOV, p)))
+          return_term loc (Layout (Box ((HOV, false, false), p)))
 (*       | SYMBOL "\\BREAK" -> return_term loc (Layout Break) *)
+(*       | SYMBOL "\\SPACE" -> return_term loc (Layout Space) *)
       | DELIM "\\["; p = l1_pattern; DELIM "\\]" ->
           return_term loc (CicNotationUtil.boxify p)
       | p = SELF; SYMBOL "\\AS"; id = IDENT ->
@@ -532,7 +543,7 @@ EXTEND
     ]
   ];
   level3_term: [
-    [ u = URI -> UriPattern u
+    [ u = URI -> UriPattern (UriManager.uri_of_string u)
     | id = IDENT -> VarPattern id
     | SYMBOL "("; terms = LIST1 SELF; SYMBOL ")" ->
         (match terms with