X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matitaB%2Fcomponents%2Fcontent_pres%2FcicNotationPres.ml;h=553ab1ae1ba2aa352439e0935255e8318eff52d5;hb=ccf5878f2a2ec7f952f140e162391708a740517b;hp=30847816982ceb501d202ffb5152b846b7cb5a6e;hpb=6f020d79dea92003151e5e588fd73452f20ffb2c;p=helm.git diff --git a/matitaB/components/content_pres/cicNotationPres.ml b/matitaB/components/content_pres/cicNotationPres.ml index 308478169..553ab1ae1 100644 --- a/matitaB/components/content_pres/cicNotationPres.ml +++ b/matitaB/components/content_pres/cicNotationPres.ml @@ -31,6 +31,7 @@ type markup = string Box.box 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 ([], ";") @@ -74,13 +75,47 @@ let add_parens child_prec curr_prec t = 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 = @@ -95,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 _ @@ -146,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 @@ -171,17 +210,47 @@ let render status ?(prec=(-1)) = | 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 -> Box.Space [] + | 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 @@ -198,14 +267,15 @@ let render_context_entry status name = function 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)])