Added support for hyperlinks in the goal view of the web interface.

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

diff --git a/matitaB/components/content_pres/boxPp.ml b/matitaB/components/content_pres/boxPp.ml
index 9511de631380c8b72d4bff00cca1500c3fa8b79a..af11da8112b5fe8a3502874327c69471cd75f5e6 100644 (file)
--- a/matitaB/components/content_pres/boxPp.ml
+++ b/matitaB/components/content_pres/boxPp.ml
@@ -104,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 -> "<A href=\"" ^ u ^ "\">" ^ txt ^ "</A>"
+    | Some t, Some u ->
+       "<A href=\"" ^ u ^ "\" title=\"" ^ t ^ "\">" ^ txt ^ "</A>"
+    | Some t, None ->
+       let u = "cic:/fakeuri.con" in
+       "<A href=\"" ^ u ^ "\" title=\"" ^ t ^ "\">" ^ txt ^ "</A>"
+  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