X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matitaB%2Fcomponents%2Fcontent_pres%2FboxPp.ml;h=af11da8112b5fe8a3502874327c69471cd75f5e6;hb=1b67bd4dfa12ef25b8fa63884c71893b961db27d;hp=9bf360a637d45fd1c5d654aae2e8007c19a832ce;hpb=6f020d79dea92003151e5e588fd73452f20ffb2c;p=helm.git
diff --git a/matitaB/components/content_pres/boxPp.ml b/matitaB/components/content_pres/boxPp.ml
index 9bf360a63..af11da811 100644
--- a/matitaB/components/content_pres/boxPp.ml
+++ b/matitaB/components/content_pres/boxPp.ml
@@ -32,7 +32,7 @@ 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 = (* string_space *) " "
let string_indent_len = utf8_string_length string_indent
let string_ink = "---------------------------"
let string_ink_len = utf8_string_length string_ink
@@ -40,8 +40,10 @@ let string_ink_len = utf8_string_length string_ink
let contains_attrs contained container =
List.for_all (fun attr -> List.mem attr container) contained
-let want_indent = contains_attrs (* (RenderingAttrs.indent_attributes `BoxML) *)[]
-let want_spacing = contains_attrs (* (RenderingAttrs.spacing_attributes `BoxML) *) []
+let small_skip_attributes _ = [ None, "width", "0.5em" ]
+
+let want_indent = contains_attrs [ None, "indent", "0.5em" ]
+let want_spacing = contains_attrs [ None, "spacing", "0.5em" ]
let shift off = List.map (fun (start,stop,v) -> start+off,stop+off,v);;
@@ -102,10 +104,33 @@ let fixed_rendering s =
let render_to_strings ~map_unicode_to_tex choose_action size markup =
prerr_endline ("render size is " ^ string_of_int size);
+ let add_markup attr txt =
+ let txt = Netencoding.Html.encode ~in_enc:`Enc_utf8 () txt in
+ let value_of_attr (_,_,v) = v in
+ let title =
+ try Some (value_of_attr (List.find (fun (_,t,_) -> t = "title") attr))
+ with _ -> None in
+ let href =
+ try Some (value_of_attr (List.find (fun (_,t,_) -> t = "href") attr))
+ with _ -> None in
+ match title,href with
+ | None,None -> txt
+ | None,Some u -> "" ^ txt ^ ""
+ | Some t, Some u ->
+ "" ^ txt ^ ""
+ | Some t, None ->
+ let u = "cic:/fakeuri.con" in
+ "" ^ txt ^ ""
+ in
+
let max_size = max_int in
let rec aux_box =
function
- | Box.Text (_, t) -> fixed_rendering t
+ | Box.Text (attr, t) ->
+ fun x ->
+ (match fixed_rendering t x with
+ | len, [txt] -> len, [add_markup attr txt]
+ | _ -> assert false)
| Box.Space _ -> fixed_rendering string_space
| Box.Ink _ -> fixed_rendering string_ink
| Box.Action (_, []) -> assert false