]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/software/components/content_pres/cicNotationParser.ml
support for mathml mpadded tag added (allows to overlap two subsequent symbols);...
[helm.git] / helm / software / components / content_pres / cicNotationParser.ml
index cd02c9d36070a011c46911210917e84246b0beb3..60eb41424f23d7e802fb80d09f28f7ef2cee2619 100644 (file)
@@ -186,6 +186,7 @@ let extract_term_production pattern =
     | 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)
   and aux_magic magic =
     match magic with
     | Ast.Opt p ->
@@ -281,6 +282,7 @@ let check_l1_pattern level1_pattern level associativity =
     | 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)
   and aux_magic magic =
     match magic with
     | Ast.Opt p -> Ast.Opt (aux p)
@@ -448,6 +450,9 @@ EXTEND
   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 ->
@@ -496,6 +501,10 @@ EXTEND
           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)))
       | LPAREN; p = l1_pattern; RPAREN ->
           return_term_of_level loc (fun l -> CicNotationUtil.group (p l))
       ]