let to_unicode = Utf8Macro.unicode_of_tex
+let small_skip = Box.Text ([], " ")
let open_paren = Box.Text ([], "(")
let closed_paren = Box.Text ([], ")")
let semicolon = Box.Text ([], ";")
BoxPp.render_to_string (function x::_->x|_->assert false)
~map_unicode_to_tex:false 80 t);*)t)
+let box_of spec attrs children =
+ match children with
+ | [t] -> t
+ | _ ->
+ let kind, spacing, indent = spec in
+ let dress children =
+ if spacing then
+ NotationUtil.dress small_skip children
+ else
+ children
+ in
+ let attrs' =
+ (if spacing then [None, "spacing", "0.5em"] else [])
+ @ (if indent then [None, "indent", "0.5em"] else [])
+ @ attrs
+ in
+ match kind with
+ | A.H -> Box.H (attrs',children)
+ | A.V -> Box.V (attrs',children)
+ | A.HV -> Box.HV (attrs',children)
+ | A.HOV -> Box.HOV (attrs',children)
+
let render status ?(prec=(-1)) =
let rec aux prec t =
match t with
| A.AttributedTerm _ ->
aux_attributes [] "" prec t
| A.Num (literal, _) -> Box.Text ([], literal)
- | A.Symbol (literal, _) -> Box.Text ([], literal)
+ | 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 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 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
| A.Sup (A.Layout (A.Sub (t1,t2)), t3)
| A.Sup (A.AttributedTerm (_,A.Layout (A.Sub (t1,t2))), t3)
-> assert false
- | A.Sub (t1, t2) -> assert false
- | A.Sup (t1, t2) -> assert false
+ | A.Sub (t1, t2) -> Box.H ([],[aux prec t1;Box.Text ([],"_");aux prec t2])
+ | A.Sup (t1, t2) -> Box.H ([],[aux prec t1;Box.Text ([],"^");aux prec t2])
| A.Below (t1, t2) -> assert false
| A.Above (t1, t2) -> assert false
| A.Frac (t1, t2)
| A.InfRule (t1, t2, t3) -> assert false
| A.Sqrt t -> assert false
| A.Root (t1, t2) -> assert false
- | A.Box (a, terms) ->
- let children = List.map (aux prec) terms in
- Box.H([],children)
+ | A.Box ((_,spacing,_) as kind, terms) ->
+ let children =
+ aux_children spacing prec
+ (NotationUtil.ungroup terms)
+ in
+ box_of kind attrs children
| A.Mstyle (l,terms) -> assert false
| A.Mpadded (l,terms) -> assert false
| A.Maction alternatives ->
toggle_action (List.map invoke_reinit alternatives)
| A.Group terms -> assert false
- | A.Break -> assert false
+ | A.Break -> Box.Space []
+ and aux_children spacing prec terms =
+ let find_clusters =
+ let rec aux_list first clusters acc =
+ function
+ [] when acc = [] -> List.rev clusters
+ | [] -> aux_list first (List.rev acc :: clusters) [] []
+ | (A.Layout A.Break) :: tl when acc = [] ->
+ aux_list first clusters [] tl
+ | (A.Layout A.Break) :: tl ->
+ aux_list first (List.rev acc :: clusters) [] tl
+ | [hd] ->
+ aux_list false clusters
+ (aux prec hd :: acc) []
+ | hd :: tl ->
+ aux_list false clusters
+ (aux prec hd :: acc) tl
+ in
+ aux_list true [] []
+ in
+ let boxify_pres =
+ function
+ [t] -> t
+ | tl -> box_of (A.H, spacing, false) [] tl
+ in
+ List.map boxify_pres (find_clusters terms)
in
- aux prec
+ (fun t ->
+ (* prerr_endline ("ast:\n" ^ (NotationPp.pp_term status t));*)
+ aux prec t)
(* let render_to_boxml id_to_uri t =
let xml_stream = print_box (box_of_mpres (render id_to_uri t)) in
render status (TermContentPres.pp_ast status t)])
let render_context status context =
- Box.V ([],
+ Box.V ([],
+ Box.Space [None, "width", "0.5em"]::
List.map
(fun (name,entry) ->
render_context_entry status (to_unicode name) entry) context)
let render_sequent status (i,context,ty) =
Box.V ([],
- [render_context status context;
+ [render_context status (List.rev context);
Box.Ink [None,"width","4cm"; None,"height","2px"];
render status (TermContentPres.pp_ast status ty)])