When the term list$NIL is encountered, the first phase of turning this into a
string is to figure out which name to render it with. The overload data
structure says that "NIL" should be used. The concrete syntax grammar is then
consulted for rules pertaining to NIL. The only rule it will find is the
list-form version, and this will be used.
Unfortunately, if there is a list rule for a bare term (like NIL) it will always
be used in preference to any other possible rules. So, even if you did
something like
add_rule {block_style = (AroundEachPhrase, (PP.CONSISTENT, 2)),
fixity = Closefix,
paren_style = OnlyIfNecessary,
pp_elements = [TOK "fooNIL"], term_name = "NIL"};
it wouldn’t work, and you’d still get “[]”. Given the wordiness of the above,
even if it worked, I’d have thought that
val _ = overload_on("LaTeXNIL", ``[]``);
val _ = TeX_notation {hol = "LaTeXNil", TeX = ("\\ensuremath{[\,]}", 2)};
would be preferable. You still need to do the analogue of the second line above
for the first solution too.
I take the point that nice LaTeX for [] would be preferable without having to do
anything at all.
One option might be to have the pretty-printing backends provide a “tiny-space”
API point. All but the TeX backends would do nothing with this, but the TeX
backend could generate a \, or whatever. The pretty-printer could then be
relied to generate a tiny-space every time two tokens followed each other
without interruption. Or perhaps the tiny-space would only appear between
list-form delimiters. Or perhaps users could call for it explicitly in grammar
rules...
Another option would be to maintain a set of TeX deltas (accompanying theories
as they were saved and loaded). These deltas could be overlaid on the standard
grammar when TeX-pretty-printing was due to happen. This would allow maximum
flexibility because the normal-use grammars wouldn’t get contaminated at all,
and weird pretty-printing stuff could be kept in its own silo. You can emulate
this a little at the moment by creating parallel PrettyPrinting theories that
only get pulled in when creating a TeX munger.
Michael
On 25/07/14 03:54, Ramana Kumar wrote:
> In fact I wouldn't need a new overload; if I could just get the pretty-printer
> to print the empty list as "NIL" I would be fine.
> But I haven't been able to do that. How do you get the pretty-printer to stop
> using the add_listform rule for NIL while retaining it for non-empty lists?
> I tried prefer_form_with_tok but it didn't work.
> On Thu, Jul 24, 2014 at 3:47 PM, Michael Norrish <[email protected]
> <mailto:[email protected]>> wrote:
> The latter is how I've done this in the past.
> Michael
> > On 24 Jul 2014, at 22:16, "Ramana Kumar" <[email protected]
> <mailto:[email protected]>> wrote:
> >
> > HOL's pretty-printer usually prints the empty list as "[]", which I
> believe is produced by two separate tokens (one for each bracket) via a
> "listform" parsing/printing rule.
> >
> > In LaTeX math mode (generated using HOL's math mode munger) "[]" does
> not
> look nice: it needs a bit of space inside. What would be the best approach
> to making the printer generate such space? Could I, perhaps, override the
> empty list (but not other lists) with a special token that I can then
> override to some custom LaTeX? Or perhaps there's a better way?
> >
> ------------------------------------------------------------------------------
> > 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
