X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=matitaB%2Fcomponents%2Fcontent_pres%2FcicNotationPres.ml;h=553ab1ae1ba2aa352439e0935255e8318eff52d5;hb=2c26d3c2140cfc213c960568587f8350e34d3459;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 = "" ^ literal ^ "" 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 =
- "" ^ literal ^ "" 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 = "" ^ literal ^ "" 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 =