If you put a temp-printer in your theory, it won't be around in descendents of
that theory, including within the munger. Instead, put your temp_ call into a
"normal" SML file, and make that file one of the arguments to the mkmunge call.
Michael
On 26/07/14 19:53, Ramana Kumar wrote:
> I tried installing a custom pretty-printer as follows (in my pretty-printing
> theory used for creating the munger):
>
> val () = temp_add_user_printer("stringprinter",``s:string``,stringprinter)
>
> But it seems that stringprinter is never called. Does the special treatment of
> string literals supersede user printers somehow, or have I done something
> wrong?
>
> Maybe Literal.string_literalpp should be overridable?
>
>
> On Fri, Jul 25, 2014 at 7:32 AM, Michael Norrish <[email protected]
> <mailto:[email protected]>> wrote:
>
> I can't think of an easy solution for this other than a custom user-level
> pretty-printer. You should probably make a feature request so that the
> TeX
> technology can do this itself. (And then think about implementing the
> feature
> request yourself :)
>
> Perhaps the classier implementation route would be to extend the backend
> API so
> that various literal forms were handled specially.
>
> Michael
>
> On 25/07/14 01:04, Ramana Kumar wrote:
> > By default the munger doesn't do anything special to strings; the usual
> > pretty-printing behaviour is to print the elements of the string
> without any
> > separators between double-quotes. In math mode, the contents of the
> string
> thus
> > are treated as LaTeX variables and appear in italics with too much
> space.
> >
> > Any ideas on a good way to make the munger wrap the contents of a
> string,
> > perhaps with a new \HOLString command?
> >
> > My guess is this probably requires removing whatever rule pretty-prints
> strings
> > and putting in a new one, but if there's anything less heavy-weight
> that could
> > be done I'd be happy to know about it.
> >
> >
> >
> ------------------------------------------------------------------------------
> > Want fast and easy access to all the code in your enterprise? Index and
> > search up to 200,000 lines of code with a free copy of Black Duck
> > Code Sight - the same software that powers the world's largest code
> > search on Ohloh, the Black Duck Open Hub! Try it now.
> > http://p.sf.net/sfu/bds
> >
> >
> >
> > _______________________________________________
> > hol-info mailing list
> > [email protected] <mailto:[email protected]>
> > https://lists.sourceforge.net/lists/listinfo/hol-info
> >
>
>
> ________________________________
>
> The information in this e-mail may be confidential and subject to legal
> professional privilege and/or copyright. National ICT Australia Limited
> accepts no liability for any damage caused by this email or its
> attachments.
>
>
________________________________
The information in this e-mail may be confidential and subject to legal
professional privilege and/or copyright. National ICT Australia Limited accepts
no liability for any damage caused by this email or its attachments.
------------------------------------------------------------------------------
Want fast and easy access to all the code in your enterprise? Index and
search up to 200,000 lines of code with a free copy of Black Duck
Code Sight - the same software that powers the world's largest code
search on Ohloh, the Black Duck Open Hub! Try it now.
http://p.sf.net/sfu/bds
_______________________________________________
hol-info mailing list
[email protected]
https://lists.sourceforge.net/lists/listinfo/hol-info
