notation with mstyle attributes, like colors and size

diff --git a/helm/software/components/acic_content/cicNotationPp.ml b/helm/software/components/acic_content/cicNotationPp.ml
index cfd8c8a308956cdef0466d57f5adc231c85e36ab..29898eb13ace83196d7340d8f10ff653dc170cc6 100644 (file)
--- a/helm/software/components/acic_content/cicNotationPp.ml
+++ b/helm/software/components/acic_content/cicNotationPp.ml
@@ -222,6 +222,10 @@ and pp_layout = function
         (String.concat " " (List.map pp_term terms))
   | Ast.Group terms ->
       sprintf "\\GROUP [%s]" (String.concat " " (List.map pp_term terms))
+  | Ast.Mstyle (l,terms) -> 
+      sprintf "\\MSTYLE %s [%s]" 
+        (String.concat " " (List.map (fun (k,v) -> k^"="^v) l))
+        (String.concat " " (List.map pp_term terms))
 
 and pp_magic = function
   | Ast.List0 (t, sep_opt) ->

diff --git a/helm/software/components/acic_content/cicNotationPt.ml b/helm/software/components/acic_content/cicNotationPt.ml
index ff72f2a86c9722cac3d24e2e8f17614c05af74a3..c7659018127aed95d660f9a23d9a5dd19674336a 100644 (file)
--- a/helm/software/components/acic_content/cicNotationPt.ml
+++ b/helm/software/components/acic_content/cicNotationPt.ml
@@ -62,7 +62,7 @@ type 'term capture_variable = 'term * 'term option
 
 (** To be increased each time the term type below changes, used for "safe"
  * marshalling *)
-let magic = 4
+let magic = 5
 
 type term =
   (* CIC AST *)
@@ -127,6 +127,7 @@ and layout_pattern =
   | Break
   | Box of box_spec * term list
   | Group of term list
+  | Mstyle of (string * string) list * term list
 
 and magic_term =
   (* level 1 magics *)

diff --git a/helm/software/components/acic_content/cicNotationUtil.ml b/helm/software/components/acic_content/cicNotationUtil.ml
index 25af9981e7f5dff7131aba171dfdcf1fb5dadf8e..5c3936d93b0771d5feb8f52c9dd16327a629c22d 100644 (file)
--- a/helm/software/components/acic_content/cicNotationUtil.ml
+++ b/helm/software/components/acic_content/cicNotationUtil.ml
@@ -91,6 +91,7 @@ let visit_layout k = function
   | Ast.Break -> Ast.Break
   | Ast.Box (kind, terms) -> Ast.Box (kind, List.map k terms)
   | Ast.Group terms -> Ast.Group (List.map k terms)
+  | Ast.Mstyle (l, term) -> Ast.Mstyle (l, List.map k term)
 
 let visit_magic k = function
   | Ast.List0 (t, l) -> Ast.List0 (k t, l)

diff --git a/helm/software/components/content_pres/cicNotationLexer.ml b/helm/software/components/content_pres/cicNotationLexer.ml
index 00696cc00d2cec8b36e4a3a4a1c8d45000331a52..4221417a0183dbf19a2e54cf140a802fdaad9ba4 100644 (file)
--- a/helm/software/components/content_pres/cicNotationLexer.ml
+++ b/helm/software/components/content_pres/cicNotationLexer.ml
@@ -31,6 +31,11 @@ exception Error of int * int * string
 
 let regexp number = xml_digit+
 let regexp utf8_blank = " " | "\r\n" | "\n" | "\t" | [160] (* this is a nbsp *)
+let regexp floatwithunit = 
+  [ '0' - '9' ] + ["."] [ '0' - '9' ] + ([ 'a' - 'z' ] + | "" )
+let regexp color = "#" [ '0' - '9' 'a' - 'f' 'A' - 'F' ] [ '0' - '9' 'a' - 'f'
+'A' - 'F' ] [ '0' - '9' 'a' - 'f' 'A' - 'F' ] [ '0' - '9' 'a' - 'f' 'A' - 'F' ]
+[ '0' - '9' 'a' - 'f' 'A' - 'F' ] [ '0' - '9' 'a' - 'f' 'A' - 'F' ]
 
   (* ZACK: breaks unicode's binder followed by an ascii letter without blank *)
 (* let regexp ident_letter = xml_letter *)
@@ -98,7 +103,7 @@ let level1_keywords =
     "break";
     "list0"; "list1"; "sep";
     "opt";
-    "term"; "ident"; "number"
+    "term"; "ident"; "number"; "mstyle"
   ] @ level1_layouts
 
 let level2_meta_keywords =
@@ -333,6 +338,9 @@ and level1_pattern_token =
          else
            return lexbuf ("IDENT", s)
        end
+  | color -> return lexbuf ("COLOR", Ulexing.utf8_lexeme lexbuf)
+  | floatwithunit -> 
+      return lexbuf ("FLOATWITHUNIT", Ulexing.utf8_lexeme lexbuf)
   | tex_token -> return lexbuf (expand_macro lexbuf)
   | qkeyword ->
       return lexbuf ("QKEYWORD", remove_quotes (Ulexing.utf8_lexeme lexbuf))

diff --git a/helm/software/components/content_pres/cicNotationParser.ml b/helm/software/components/content_pres/cicNotationParser.ml
index 21720c01d5b40a3f41a9b3369fce8f335211b615..f58bd21b59b460295d196e3a095f626ac8298e48 100644 (file)
--- a/helm/software/components/content_pres/cicNotationParser.ml
+++ b/helm/software/components/content_pres/cicNotationParser.ml
@@ -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 ->
@@ -242,6 +243,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 +407,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 ->
@@ -449,6 +454,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))
       ]

diff --git a/helm/software/components/content_pres/cicNotationPres.ml b/helm/software/components/content_pres/cicNotationPres.ml
index abd7ab0410b628de77835376ea2186c2136a73e1..e6cbbf692be37411ab8c1ee8c1f10e465179cae6 100644 (file)
--- a/helm/software/components/content_pres/cicNotationPres.ml
+++ b/helm/software/components/content_pres/cicNotationPres.ml
@@ -344,7 +344,7 @@ let render ids_to_uris ?(prec=(-1)) =
             | Some prec -> prec
           in
           (match !inferred_level with
-          | None -> aux !new_xmlattrs mathonly new_xref prec t 
+          | None -> aux !new_xmlattrs mathonly new_xref prec t
           | Some child_prec ->
               let t' = aux !new_xmlattrs mathonly new_xref child_prec t in
               (*prerr_endline 
@@ -399,6 +399,12 @@ let render ids_to_uris ?(prec=(-1)) =
             (CicNotationUtil.ungroup terms)
         in
         box_of mathonly kind attrs children
+    | A.Mstyle (l,terms) -> 
+        Mpres.Mstyle 
+          (List.map (fun (k,v) -> None,k,v) l, 
+           box_of mathonly (A.H, false, false) attrs 
+            (aux_children mathonly false xref  prec 
+              (CicNotationUtil.ungroup terms)))
     | A.Group terms ->
        let children =
           aux_children mathonly false xref  prec