On 27/04/11 16:17, Lu Zhao wrote: > I have a pretty printer function added by using temp_add_user_printer. > It looks like the following:
> --------------------------------------------------------------
> fun pp_lins Gs sys (ppsFun:ppstream_funs) gravs d pps t : unit = let
> val (label, code) = (dest_pair) t
> val ins = code |> term_to_string
> |> cached_add_comment
> val str = #add_string ppsFun
> in
> str "(";
> sys (Top, Top, Top) (d - 1) label;
> str ",";
> sys (Top, Top, Top) (d - 1) code;
> str ins;
> str ")";
> ()
> end handle _ => raise term_pp_types.UserPP_Failed;
You need to replace the semi-colon sequencing with smpp.>>. The best way to do
this is to do
fun myprinter args = let
open smpp
...
in
str "(" >>
sys (Top,Top,Top) (d - 1) label >>
...
end handle _ => ...
For an example, see the way that I changed the printer for conditional
expressions in src/1/ParseExtras.sml to see what the parameters to your
function should be.
> Also, how to remove a user-added-printer correspondingly? My current
> method is the following, which I don't know if still works in the latest
> HOL:
You should use remove_user_printer or temp_remove_user_printer.
Michael
signature.asc
Description: OpenPGP digital signature
------------------------------------------------------------------------------ WhatsUp Gold - Download Free Network Management Software The most intuitive, comprehensive, and cost-effective network management toolset available today. Delivers lowest initial acquisition cost and overall TCO of any competing solution. http://p.sf.net/sfu/whatsupgold-sd
_______________________________________________ hol-info mailing list [email protected] https://lists.sourceforge.net/lists/listinfo/hol-info
