X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_notation%2FcicNotationParser.ml;h=ba12b49da15fe86d2c2ceef0baac78d254180e2f;hb=12cc5b2b8e7f7bb0b5e315094b008a293a4df6b1;hp=246417d77339bad0eee9746ed4963d6396cdeffd;hpb=bf6144a808a16d4e576e56593bbcd63b8db5fe4c;p=helm.git

diff --git a/helm/ocaml/cic_notation/cicNotationParser.ml b/helm/ocaml/cic_notation/cicNotationParser.ml
index 246417d77..ba12b49da 100644
--- 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"
@@ -144,7 +154,7 @@ let extract_term_production pattern =
         [NoBinding, symbol "\\ROOT"] @ aux p2 @ [NoBinding, symbol "\\OF"]
         @ aux p1
     | Sqrt p -> [NoBinding, symbol "\\SQRT"] @ aux p
-    | Break -> []
+(*     | Break -> [] *)
     | Box (_, pl) -> List.flatten (List.map aux pl)
   and aux_magic magic =
     match magic with
@@ -244,10 +254,6 @@ let delete atoms = Grammar.delete_rule l2_pattern atoms
 
 (** {2 Grammar} *)
 
-let boxify = function
-  | [ a ] -> a
-  | l -> Layout (Box (H, l))
-
 let fold_binder binder pt_names body =
   let fold_cluster binder terms ty body =
     List.fold_right
@@ -324,12 +330,17 @@ 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)))
-      | SYMBOL "\\BREAK" -> return_term loc (Layout Break)
+          return_term loc (Layout (Box ((V, false, false), p)))
+      | SYMBOL "\\HVBOX"; DELIM "\\["; p = l1_pattern; DELIM "\\]" ->
+          return_term loc (Layout (Box ((HV, false, false), p)))
+      | SYMBOL "\\HOVBOX"; DELIM "\\["; p = l1_pattern; DELIM "\\]" ->
+          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 (boxify p)
+          return_term loc (CicNotationUtil.boxify p)
       | p = SELF; SYMBOL "\\AS"; id = IDENT ->
           return_term loc (Variable (Ascription (p, id)))
       ]