X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fcontent_pres%2FcicNotationParser.ml;h=60eb41424f23d7e802fb80d09f28f7ef2cee2619;hb=5c30190ffa401334eb2fa9fab0be7db0de26a458;hp=e3e54f112a5730608644d65f28b6135df444f250;hpb=01001c883a8151edba81cd03a6f254d24a81c867;p=helm.git

diff --git a/helm/software/components/content_pres/cicNotationParser.ml b/helm/software/components/content_pres/cicNotationParser.ml
index e3e54f112..60eb41424 100644
--- a/helm/software/components/content_pres/cicNotationParser.ml
+++ b/helm/software/components/content_pres/cicNotationParser.ml
@@ -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))
       ]
@@ -563,6 +572,7 @@ EXTEND
   sort: [
     [ "Prop" -> `Prop
     | "Set" -> `Set
+    | "Type"; SYMBOL "["; n = NUMBER; SYMBOL "]" -> `NType n 
     | "Type" -> `Type (CicUniv.fresh ()) 
     | "CProp" -> `CProp (CicUniv.fresh ())
     ]