| 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 =
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 _
(* 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
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 =