X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fcontent_pres%2FcicNotationParser.ml;h=859697cd632ecf08c3b2f3d6debd5155f5e3e4eb;hb=2a5fa3d7b64f23c060a2e6a2a4b87c6f277ddfae;hp=d7da2ff822d27f46a817820a11db23caf6ccd888;hpb=6f64f2bbba6d5488cc36b8e2f5a717e866a3015d;p=helm.git

diff --git a/helm/software/components/content_pres/cicNotationParser.ml b/helm/software/components/content_pres/cicNotationParser.ml
index d7da2ff82..859697cd6 100644
--- a/helm/software/components/content_pres/cicNotationParser.ml
+++ b/helm/software/components/content_pres/cicNotationParser.ml
@@ -150,7 +150,7 @@ let extract_term_production pattern =
     | Ast.Below (p1, p2) -> aux p1 @ [NoBinding, gram_symbol "\\below"] @ aux p2
     | Ast.Above (p1, p2) -> aux p1 @ [NoBinding, gram_symbol "\\above"] @ aux p2
     | Ast.Frac (p1, p2) -> aux p1 @ [NoBinding, gram_symbol "\\frac"] @ aux p2
-    | Ast.InfRule (p1, p2, p3) -> aux p1 @ [NoBinding, gram_symbol "\\infrule"] @ aux p2 @ aux p3
+    | Ast.InfRule (p1, p2, p3) -> [NoBinding, gram_symbol "\\infrule"] @ aux p1 @ aux p2 @ aux p3
     | Ast.Atop (p1, p2) -> aux p1 @ [NoBinding, gram_symbol "\\atop"] @ aux p2
     | Ast.Over (p1, p2) -> aux p1 @ [NoBinding, gram_symbol "\\over"] @ aux p2
     | Ast.Root (p1, p2) ->
@@ -160,6 +160,7 @@ let extract_term_production pattern =
     | Ast.Break -> []
     | 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)
   and aux_magic magic =
     match magic with
     | Ast.Opt p ->
@@ -213,6 +214,17 @@ let extract_term_production pattern =
 
 type rule_id = Grammar.token Gramext.g_symbol list
 
+let compare_rule_id x y =
+  let rec aux = function
+    | [],[] -> 0
+    | [],_ -> ~-1
+    | _,[] -> 1
+    | ((s1::tl1) as x),((s2::tl2) as y) ->
+        if Gramext.eq_symbol s1 s2 then aux (tl1,tl2)
+        else Pervasives.compare x y 
+  in
+    aux (x,y)
+
   (* mapping: rule_id -> owned keywords. (rule_id, string list) Hashtbl.t *)
 let owned_keywords = Hashtbl.create 23
 
@@ -242,6 +254,7 @@ let check_l1_pattern level1_pattern level associativity =
     | Ast.Break as t -> t 
     | 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)
   and aux_magic magic =
     match magic with
     | Ast.Opt p -> Ast.Opt (aux p)
@@ -405,6 +418,9 @@ EXTEND
     | "ident"; id = IDENT -> Ast.IdentVar id
     ]
   ];
+  mstyle: [ 
+    [ id = IDENT; 
+      v = [ IDENT | NUMBER | COLOR | FLOATWITHUNIT ] -> id, v]];
   l1_simple_pattern:
     [ "layout" LEFTA
       [ p1 = SELF; SYMBOL "\\sub"; p2 = SELF ->
@@ -425,7 +441,7 @@ EXTEND
       | p1 = SELF; SYMBOL "\\atop"; p2 = SELF ->
           return_term_of_level loc 
             (fun l -> Ast.Layout (Ast.Atop (p1 l, p2 l)))
-      | SYMBOL "\\frac"; p1 = SELF; p2 = SELF ->
+      | p1 = SELF; SYMBOL "\\frac"; p2 = SELF ->
           return_term_of_level loc 
             (fun l -> Ast.Layout (Ast.Frac (p1 l, p2 l)))
       | SYMBOL "\\infrule"; p1 = SELF; p2 = SELF; p3 = SELF ->
@@ -449,6 +465,10 @@ EXTEND
           return_term_of_level loc 
             (fun l -> Ast.Layout (Ast.Box ((Ast.HOV, false, false), p l)))
       | "break" -> return_term_of_level loc (fun _ -> Ast.Layout Ast.Break)
+      | "mstyle"; m = LIST1 mstyle ; LPAREN; t = l1_pattern; RPAREN ->
+          return_term_of_level loc 
+            (fun l -> 
+               Ast.Layout (Ast.Mstyle (m, t l)))
       | LPAREN; p = l1_pattern; RPAREN ->
           return_term_of_level loc (fun l -> CicNotationUtil.group (p l))
       ]