]> matita.cs.unibo.it Git - helm.git/commitdiff
Simplified rendering
authorAndrea Asperti <andrea.asperti@unibo.it>
Fri, 20 May 2011 08:42:04 +0000 (08:42 +0000)
committerAndrea Asperti <andrea.asperti@unibo.it>
Fri, 20 May 2011 08:42:04 +0000 (08:42 +0000)
matitaB/components/content_pres/.depend
matitaB/components/content_pres/Makefile
matitaB/components/content_pres/box.ml
matitaB/components/content_pres/box.mli
matitaB/components/content_pres/boxPp.ml
matitaB/components/content_pres/boxPp.mli
matitaB/components/content_pres/cicNotationPres.ml
matitaB/components/content_pres/cicNotationPres.mli

index f519ea34f0b36405bef7ea6a8800223aa53af35a..dcc30c6ee9ed7e06137c30d0c4c330412d4c1b66 100644 (file)
@@ -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 
index 084940b4dd7c6450eee9c2613631c5e02250887a..658d8d354d62465e5ef717dc723034e8ae4abad6 100644 (file)
@@ -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
index 7c50692621d99ff3fcff497209ce81c64193924d..6e5bb4d922910fee54e5357ee41ab9c6226ac567 100644 (file)
  * http://cs.unibo.it/helm/.
  *)
 
-(*************************************************************************)
-(*                                                                       *)
-(*                           PROJECT HELM                                *)
-(*                                                                       *)
-(*                Andrea Asperti <asperti@cs.unibo.it>                   *)
-(*                             13/2/2004                                 *)
-(*                                                                       *)
-(*************************************************************************)
-
 (* $Id$ *)
 
 type 
index d2ca17bddd15128a15c2e7146e4e4d7f58b33585..e7c2588ebade764d308a39bab3c3a695355a5853 100644 (file)
  * http://cs.unibo.it/helm/.
  *)
 
-(*************************************************************************)
-(*                                                                       *)
-(*                           PROJECT HELM                                *)
-(*                                                                       *)
-(*                Andrea Asperti <asperti@cs.unibo.it>                   *)
-(*                             13/2/2004                                 *)
-(*                                                                       *)
-(*************************************************************************)
-
 type 
   'expr box =
     Text of attr * string
index 45c8b6c20b89f4c131848c92da3d93d39a263b06..7f71aa20bd81f8ffd0abbfb63a9c59a0cc19a851 100644 (file)
@@ -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)
index c4d6fd53b8d51150a757e5b29f37c094acf91617..32e31e84858b0a6854d45dd950d84c9813e83ef5 100644 (file)
    * @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
 
index 305fe57947edba39d50e13c0c834230b1e15a023..563af0b065454388fc7b88421c16f966ed148e22 100644 (file)
  * 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)])
+         
+
index 57e7ee84463ee565399346248e19d8e75db9726c..65507f05394b7ba3a0a933de6f96244eedde15c3 100644 (file)
  * 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