From: Enrico Tassi Date: Sat, 23 Aug 2008 04:11:04 +0000 (+0000) Subject: notation with mstyle attributes, like colors and size X-Git-Tag: make_still_working~4855 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=3e1e59644a24ed855a7f21bf9eab76f96577fd17;p=helm.git 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 cfd8c8a30..29898eb13 100644 --- 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 ff72f2a86..c76590181 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 = 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 25af9981e..5c3936d93 100644 --- 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 00696cc00..4221417a0 100644 --- 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 21720c01d..f58bd21b5 100644 --- 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 abd7ab041..e6cbbf692 100644 --- 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