From: Enrico Tassi Date: Thu, 11 Dec 2008 14:16:47 +0000 (+0000) Subject: support for mathml mpadded tag added (allows to overlap two subsequent symbols);... X-Git-Tag: make_still_working~4420 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=be73a507f4f3c1b40a77dd7fc587adaf45b4d8ea;p=helm.git support for mathml mpadded tag added (allows to overlap two subsequent symbols); you library needs to be recompiled after the update --- diff --git a/helm/software/components/acic_content/cicNotationPp.ml b/helm/software/components/acic_content/cicNotationPp.ml index b92b38656..4d68dadf9 100644 --- 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 3c96a5a51..cfbd21b3a 100644 --- 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 5c3936d93..8997a924f 100644 --- 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 f80821a5f..11fcc4106 100644 --- 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 cd02c9d36..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)) ] diff --git a/helm/software/components/content_pres/cicNotationPres.ml b/helm/software/components/content_pres/cicNotationPres.ml index 77dc2b08c..c4dd944b4 100644 --- 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