HUGE COMMIT:

[helm.git] / matita / components / content_pres / boxPp.ml

diff --git a/matita/components/content_pres/boxPp.ml b/matita/components/content_pres/boxPp.ml
index 0d58d97643a17aa147d117d006ed4cc8cec212d5..80c669d457ff004241c58630675eee928313c719 100644 (file)
--- a/matita/components/content_pres/boxPp.ml
+++ b/matita/components/content_pres/boxPp.ml
@@ -33,7 +33,7 @@ let string_space = " "
 let string_space_len = String.length string_space
 let string_indent = (* string_space *) ""
 let string_indent_len = String.length string_indent
-let string_ink = "##"
+let string_ink = "---------------------------"
 let string_ink_len = String.length string_ink
 
 let contains_attrs contained container =
@@ -51,6 +51,9 @@ let choose_rendering size (best, other) =
   let best_size, _ = best in
   if size >= best_size then best else other
 
+(* merge_columns [ X1 ;  X3 ] returns X1
+                   X2    X4           X2 X3
+                                         X4 *)
 let merge_columns sep cols =
   let sep_len = String.length sep in
   let indent = ref 0 in
@@ -242,6 +245,8 @@ let render_to_strings ~map_unicode_to_tex choose_action size markup =
   snd (aux_mpres markup size)
 
 let render_to_string ~map_unicode_to_tex choose_action size markup =
+ (* CSC: no information about hyperlinks yet *)
+ [],
   String.concat "\n"
     (render_to_strings ~map_unicode_to_tex choose_action size markup)