I am already using a special "pretty-printing" theory when creating my
munger, but I still don't know what to put in it to change printing of the
empty list. (In your email you explained why all the code snippets you
provided don't work.)
It sounds like there's no way to change how the empty list is printed
without removing the listform rule (and can it even be removed?), but of
course I want the listform rule for non-empty lists.
I think the tiny-space idea sounds like too much of a special case. What we
would want is general mechanisms for overriding the printer's behaviour
that don't have to anticipate why we want to do it.
If I understand correctly, what is missing is some way to give preference
to an overload over a listform.
On Fri, Jul 25, 2014 at 3:22 AM, Michael Norrish <
michael.norr...@nicta.com.au> wrote:
> 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 <
> michael.norr...@nicta.com.au
> > <mailto:michael.norr...@nicta.com.au>> wrote:
>
> > The latter is how I've done this in the past.
>
> > Michael
>
> > > On 24 Jul 2014, at 22:16, "Ramana Kumar" <
> ramana.ku...@cl.cam.ac.uk
> > <mailto:ramana.ku...@cl.cam.ac.uk>> 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
> > > hol-info@lists.sourceforge.net <mailto:
> 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.
>
> ________________________________
>
> 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
