X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matitaB%2Fcomponents%2Fcontent_pres%2FcicNotationPres.ml;h=553ab1ae1ba2aa352439e0935255e8318eff52d5;hb=c81b0e8dbfe80e2350e9322afa8316f39f98c3b3;hp=7f1470f76d8f44935ec8a9d1ff1c192a6a8acaf5;hpb=4e89ae4ac9b001c0479d68d9f74fe81fca6ecd2d;p=helm.git

diff --git a/matitaB/components/content_pres/cicNotationPres.ml b/matitaB/components/content_pres/cicNotationPres.ml
index 7f1470f76..553ab1ae1 100644
--- 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
@@ -243,7 +249,7 @@ let render status ?(prec=(-1)) =
       List.map boxify_pres (find_clusters terms) 
   in
   (fun t ->
-          prerr_endline ("ast:\n" ^ (NotationPp.pp_term status t));
+   (* prerr_endline ("ast:\n" ^ (NotationPp.pp_term status t));*)
   aux prec t)
 
 (* let render_to_boxml id_to_uri t =