From: Andrea Asperti Date: Fri, 20 May 2011 08:42:04 +0000 (+0000) Subject: Simplified rendering X-Git-Tag: make_still_working~2509 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=d206219b4b193feeebaa25bea70bc8ec153777e5;p=helm.git Simplified rendering --- diff --git a/matitaB/components/content_pres/.depend b/matitaB/components/content_pres/.depend index f519ea34f..dcc30c6ee 100644 --- a/matitaB/components/content_pres/.depend +++ b/matitaB/components/content_pres/.depend @@ -1,44 +1,26 @@ -renderingAttrs.cmi: cicNotationLexer.cmi: -interpTable.cmi: smallLexer.cmi: cicNotationParser.cmi: -mpresentation.cmi: box.cmi: -content2presMatcher.cmi: termContentPres.cmi: cicNotationParser.cmi -boxPp.cmi: mpresentation.cmi cicNotationPres.cmi box.cmi -cicNotationPres.cmi: mpresentation.cmi box.cmi -content2pres.cmi: termContentPres.cmi cicNotationPres.cmi -renderingAttrs.cmo: renderingAttrs.cmi -renderingAttrs.cmx: renderingAttrs.cmi +boxPp.cmi: cicNotationPres.cmi +cicNotationPres.cmi: termContentPres.cmi box.cmi +content2presMatcher.cmi: cicNotationLexer.cmo: cicNotationLexer.cmi cicNotationLexer.cmx: cicNotationLexer.cmi -interpTable.cmo: interpTable.cmi -interpTable.cmx: interpTable.cmi smallLexer.cmo: smallLexer.cmi smallLexer.cmx: smallLexer.cmi cicNotationParser.cmo: cicNotationLexer.cmi cicNotationParser.cmi cicNotationParser.cmx: cicNotationLexer.cmx cicNotationParser.cmi -mpresentation.cmo: mpresentation.cmi -mpresentation.cmx: mpresentation.cmi box.cmo: renderingAttrs.cmi box.cmi box.cmx: renderingAttrs.cmx box.cmi -content2presMatcher.cmo: content2presMatcher.cmi -content2presMatcher.cmx: content2presMatcher.cmi termContentPres.cmo: renderingAttrs.cmi content2presMatcher.cmi \ cicNotationParser.cmi termContentPres.cmi termContentPres.cmx: renderingAttrs.cmx content2presMatcher.cmx \ cicNotationParser.cmx termContentPres.cmi -boxPp.cmo: renderingAttrs.cmi mpresentation.cmi cicNotationPres.cmi box.cmi \ - boxPp.cmi -boxPp.cmx: renderingAttrs.cmx mpresentation.cmx cicNotationPres.cmx box.cmx \ - boxPp.cmi -cicNotationPres.cmo: renderingAttrs.cmi mpresentation.cmi box.cmi \ - cicNotationPres.cmi -cicNotationPres.cmx: renderingAttrs.cmx mpresentation.cmx box.cmx \ - cicNotationPres.cmi -content2pres.cmo: termContentPres.cmi renderingAttrs.cmi mpresentation.cmi \ - cicNotationPres.cmi box.cmi content2pres.cmi -content2pres.cmx: termContentPres.cmx renderingAttrs.cmx mpresentation.cmx \ - cicNotationPres.cmx box.cmx content2pres.cmi +boxPp.cmo: renderingAttrs.cmi box.cmi boxPp.cmi +boxPp.cmx: renderingAttrs.cmx box.cmx boxPp.cmi +cicNotationPres.cmo: termContentPres.cmi box.cmi cicNotationPres.cmi +cicNotationPres.cmx: termContentPres.cmx box.cmx cicNotationPres.cmi +content2presMatcher.cmo: content2presMatcher.cmi +content2presMatcher.cmx: content2presMatcher.cmi diff --git a/matitaB/components/content_pres/Makefile b/matitaB/components/content_pres/Makefile index 084940b4d..658d8d354 100644 --- a/matitaB/components/content_pres/Makefile +++ b/matitaB/components/content_pres/Makefile @@ -2,26 +2,22 @@ PACKAGE = content_pres PREDICATES = INTERFACE_FILES = \ - renderingAttrs.mli \ cicNotationLexer.mli \ - interpTable.mli \ smallLexer.mli \ cicNotationParser.mli \ - mpresentation.mli \ box.mli \ - content2presMatcher.mli \ termContentPres.mli \ boxPp.mli \ cicNotationPres.mli \ - content2pres.mli \ + content2presMatcher.mli \ $(NULL) IMPLEMENTATION_FILES = \ $(INTERFACE_FILES:%.mli=%.ml) \ PKGS = -package "$(MATITA_REQUIRES)" -CMOS = $(ML:%.ml=%.cmo) -$(CMOS) : $(LIB_DEPS) +#CMOS = $(ML:%.ml=%.cmo) +#$(CMOS) : $(LIB_DEPS) cicNotationPres.cmi: OCAMLOPTIONS += -rectypes cicNotationPres.cmo: OCAMLOPTIONS += -rectypes diff --git a/matitaB/components/content_pres/box.ml b/matitaB/components/content_pres/box.ml index 7c5069262..6e5bb4d92 100644 --- a/matitaB/components/content_pres/box.ml +++ b/matitaB/components/content_pres/box.ml @@ -23,15 +23,6 @@ * http://cs.unibo.it/helm/. *) -(*************************************************************************) -(* *) -(* PROJECT HELM *) -(* *) -(* Andrea Asperti *) -(* 13/2/2004 *) -(* *) -(*************************************************************************) - (* $Id$ *) type diff --git a/matitaB/components/content_pres/box.mli b/matitaB/components/content_pres/box.mli index d2ca17bdd..e7c2588eb 100644 --- a/matitaB/components/content_pres/box.mli +++ b/matitaB/components/content_pres/box.mli @@ -23,15 +23,6 @@ * http://cs.unibo.it/helm/. *) -(*************************************************************************) -(* *) -(* PROJECT HELM *) -(* *) -(* Andrea Asperti *) -(* 13/2/2004 *) -(* *) -(*************************************************************************) - type 'expr box = Text of attr * string diff --git a/matitaB/components/content_pres/boxPp.ml b/matitaB/components/content_pres/boxPp.ml index 45c8b6c20..7f71aa20b 100644 --- a/matitaB/components/content_pres/boxPp.ml +++ b/matitaB/components/content_pres/boxPp.ml @@ -25,7 +25,6 @@ (* $Id$ *) -module Pres = Mpresentation (** {2 Pretty printing from BoxML to strings} *) @@ -33,8 +32,8 @@ let utf8_string_length s = Utf8.compute_len s 0 (String.length s) let string_space = " " let string_space_len = utf8_string_length string_space -let string_indent = (* string_space *) [],"" -let string_indent_len = utf8_string_length (snd string_indent) +let string_indent = (* string_space *) "" +let string_indent_len = utf8_string_length string_indent let string_ink = "---------------------------" let string_ink_len = utf8_string_length string_ink @@ -46,24 +45,8 @@ let want_spacing = contains_attrs (RenderingAttrs.spacing_attributes `BoxML) let shift off = List.map (fun (start,stop,v) -> start+off,stop+off,v);; -let (^^) (map1,s1) (map2,s2) = map1 @ (shift (utf8_string_length s1) map2), s1 ^ s2;; +let indent_string s = string_indent ^ s -(* CSC: inefficient (quadratic) implementation *) -let mapped_string_concat sep = - let sep_len = utf8_string_length sep in - let rec aux off = - function - [] -> [],"" - | [map,s] -> shift off map,s - | (map,s)::tl -> - let map = shift off map in - let map2,s2 = aux (off + utf8_string_length s + sep_len) tl in - map@map2, s ^ sep ^ s2 - in - aux 0 -;; - -let indent_string s = string_indent ^^ s let indent_children (size, children) = let children' = List.map indent_string children in size + string_space_len, children' @@ -82,9 +65,9 @@ let merge_columns sep cols = let add_row ~continue row = match !res_rows with | last :: prev when continue -> - res_rows := (last ^^ ([],sep) ^^ row) :: prev; - indent := !indent + utf8_string_length (snd last) + sep_len - | _ -> res_rows := (([],String.make !indent ' ') ^^ row) :: !res_rows; + res_rows := (last ^ sep ^ row) :: prev; + indent := !indent + utf8_string_length last + sep_len + | _ -> res_rows := ((String.make !indent ' ') ^ row) :: !res_rows; in List.iter (fun rows -> @@ -97,7 +80,7 @@ let merge_columns sep cols = List.rev !res_rows let max_len = - List.fold_left (fun max_size (_,s) -> max (utf8_string_length s) max_size) 0 + List.fold_left (fun max_size s -> max (utf8_string_length s) max_size) 0 let render_row available_space spacing children = let spacing_bonus = if spacing then string_space_len else 0 in @@ -113,21 +96,20 @@ let render_row available_space spacing children = let rendering = merge_columns sep (List.rev !renderings) in max_len rendering, rendering -let fixed_rendering href s = +let fixed_rendering s = let s_len = utf8_string_length s in - let map = match href with None -> [] | Some href -> [0,s_len-1,href] in - (fun _ -> s_len, [map,s]) + fun _ -> s_len,[s] let render_to_strings ~map_unicode_to_tex choose_action size markup = let max_size = max_int in let rec aux_box = function - | Box.Text (_, t) -> fixed_rendering None t - | Box.Space _ -> fixed_rendering None string_space - | Box.Ink _ -> fixed_rendering None string_ink + | Box.Text (_, t) -> fixed_rendering t + | Box.Space _ -> fixed_rendering string_space + | Box.Ink _ -> fixed_rendering string_ink | Box.Action (_, []) -> assert false | Box.Action (_, l) -> aux_box (choose_action l) - | Box.Object (_, o) -> aux_mpres o + | Box.Object (_, o) -> fixed_rendering o | Box.H (attrs, children) -> let spacing = want_spacing attrs in let children' = List.map aux_box children in @@ -150,7 +132,7 @@ let render_to_strings ~map_unicode_to_tex choose_action size markup = let hd_f = aux_box hd in let tl_fs = List.map aux_box tl in (fun size -> - let _, hd_rendering = hd_f size in + let hd_rendering = snd (hd_f size) in let children_size = max 0 (if indent then size - string_indent_len else size) in @@ -207,74 +189,9 @@ let render_to_strings ~map_unicode_to_tex choose_action size markup = fs; if !renderings <> [] then end_cluster (); max_len !rows, List.rev !rows) - and aux_mpres = - let text s = Pres.Mtext ([], s) in - let mrow c = Pres.Mrow ([], c) in - let parentesize s = s in - function x -> - let attrs = Pres.get_attr x in - let href = - try - let _,_,href = - List.find (fun (ns,na,value) -> ns = Some "xlink" && na = "href") attrs - in - Some href - with Not_found -> None in - match x with - | Pres.Mi (_, s) - | Pres.Mn (_, s) - | Pres.Mtext (_, s) - | Pres.Ms (_, s) - | Pres.Mgliph (_, s) -> fixed_rendering href s - | Pres.Mo (_, s) -> - let s = - if map_unicode_to_tex then begin - if utf8_string_length s = 1 && Char.code s.[0] < 128 then - s - else - match Utf8Macro.tex_of_unicode s with - | s::_ -> s ^ " " - | [] -> " " ^ s ^ " " - end else - s - in - fixed_rendering href s - | Pres.Mspace _ -> fixed_rendering href string_space - | Pres.Mrow (attrs, children) -> - let children' = List.map aux_mpres children in - (fun size -> render_row size false children') - | Pres.Mfrac (_, m, n) -> - aux_mpres (mrow [ text " \\frac "; parentesize m ; text " "; parentesize n; text " " ]) - | Pres.Msqrt (_, m) -> aux_mpres (mrow [ text " \\sqrt "; parentesize m; text " "]) - | Pres.Mroot (_, r, i) -> - aux_mpres (mrow [ - text " \\root "; parentesize i; text " \\of "; parentesize r; text " " ]) - | Pres.Mstyle (_, m) - | Pres.Merror (_, m) - | Pres.Mpadded (_, m) - | Pres.Mphantom (_, m) - | Pres.Menclose (_, m) -> aux_mpres m - | Pres.Mfenced (_, children) -> aux_mpres (mrow children) - | Pres.Maction (_, []) -> assert false - | Pres.Msub (_, m, n) -> - aux_mpres (mrow [ text " "; parentesize m; text " \\sub "; parentesize n; text " " ]) - | Pres.Msup (_, m, n) -> - aux_mpres (mrow [ text " "; parentesize m; text " \\sup "; parentesize n; text " " ]) - | Pres.Munder (_, m, n) -> - aux_mpres (mrow [ text " "; parentesize m; text " \\below "; parentesize n; text " " ]) - | Pres.Mover (_, m, n) -> - aux_mpres (mrow [ text " "; parentesize m; text " \\above "; parentesize n; text " " ]) - | Pres.Msubsup _ - | Pres.Munderover _ - | Pres.Mtable _ -> - prerr_endline - "MathML presentation element not yet available in concrete syntax"; - assert false - | Pres.Maction (_, hd :: _) -> aux_mpres hd - | Pres.Mobject (_, o) -> aux_box (o: CicNotationPres.boxml_markup) in - snd (aux_mpres markup size) + snd (aux_box markup size) let render_to_string ~map_unicode_to_tex choose_action size markup = - mapped_string_concat "\n" + String.concat "\n" (render_to_strings ~map_unicode_to_tex choose_action size markup) diff --git a/matitaB/components/content_pres/boxPp.mli b/matitaB/components/content_pres/boxPp.mli index c4d6fd53b..32e31e848 100644 --- a/matitaB/components/content_pres/boxPp.mli +++ b/matitaB/components/content_pres/boxPp.mli @@ -27,11 +27,11 @@ * @param map_unicode_to_tex if true converts multibye unicode sequences to * TeX-like macros (when possible). Default: true * @param size - * @returns hyperlinks and text + * @returns text *) + val render_to_string: map_unicode_to_tex:bool -> - (CicNotationPres.boxml_markup Mpresentation.mpres Box.box list -> CicNotationPres.boxml_markup) -> - int -> CicNotationPres.markup -> - (int * int * string) list * string + (CicNotationPres.markup list -> CicNotationPres.markup) -> + int -> CicNotationPres.markup -> string diff --git a/matitaB/components/content_pres/cicNotationPres.ml b/matitaB/components/content_pres/cicNotationPres.ml index 305fe5794..563af0b06 100644 --- a/matitaB/components/content_pres/cicNotationPres.ml +++ b/matitaB/components/content_pres/cicNotationPres.ml @@ -23,129 +23,20 @@ * http://helm.cs.unibo.it/ *) -(* $Id$ *) - open Printf -module Ast = NotationPt -module Mpres = Mpresentation - -type mathml_markup = boxml_markup Mpres.mpres -and boxml_markup = mathml_markup Box.box - -type markup = mathml_markup +module A = NotationPt -let atop_attributes = [None, "linethickness", "0pt"] +type markup = string Box.box let to_unicode = Utf8Macro.unicode_of_tex -let rec make_attributes l1 = function - | [] -> [] - | hd :: tl -> - (match hd with - | None -> make_attributes (List.tl l1) tl - | Some s -> - let p,n = List.hd l1 in - (p,n,s) :: make_attributes (List.tl l1) tl) - -let box_of_mpres = - function - | Mpresentation.Mobject (attrs, box) -> - assert (attrs = []); - box - | mpres -> Box.Object ([], mpres) - -let mpres_of_box = - function - | Box.Object (attrs, mpres) -> - assert (attrs = []); - mpres - | box -> Mpresentation.Mobject ([], box) - -let rec genuine_math = - function - | Mpresentation.Mobject ([], obj) -> not (genuine_box obj) - | _ -> true -and genuine_box = - function - | Box.Object ([], mpres) -> not (genuine_math mpres) - | _ -> true - -let rec eligible_math = - function - | Mpresentation.Mobject ([], Box.Object ([], mpres)) -> eligible_math mpres - | Mpresentation.Mobject ([], _) -> false - | _ -> true - -let rec promote_to_math = - function - | Mpresentation.Mobject ([], Box.Object ([], mpres)) -> promote_to_math mpres - | math -> math - -let small_skip = - Mpresentation.Mspace (RenderingAttrs.small_skip_attributes `MathML) +let open_paren = Box.Text ([], "(") +let closed_paren = Box.Text ([], ")") +let semicolon = Box.Text ([], ";") -let rec add_mpres_attributes new_attr = function - | Mpresentation.Mobject (attr, box) -> - Mpresentation.Mobject (attr, add_box_attributes new_attr box) - | mpres -> - Mpresentation.set_attr (new_attr @ Mpresentation.get_attr mpres) mpres -and add_box_attributes new_attr = function - | Box.Object (attr, mpres) -> - Box.Object (attr, add_mpres_attributes new_attr mpres) - | box -> Box.set_attr (new_attr @ Box.get_attr box) box - -let box_of mathonly spec attrs children = - match children with - | [t] -> add_mpres_attributes attrs t - | _ -> - let kind, spacing, indent = spec in - let dress children = - if spacing then - NotationUtil.dress small_skip children - else - children - in - if mathonly then Mpresentation.Mrow (attrs, dress children) - else - let attrs' = - (if spacing then RenderingAttrs.spacing_attributes `BoxML else []) - @ (if indent then RenderingAttrs.indent_attributes `BoxML else []) - @ attrs - in - match kind with - | Ast.H -> - if List.for_all eligible_math children then - Mpresentation.Mrow (attrs', - dress (List.map promote_to_math children)) - else - mpres_of_box (Box.H (attrs', - List.map box_of_mpres children)) -(* | Ast.H when List.for_all genuine_math children -> - Mpresentation.Mrow (attrs', dress children) *) - | Ast.V -> - mpres_of_box (Box.V (attrs', - List.map box_of_mpres children)) - | Ast.HV -> - mpres_of_box (Box.HV (attrs', - List.map box_of_mpres children)) - | Ast.HOV -> - mpres_of_box (Box.HOV (attrs', - List.map box_of_mpres children)) - -let open_paren = Mpresentation.Mo ([], "(") -let closed_paren = Mpresentation.Mo ([], ")") -let open_bracket = Mpresentation.Mo ([], "[") -let closed_bracket = Mpresentation.Mo ([], "]") -let open_brace = Mpresentation.Mo ([], "{") -let closed_brace = Mpresentation.Mo ([], "}") -let hidden_substs = Mpresentation.Mtext ([], "{...}") -let hidden_lctxt = Mpresentation.Mtext ([], "[...]") -let open_box_paren = Box.Text ([], "(") -let closed_box_paren = Box.Text ([], ")") -let semicolon = Mpresentation.Mo ([], ";") let toggle_action children = - Mpresentation.Maction ([None, "actiontype", "toggle"], children) + Box.Action ([None, "actiontype", "toggle"], children) type child_pos = [ `Left | `Right | `Inner ] @@ -155,31 +46,17 @@ let pp_assoc = | Gramext.RightA -> "RightA" | Gramext.NonA -> "NonA" -let is_atomic t = - let rec aux_mpres = function - | Mpres.Mi _ - | Mpres.Mo _ - | Mpres.Mn _ - | Mpres.Ms _ - | Mpres.Mtext _ - | Mpres.Mspace _ -> true - | Mpres.Mobject (_, box) -> aux_box box - | Mpres.Maction (_, [mpres]) - | Mpres.Mrow (_, [mpres]) -> aux_mpres mpres - | _ -> false - and aux_box = function - | Box.Space _ - | Box.Ink _ - | Box.Text _ -> true - | Box.Object (_, mpres) -> aux_mpres mpres - | Box.H (_, [box]) - | Box.V (_, [box]) - | Box.HV (_, [box]) - | Box.HOV (_, [box]) - | Box.Action (_, [box]) -> aux_box box - | _ -> false - in - aux_mpres t +let rec is_atomic = function + | Box.Space _ + | Box.Ink _ + | Box.Text _ + | Box.Object _ -> true + | Box.H (_, [box]) + | Box.V (_, [box]) + | Box.HV (_, [box]) + | Box.HOV (_, [box]) + | Box.Action (_, [box]) -> is_atomic box + | _ -> false let add_parens child_prec curr_prec t = if is_atomic t then @@ -191,107 +68,43 @@ let add_parens child_prec curr_prec t = (*prerr_endline ("adding parens around: "^ BoxPp.render_to_string (function x::_->x|_->assert false) ~map_unicode_to_tex:false 80 t);*) - match t with - | Mpresentation.Mobject (_, box) -> - mpres_of_box (Box.H ([], [ open_box_paren; box; closed_box_paren ])) - | mpres -> Mpresentation.Mrow ([], [open_paren; t; closed_paren]) + Box.H ([], [ open_paren; t; closed_paren ]) end else ((*prerr_endline ("NOT adding parens around: "^ BoxPp.render_to_string (function x::_->x|_->assert false) ~map_unicode_to_tex:false 80 t);*)t) -let render status ~lookup_uri ?(prec=(-1)) = - let module A = Ast in - let module P = Mpresentation in -(* let use_unicode = true in *) - let make_href xmlattrs xref = - let xref_uris = - List.fold_right - (fun xref uris -> - match lookup_uri xref with - | None -> uris - | Some uri -> uri :: uris) - !xref [] - in - let xmlattrs_uris, xmlattrs = - let xref_attrs, other_attrs = - List.partition - (function Some "xlink", "href", _ -> true | _ -> false) - xmlattrs - in - List.map (fun (_, _, uri) -> uri) xref_attrs, - other_attrs - in - let uris = - match xmlattrs_uris @ xref_uris with - | [] -> None - | uris -> - Some (String.concat " " - (HExtlib.list_uniq (List.sort String.compare uris))) - in - let xrefs = - match !xref with [] -> None | xrefs -> Some (String.concat " " xrefs) - in - xref := []; - xmlattrs - @ make_attributes [Some "helm", "xref"; Some "xlink", "href"] - [xrefs; uris] - in - let make_xref xref = - let xrefs = - match !xref with [] -> None | xrefs -> Some (String.concat " " xrefs) - in - xref := []; - make_attributes [Some "helm","xref"] [xrefs] - in - (* when mathonly is true no boxes should be generated, only mrows *) - (* "xref" is *) - let rec aux xmlattrs mathonly xref prec t = +let render status ?(prec=(-1)) = + let rec aux prec t = match t with | A.AttributedTerm _ -> - aux_attributes xmlattrs mathonly xref prec t - | A.Num (literal, _) -> - let attrs = - (RenderingAttrs.number_attributes `MathML) - @ make_href xmlattrs xref - in - Mpres.Mn (attrs, literal) - | A.Symbol (literal, _) -> - let attrs = - (RenderingAttrs.symbol_attributes `MathML) - @ make_href xmlattrs xref - in - Mpres.Mo (attrs, to_unicode literal) - | A.Ident (literal, _) -> - let attrs = - (RenderingAttrs.ident_attributes `MathML) - @ make_href xmlattrs xref - in - Mpres.Mi (attrs, to_unicode literal) + aux_attributes [] "" prec t + | A.Num (literal, _) -> Box.Text ([], literal) + | A.Symbol (literal, _) -> Box.Text ([], literal) + | A.Ident (literal, _) -> Box.Text ([], to_unicode literal) | A.Meta(n, l) -> - let local_context l = - box_of mathonly (A.H, false, false) [] - ([ Mpres.Mtext ([], "[") ] @ - (NotationUtil.dress (Mpres.Mtext ([], ";")) + let local_context = + Box.Text ([], "["):: + (NotationUtil.dress (Box.Text ([], ";")) (List.map (function - | None -> Mpres.Mtext ([], "_") - | Some t -> aux xmlattrs mathonly xref prec t) l)) @ - [ Mpres.Mtext ([], "]")]) + | None -> Box.Text ([], "_") + | Some t -> aux prec t) l)) @ + [Box.Text ([], "]")] in - let lctxt_maction = toggle_action [ hidden_lctxt; local_context l ] in - box_of mathonly (A.H, false, false) [] - ([Mpres.Mtext ([], "?"^string_of_int n) ] - @ (if l <> [] then [lctxt_maction] else [])) - | A.Literal l -> aux_literal xmlattrs xref prec l - | A.UserInput -> Mpres.Mtext ([], "%") - | A.Layout l -> aux_layout mathonly xref prec l + Box.H ([], + (Box.Text ([], "?"^string_of_int n):: + (if (l <> []) then [Box.H ([],local_context)] else []))) + | A.Literal l -> aux_literal prec l + | A.UserInput -> Box.Text ([], "%") + | A.Layout l -> aux_layout prec l | A.Magic _ | A.Variable _ -> assert false (* should have been instantiated *) | t -> prerr_endline ("unexpected ast: " ^ NotationPp.pp_term status t); assert false - and aux_attributes xmlattrs mathonly xref prec t = + + and aux_attributes xmlattrs xref prec t = let reset = ref false in let inferred_level = ref None in let expected_level = ref None in @@ -318,9 +131,9 @@ let render status ~lookup_uri ?(prec=(-1)) = | Some prec -> prec in (match !inferred_level with - | None -> aux !new_xmlattrs mathonly new_xref prec t + | None -> aux prec t | Some child_prec -> - let t' = aux !new_xmlattrs mathonly new_xref child_prec t in + let t' = aux child_prec t in (*prerr_endline ("inferred: "^string_of_int child_prec^ " exp: "^string_of_int prec ^ @@ -332,107 +145,68 @@ let render status ~lookup_uri ?(prec=(-1)) = in (* prerr_endline (NotationPp.pp_term t); *) aux_attribute t - and aux_literal xmlattrs xref prec l = - let attrs = make_href xmlattrs xref in + + and aux_literal prec l = (match l with - | `Symbol s -> Mpres.Mo (attrs, to_unicode s) - | `Keyword s -> Mpres.Mtext (attrs, to_unicode s) - | `Number s -> Mpres.Mn (attrs, to_unicode s)) - and aux_layout mathonly xref prec l = - let attrs = make_xref xref in - let invoke' t = aux [] true (ref []) prec t in + | `Symbol s -> Box.Text ([], to_unicode s) + | `Keyword s -> Box.Text ([], to_unicode s) + | `Number s -> Box.Text ([], to_unicode s)) + + and aux_layout prec l = + let attrs = [] in + let invoke' t = aux prec t in (* use the one below to reset precedence and associativity *) - let invoke_reinit t = aux [] mathonly xref ~-1 t in + let invoke_reinit t = aux ~-1 t in match l with | A.Sup (A.Layout (A.Sub (t1,t2)), t3) | A.Sup (A.AttributedTerm (_,A.Layout (A.Sub (t1,t2))), t3) - -> Mpres.Msubsup (attrs, invoke' t1, invoke_reinit t2, invoke_reinit t3) - | A.Sub (t1, t2) -> Mpres.Msub (attrs, invoke' t1, invoke_reinit t2) - | A.Sup (t1, t2) -> Mpres.Msup (attrs, invoke' t1, invoke_reinit t2) - | A.Below (t1, t2) -> Mpres.Munder (attrs, invoke' t1, invoke_reinit t2) - | A.Above (t1, t2) -> Mpres.Mover (attrs, invoke' t1, invoke_reinit t2) + -> assert false + | A.Sub (t1, t2) -> assert false + | A.Sup (t1, t2) -> assert false + | A.Below (t1, t2) -> assert false + | A.Above (t1, t2) -> assert false | A.Frac (t1, t2) - | A.Over (t1, t2) -> - Mpres.Mfrac (attrs, invoke_reinit t1, invoke_reinit t2) - | A.Atop (t1, t2) -> - Mpres.Mfrac (atop_attributes @ attrs, invoke_reinit t1, - invoke_reinit t2) - | A.InfRule (t1, t2, t3) -> - Mpres.Mstyle ([None,"mathsize","big"], - Mpres.Mrow (attrs, - [Mpres.Mfrac ([], - Mpres.Mstyle ([None,"scriptlevel","0"],invoke_reinit t1), - Mpres.Mstyle ([None,"scriptlevel","0"],invoke_reinit t2)); - Mpres.Mstyle ([None,"scriptlevel","2"], - Mpresentation.Mspace - (RenderingAttrs.small_skip_attributes `MathML)); - Mpres.Mstyle ([None,"scriptlevel","1"],invoke_reinit t3)])) - | A.Sqrt t -> Mpres.Msqrt (attrs, invoke_reinit t) - | A.Root (t1, t2) -> - Mpres.Mroot (attrs, invoke_reinit t1, invoke_reinit t2) - | A.Box ((_, spacing, _) as kind, terms) -> - let children = - aux_children mathonly spacing xref prec - (NotationUtil.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 - (NotationUtil.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 - (NotationUtil.ungroup terms))) + | A.Over (t1, t2) -> assert false + | A.Atop (t1, t2) -> assert false + | A.InfRule (t1, t2, t3) -> assert false + | A.Sqrt t -> assert false + | A.Root (t1, t2) -> assert false + | A.Box (a, terms) -> + let children = List.map (aux prec) terms in + Box.H([],children) + | A.Mstyle (l,terms) -> assert false + | A.Mpadded (l,terms) -> assert false | A.Maction alternatives -> toggle_action (List.map invoke_reinit alternatives) - | A.Group terms -> - let children = - aux_children mathonly false xref prec - (NotationUtil.ungroup terms) - in - box_of mathonly (A.H, false, false) attrs children - | A.Break -> assert false (* TODO? *) - and aux_children mathonly spacing xref prec terms = - let find_clusters = - let rec aux_list first clusters acc = - function - [] when acc = [] -> List.rev clusters - | [] -> aux_list first (List.rev acc :: clusters) [] [] - | (A.Layout A.Break) :: tl when acc = [] -> - aux_list first clusters [] tl - | (A.Layout A.Break) :: tl -> - aux_list first (List.rev acc :: clusters) [] tl - | [hd] -> - aux_list false clusters - (aux [] mathonly xref prec hd :: acc) [] - | hd :: tl -> - aux_list false clusters - (aux [] mathonly xref prec hd :: acc) tl - in - aux_list true [] [] - in - let boxify_pres = - function - [t] -> t - | tl -> box_of mathonly (A.H, spacing, false) [] tl - in - List.map boxify_pres (find_clusters terms) + | A.Group terms -> assert false + | A.Break -> assert false in - aux [] false (ref []) prec - -let rec print_box (t: boxml_markup) = - Box.box2xml print_mpres t -and print_mpres (t: mathml_markup) = - Mpresentation.print_mpres print_box t - -let print_xml = print_mpres + aux prec (* let render_to_boxml id_to_uri t = let xml_stream = print_box (box_of_mpres (render id_to_uri t)) in Xml.add_xml_declaration xml_stream *) +let render_context_entry status name = function + | A.Decl t -> + Box.H ([], + [Box.Text([],name); Box.Text([],":"); + render status (TermContentPres.pp_ast status t)]) + | A.Def (t,ty) -> + Box.H ([], + [Box.Text([],name); Box.Text([],Utf8Macro.unicode_of_tex"\\def"); + render status (TermContentPres.pp_ast status t)]) + +let render_context status context = + Box.V ([], + List.map + (fun (name,entry) -> + render_context_entry status (to_unicode name) entry) context) + +let render_sequent status (i,context,ty) = + Box.V ([], + [render_context status context; + Box.Ink [None,"width","4cm"; None,"height","2px"]; + render status (TermContentPres.pp_ast status ty)]) + + diff --git a/matitaB/components/content_pres/cicNotationPres.mli b/matitaB/components/content_pres/cicNotationPres.mli index 57e7ee844..65507f053 100644 --- a/matitaB/components/content_pres/cicNotationPres.mli +++ b/matitaB/components/content_pres/cicNotationPres.mli @@ -23,34 +23,15 @@ * http://helm.cs.unibo.it/ *) -type mathml_markup = boxml_markup Mpresentation.mpres -and boxml_markup = mathml_markup Box.box -type markup = mathml_markup +type markup = string Box.box -(** {2 Markup conversions} *) - -val mpres_of_box: boxml_markup -> mathml_markup -val box_of_mpres: mathml_markup -> boxml_markup - -(** {2 Rendering} *) - -(** level 1 -> level 0 - * @param ids_to_uris mapping id -> uri for hyperlinking - * @param prec precedence level *) val render: #NCic.status -> - lookup_uri:(Content.id -> string option) -> ?prec:int -> NotationPt.term -> - markup - -(** level 0 -> xml stream *) -val print_xml: markup -> Xml.token Stream.t - -(* |+* level 1 -> xml stream - * @param ids_to_uris +| -val render_to_boxml: - (Cic.id, string) Hashtbl.t -> NotationPt.term -> Xml.token Stream.t *) - -val print_box: boxml_markup -> Xml.token Stream.t -val print_mpres: mathml_markup -> Xml.token Stream.t + ?prec:int -> NotationPt.term -> + markup +val render_sequent: + #TermContentPres.status -> + NotationPt.sequent -> + markup