support for mathml mpadded tag added (allows to overlap two subsequent symbols);...

diff --git a/helm/software/components/acic_content/cicNotationPp.ml b/helm/software/components/acic_content/cicNotationPp.ml
index b92b38656dd3704e58ee97342b6f1f94fbe150dc..4d68dadf9f682e89743593f00bcc0a2322494247 100644 (file)
--- a/helm/software/components/acic_content/cicNotationPp.ml
+++ b/helm/software/components/acic_content/cicNotationPp.ml
@@ -227,6 +227,10 @@ and pp_layout = function
       sprintf "\\MSTYLE %s [%s]" 
         (String.concat " " (List.map (fun (k,v) -> k^"="^v) l))
         (String.concat " " (List.map pp_term terms))
+  | Ast.Mpadded (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 3c96a5a512ac7d1bd49b94ff9ab79cf373b9d0b9..cfbd21b3a7f0c61f48e07e97dcdd8993ec53b6f7 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 = 5
+let magic = 6
 
 type term =
   (* CIC AST *)
@@ -128,6 +128,7 @@ and layout_pattern =
   | Box of box_spec * term list
   | Group of term list
   | Mstyle of (string * string) list * term list
+  | Mpadded 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 5c3936d93b0771d5feb8f52c9dd16327a629c22d..8997a924f46916b3739ac66e9b7dd719573cadaf 100644 (file)
--- a/helm/software/components/acic_content/cicNotationUtil.ml
+++ b/helm/software/components/acic_content/cicNotationUtil.ml
@@ -92,6 +92,7 @@ let visit_layout k = function
   | 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)
+  | Ast.Mpadded (l, term) -> Ast.Mpadded (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 f80821a5f1b6562cb77f7fe55f0bb7d62ffc0d42..11fcc4106d812e643df6f83151657612e8110fbd 100644 (file)
--- a/helm/software/components/content_pres/cicNotationLexer.ml
+++ b/helm/software/components/content_pres/cicNotationLexer.ml
@@ -31,8 +31,10 @@ 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 percentage = 
+  ('-' | "") [ '0' - '9' ] + '%'
 let regexp floatwithunit = 
-  [ '0' - '9' ] + ["."] [ '0' - '9' ] + ([ 'a' - 'z' ] + | "" )
+  ('-' | "") [ '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' ]
@@ -103,7 +105,7 @@ let level1_keywords =
     "break";
     "list0"; "list1"; "sep";
     "opt";
-    "term"; "ident"; "number"; "mstyle"
+    "term"; "ident"; "number"; "mstyle" ; "mpadded"
   ] @ level1_layouts
 
 let level2_meta_keywords =
@@ -346,6 +348,8 @@ and level1_pattern_token =
            return lexbuf ("IDENT", s)
        end
   | color -> return lexbuf ("COLOR", Ulexing.utf8_lexeme lexbuf)
+  | percentage -> 
+      return lexbuf ("PERCENTAGE", Ulexing.utf8_lexeme lexbuf)
   | floatwithunit -> 
       return lexbuf ("FLOATWITHUNIT", Ulexing.utf8_lexeme lexbuf)
   | tex_token -> return lexbuf (expand_macro lexbuf)

diff --git a/helm/software/components/content_pres/cicNotationParser.ml b/helm/software/components/content_pres/cicNotationParser.ml
index cd02c9d36070a011c46911210917e84246b0beb3..60eb41424f23d7e802fb80d09f28f7ef2cee2619 100644 (file)
--- 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))
       ]

diff --git a/helm/software/components/content_pres/cicNotationPres.ml b/helm/software/components/content_pres/cicNotationPres.ml
index 77dc2b08cf8c52ebfcf2fb7f49b8e98f2eaa6903..c4dd944b4b956c65479adc70e7d424ae220638a5 100644 (file)
--- a/helm/software/components/content_pres/cicNotationPres.ml
+++ b/helm/software/components/content_pres/cicNotationPres.ml
@@ -405,6 +405,12 @@ let render ids_to_uris ?(prec=(-1)) =
            box_of mathonly (A.H, false, false) attrs 
             (aux_children mathonly false xref  prec 
               (CicNotationUtil.ungroup terms)))
+    | A.Mpadded (l,terms) -> 
+        Mpres.Mpadded 
+          (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