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

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

diff --git a/matitaB/components/content_pres/cicNotationPres.ml b/matitaB/components/content_pres/cicNotationPres.ml
index 7f1470f76d8f44935ec8a9d1ff1c192a6a8acaf5..e0ca07b563ab6c64c651e139cf4a8b5e10dd0e8a 100644 (file)
--- a/matitaB/components/content_pres/cicNotationPres.ml
+++ b/matitaB/components/content_pres/cicNotationPres.ml
@@ -103,17 +103,19 @@ let render status ?(prec=(-1)) =
     | A.AttributedTerm _ ->
         aux_attributes [] ""  prec t
     | A.Num (literal, _) -> Box.Text ([], literal)
-    | A.Symbol (literal, Some (None,desc)) -> 
-        let txt = "<A title=\"" ^ desc ^ "\">" ^ literal ^ "</A>" in 
-                    Box.Text ([], to_unicode txt)
+    | A.Symbol (literal, Some (None,desc)) ->
+        let literal = to_unicode literal in
+        let attr = [ None, "title", desc ] in
+          Box.Text (attr, literal)
     | A.Symbol (literal, Some (Some u,desc)) -> 
-        let txt = 
-         "<A href=\"" ^ u ^ "\" title=\"" ^ desc ^ "\">" ^ literal ^ "</A>" in
-        Box.Text ([], to_unicode txt)
+        let literal = to_unicode literal in
+        let attr = [ None, "title", desc; None, "href", u ] in
+        Box.Text (attr, literal)
     | A.Symbol (literal, _) -> Box.Text ([], to_unicode literal)
     | A.Ident (literal, `Uri u) ->
-        let txt = "<A href=\"" ^ u ^ "\">" ^ literal ^ "</A>" in 
-        Box.Text ([], to_unicode txt)
+        let attr = [ None, "href", u ] in
+        let literal = to_unicode literal in
+        Box.Text (attr,literal)
     | A.Ident (literal, _) -> Box.Text ([], to_unicode literal)
     | A.Meta(n, l) ->
         let local_context =
@@ -128,7 +130,17 @@ let render status ?(prec=(-1)) =
         Box.H ([],
           (Box.Text ([], "?"^string_of_int n)::
             (if (l <> []) then [Box.H ([],local_context)] else [])))
-    | A.Literal l -> aux_literal prec l
+    | A.Literal (`Symbol (s,x))
+    | A.Literal (`Keyword (s,x))
+    | A.Literal (`Number (s,x)) ->
+       let attr = 
+         match x with
+         | None, None -> []
+         | Some u, None -> [ None, "href", u ]
+         | None, Some d -> [ None, "title", d ]
+         | Some u, Some d -> [ None, "href", u; None, "title", d ]
+       in        
+       Box.Text (attr, to_unicode s)
     | A.UserInput -> Box.Text ([], "%")
     | A.Layout l -> aux_layout prec l
     | A.Magic _
@@ -179,12 +191,6 @@ let render status ?(prec=(-1)) =
 (*     prerr_endline (NotationPp.pp_term t); *)
     aux_attribute t
 
-  and aux_literal prec l =
-    (match l with
-    | `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