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 <
michael.norr...@nicta.com.au> 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
> > hol-info@lists.sourceforge.net
> > 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.
>
------------------------------------------------------------------------------
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
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
