From: Stefano Zacchiroli Date: Wed, 27 Jul 2005 07:54:24 +0000 (+0000) Subject: *** empty log message *** X-Git-Tag: V_0_7_2~48 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=206f96afb7097c20b3cc8bd144825467b4fde7ae;p=helm.git *** empty log message *** --- diff --git a/helm/ocaml/cic_notation/.depend b/helm/ocaml/cic_notation/.depend index da57d442c..3a17410dd 100644 --- a/helm/ocaml/cic_notation/.depend +++ b/helm/ocaml/cic_notation/.depend @@ -9,6 +9,7 @@ cicNotationRew.cmi: cicNotationPt.cmo cicNotationParser.cmi: cicNotationPt.cmo cicNotationEnv.cmi grafiteParser.cmi: grafiteAst.cmo cicNotationPt.cmo cicNotationPres.cmi: mpresentation.cmi cicNotationPt.cmo box.cmi +boxPp.cmi: cicNotationPres.cmi cicNotation.cmi: grafiteAst.cmo grafiteAst.cmo: cicNotationPt.cmo grafiteAst.cmx: cicNotationPt.cmx @@ -64,6 +65,10 @@ cicNotationPres.cmo: renderingAttrs.cmi mpresentation.cmi cicNotationUtil.cmi \ cicNotationPres.cmx: renderingAttrs.cmx mpresentation.cmx cicNotationUtil.cmx \ cicNotationPt.cmx cicNotationPres.cmx cicNotationPp.cmx box.cmx \ cicNotationPres.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 cicNotation.cmo: grafiteParser.cmi grafiteAst.cmo cicNotationRew.cmi \ cicNotationParser.cmi cicNotationFwd.cmi cicNotation.cmi cicNotation.cmx: grafiteParser.cmx grafiteAst.cmx cicNotationRew.cmx \ diff --git a/helm/ocaml/cic_notation/Makefile b/helm/ocaml/cic_notation/Makefile index 898efa32a..61c3f6d08 100644 --- a/helm/ocaml/cic_notation/Makefile +++ b/helm/ocaml/cic_notation/Makefile @@ -24,6 +24,7 @@ INTERFACE_FILES = \ mpresentation.mli \ box.mli \ cicNotationPres.mli \ + boxPp.mli \ cicNotation.mli \ $(NULL) IMPLEMENTATION_FILES = \ diff --git a/helm/ocaml/cic_notation/TODO b/helm/ocaml/cic_notation/TODO index 9b74c2cfa..ad5df1a6f 100644 --- a/helm/ocaml/cic_notation/TODO +++ b/helm/ocaml/cic_notation/TODO @@ -5,14 +5,15 @@ TODO * prestazioni trasformazioni 3 => 2 e 2 => 1 * magic per gestione degli array? * gestione della notazione per i numeri +* pretty printing verso testo * sintassi concreta - studiare/implementare sintassi con ... per i magic fold -* integrazione - - togliere file non piu' utilizzati (caterva di cvs remove) * trasformazioni - - parentesi cagose + - parentesi cagose (tail) - spacing delle keyword - hyperlink su head dei case pattern e sul tipo induttivo su cui si fa match + - hyperlink multipli con il magic fold (e.g. notazione per le liste) + - ident0 -> ident_0 ? * bug di rimozione della notazione: pare che camlp4 distrugga un livello grammaticale quando toglie l'ultima produzione ivi definita @@ -37,6 +38,7 @@ DONE - salvare la notazione nei file .moo - portare le trasformazioni al nuovo ast - gestire i problemi di ridefinizione della stessa notazione? + - togliere file non piu' utilizzati (caterva di cvs remove) * gtkmathview - aggiungere metodo per caricare un file di configurazione dell'utente (idem nel binding) diff --git a/helm/ocaml/cic_notation/cicNotationPres.ml b/helm/ocaml/cic_notation/cicNotationPres.ml index e7afad578..7c87dedce 100644 --- a/helm/ocaml/cic_notation/cicNotationPres.ml +++ b/helm/ocaml/cic_notation/cicNotationPres.ml @@ -23,6 +23,8 @@ * http://helm.cs.unibo.it/ *) +module P = Mpresentation + type mathml_markup = boxml_markup Mpresentation.mpres and boxml_markup = mathml_markup Box.box @@ -69,7 +71,8 @@ let rec promote_to_math = | Mpresentation.Mobject ([], Box.Object ([], mpres)) -> promote_to_math mpres | math -> math -let small_skip = Mpresentation.Mspace [None, "width", "0.5em"] +let small_skip = + Mpresentation.Mspace (RenderingAttrs.small_skip_attributes `MathML) let box_of mathonly spec attrs children = match children with @@ -85,8 +88,8 @@ let box_of mathonly spec attrs children = if mathonly then Mpresentation.Mrow (attrs, dress children) else let attrs' = - (if spacing then [None, "spacing", "0.5em"] else []) - @ (if indent then [None, "indent", "0.5em"] else []) + (if spacing then RenderingAttrs.spacing_attributes `BoxML else []) + @ (if indent then RenderingAttrs.indent_attributes `BoxML else []) @ attrs in match kind with @@ -136,7 +139,6 @@ let pp_pos = | `Inner -> "`Inner" let is_atomic t = - let module P = Mpresentation in let rec aux_mpres = function | P.Mi _ | P.Mo _ @@ -204,8 +206,8 @@ let render ids_to_uris = (* when mathonly is true no boxes should be generated, only mrows *) let rec aux xmlattrs mathonly xref pos prec uris t = match t with - | A.AttributedTerm (attr, t) -> - aux_attribute xmlattrs mathonly xref pos prec uris t attr + | A.AttributedTerm _ -> + aux_attributes xmlattrs mathonly xref pos prec uris t | A.Num (literal, _) -> let attrs = (RenderingAttrs.number_attributes `MathML) @@ -263,8 +265,34 @@ let render ids_to_uris = | t -> prerr_endline ("unexpected ast: " ^ CicNotationPp.pp_term t); assert false - and aux_attribute xmlattrs mathonly xref pos prec uris t = - function + and aux_attributes xmlattrs mathonly xref pos prec uris t = + let new_level = ref None in + let new_xref = ref None in + let new_uris = ref [] in + let new_xmlattrs = ref [] in + let rec aux_attribute = + function + | A.AttributedTerm (attr, t) -> + (match attr with + | `Loc _ + | `Raw _ -> () + | `Level (child_prec, child_assoc) -> + new_level := Some (child_prec, child_assoc) + | `IdRef xref -> new_xref := Some xref + | `Href hrefs -> new_uris := hrefs + | `XmlAttrs attrs -> new_xmlattrs := attrs); + aux_attribute t + | t -> + (match !new_level with + | None -> aux !new_xmlattrs mathonly !new_xref pos prec !new_uris t + | Some (child_prec, child_assoc) -> + let t' = + aux !new_xmlattrs mathonly !new_xref pos child_prec !new_uris t + in + add_parens child_prec child_assoc pos prec t') + in + aux_attribute t +(* function | `Loc _ | `Raw _ -> aux xmlattrs mathonly xref pos prec uris t | `Level (child_prec, child_assoc) -> @@ -272,7 +300,7 @@ let render ids_to_uris = add_parens child_prec child_assoc pos prec t' | `IdRef xref -> aux xmlattrs mathonly (Some xref) pos prec uris t | `Href uris' -> aux xmlattrs mathonly xref pos prec uris' t - | `XmlAttrs xmlattrs -> aux xmlattrs mathonly xref pos prec uris t + | `XmlAttrs xmlattrs -> aux xmlattrs mathonly xref pos prec uris t *) and aux_literal xmlattrs xref prec uris l = let attrs = make_href xmlattrs xref uris in (match l with @@ -358,7 +386,9 @@ let rec print_box (t: CicNotationPres.boxml_markup) = and print_mpres (t: CicNotationPres.mathml_markup) = Mpresentation.print_mpres print_box t -let render_to_boxml id_to_uri t = +let print_xml = print_mpres + +(* 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 + Xml.add_xml_declaration xml_stream *) diff --git a/helm/ocaml/cic_notation/cicNotationPres.mli b/helm/ocaml/cic_notation/cicNotationPres.mli index f507dc6bf..d02973871 100644 --- a/helm/ocaml/cic_notation/cicNotationPres.mli +++ b/helm/ocaml/cic_notation/cicNotationPres.mli @@ -28,20 +28,25 @@ and boxml_markup = mathml_markup Box.box type markup = mathml_markup +(** {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 *) val render: (Cic.id, string) Hashtbl.t -> CicNotationPt.term -> markup -(** @param ids_to_uris *) -val render_to_boxml: - (Cic.id, string) Hashtbl.t -> CicNotationPt.term -> Xml.token Stream.t - -(* val render_to_mathml: - (Cic.id, string) Hashtbl.t -> CicNotationPt.term -> mathml_markup *) +(** level 0 -> xml stream *) +val print_xml: markup -> Xml.token Stream.t -val mpres_of_box: boxml_markup -> mathml_markup -val box_of_mpres: mathml_markup -> boxml_markup +(* |+* level 1 -> xml stream + * @param ids_to_uris +| +val render_to_boxml: + (Cic.id, string) Hashtbl.t -> CicNotationPt.term -> Xml.token Stream.t *) -val print_mpres: mathml_markup -> Xml.token Stream.t val print_box: boxml_markup -> Xml.token Stream.t +val print_mpres: mathml_markup -> Xml.token Stream.t diff --git a/helm/ocaml/cic_notation/test_parser.ml b/helm/ocaml/cic_notation/test_parser.ml index dc76884ac..1ad6b924a 100644 --- a/helm/ocaml/cic_notation/test_parser.ml +++ b/helm/ocaml/cic_notation/test_parser.ml @@ -39,7 +39,9 @@ let dump_xml t id_to_uri fname = prerr_endline (sprintf "dumping MathML to %s ..." fname); flush stdout; let oc = open_out fname in - Xml.pp_to_outchan (CicNotationPres.render_to_boxml id_to_uri t) oc; + let markup = CicNotationPres.render id_to_uri t in + let xml_stream = CicNotationPres.print_xml markup in + Xml.pp_to_outchan xml_stream oc; close_out oc let extract_loc =