| Ast.Box (_, pl) -> List.flatten (List.map aux pl)
| Ast.Group pl -> List.flatten (List.map aux pl)
| Ast.Mstyle (_,pl) -> List.flatten (List.map aux pl)
+ | Ast.Mpadded (_,pl) -> List.flatten (List.map aux pl)
+ | Ast.Maction l -> List.flatten (List.map aux l)
and aux_magic magic =
match magic with
| Ast.Opt p ->
type checked_l1_pattern = CL1P of CicNotationPt.term * int
-let check_l1_pattern level1_pattern level associativity =
+let check_l1_pattern level1_pattern pponly level associativity =
let variables = ref 0 in
let symbols = ref 0 in
let rec aux = function
| Ast.Box (b, pl) -> Ast.Box(b, List.map aux pl)
| Ast.Group pl -> Ast.Group (List.map aux pl)
| Ast.Mstyle (l,pl) -> Ast.Mstyle (l, List.map aux pl)
+ | Ast.Mpadded (l,pl) -> Ast.Mpadded (l, List.map aux pl)
+ | Ast.Maction l as t ->
+ if not pponly then
+ raise(Parse_error("Maction can be used only in output notations"))
+ else t
and aux_magic magic =
match magic with
| Ast.Opt p -> Ast.Opt (aux p)
mstyle: [
[ id = IDENT;
v = [ IDENT | NUMBER | COLOR | FLOATWITHUNIT ] -> id, v]];
+ mpadded: [
+ [ id = IDENT;
+ v = [ PERCENTAGE ] -> id, v]];
l1_simple_pattern:
[ "layout" LEFTA
[ p1 = SELF; SYMBOL "\\sub"; p2 = SELF ->
return_term_of_level loc
(fun l ->
Ast.Layout (Ast.Mstyle (m, t l)))
+ | "mpadded"; m = LIST1 mpadded ; LPAREN; t = l1_pattern; RPAREN ->
+ return_term_of_level loc
+ (fun l ->
+ Ast.Layout (Ast.Mpadded (m, t l)))
+ | "maction"; m = LIST1 [ LPAREN; l = l1_pattern; RPAREN -> l ] ->
+ return_term_of_level loc
+ (fun l -> Ast.Layout (Ast.Maction (List.map (fun x ->
+ CicNotationUtil.group (x l)) m)))
| LPAREN; p = l1_pattern; RPAREN ->
return_term_of_level loc (fun l -> CicNotationUtil.group (p l))
]