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

diff --git a/helm/software/components/content_pres/cicNotationParser.ml b/helm/software/components/content_pres/cicNotationParser.ml
index aca53578b..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))
       ]
@@ -550,7 +570,6 @@ EXTEND
   ];
   binder: [
     [ SYMBOL <:unicode<Pi>>     (* Π *) -> `Pi
-(*     | SYMBOL <:unicode<exists>> |+ ∃ +| -> `Exists *)
     | SYMBOL <:unicode<forall>> (* ∀ *) -> `Forall
     | SYMBOL <:unicode<lambda>> (* λ *) -> `Lambda
     ]
@@ -649,9 +668,6 @@ EXTEND
     [
       [ b = binder; (vars, typ) = maybe_protected_binder_vars; SYMBOL "."; body = term LEVEL "19" ->
           return_term loc (fold_cluster b vars typ body)
-      | SYMBOL <:unicode<exists>> (* ∃ *);
-        (vars, typ) = maybe_protected_binder_vars; SYMBOL "."; body = term LEVEL "19"->
-          return_term loc (fold_exists vars typ body)
       ]
     ];
   term: LEVEL "70"