On Fri, Jul 25, 2014 at 7:18 AM, Michael Norrish <
michael.norr...@nicta.com.au> wrote:
> No, the overload_on approach works.
>
Confirmed. Thanks!
> It works because the handling of list$NIL chooses the name "LaTeXNIL" for
> it,
> and this isn't then picked up by the concrete syntax phase (only "NIL" is).
>
I see.
>
> Normal lists will print as per the list-form rule.
>
> Michael
>
> On 25/07/14 16:10, Ramana Kumar wrote:
> > 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
> > <mailto: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>
> > > <mailto: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>
> > > <mailto: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>
> > <mailto: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
> >
>
>
> ________________________________
>
> 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
