Re: [racket-users] Adding terms to Scribble table of contents

2017-07-16 Thread Matthew Flatt
You can make a `toc-target-element` instance to add to the "on this
page" content to the left of a documentation page. I think you'll have
to use `scribble/core` for that, since `scribble/base` doesn't provide
a wrapper for it (as far as I can remember).

At Fri, 7 Jul 2017 10:45:38 -0500, Philip McGrath wrote:
> I am trying to use Scribble to document some things that are not Racket
> bindings. I can get the linking and typesetting behavior I want by building
> on top of elemtag and elemref, but I would also like the defining instances
> to be added to the table of contents in the same way as bindings defined
> using defproc and friends. Is there a mechanism to do this?
> 
> Thanks,
> Philip
> 
> -- 
> You received this message because you are subscribed to the Google Groups 
> "Racket Users" group.
> To unsubscribe from this group and stop receiving emails from it, send an 
> email to racket-users+unsubscr...@googlegroups.com.
> For more options, visit https://groups.google.com/d/optout.

-- 
You received this message because you are subscribed to the Google Groups 
"Racket Users" group.
To unsubscribe from this group and stop receiving emails from it, send an email 
to racket-users+unsubscr...@googlegroups.com.
For more options, visit https://groups.google.com/d/optout.


[racket-users] Adding terms to Scribble table of contents

2017-07-07 Thread Philip McGrath
I am trying to use Scribble to document some things that are not Racket
bindings. I can get the linking and typesetting behavior I want by building
on top of elemtag and elemref, but I would also like the defining instances
to be added to the table of contents in the same way as bindings defined
using defproc and friends. Is there a mechanism to do this?

Thanks,
Philip

-- 
You received this message because you are subscribed to the Google Groups 
"Racket Users" group.
To unsubscribe from this group and stop receiving emails from it, send an email 
to racket-users+unsubscr...@googlegroups.com.
For more options, visit https://groups.google.com/d/optout.