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"
| 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 ->