Thanks! Looks pretty helpful to me; at the very least I think I can rip out the parser and interactive loop. I've already got something syntax highlighting by calling off to Pygmentize.
Might if I reuse some of that code and put it in a little scribble library? (I don't see a license) -- William J. Bowman On Thu, Feb 14, 2019 at 03:49:55PM -0800, Sorawee Porncharoenwase wrote: > I did exactly this, but for Pollen. You will want to create a new > subprocess with coqtop -emacs 2>&1. > You need -emacs because coqtop alone won’t distinguish the message panel > and the context panel, > and you need 2>&1 because Racket’s merge-input doesn’t preserve the order > when merging stderr and stdout. > > The output is needed to be parsed with regex (that’s how Emacs does it). > Note that even though the > grammar looks like XML, it will always be one level deep, so using regex is > fine here. > > - If you see <infomsg>...</infomsg>, the thing inside the tag should > appear in the message panel. > - If you see <prompt>...</prompt>, it means Coq has processed a new > command > (such as a focus or a command terminating with dot). The information > inside is not useful for me, but it might be for you. > - If you see Toplevel input, your code has an error. > > If it’s helpful (I don’t think it will), here’s my work-in-progress code > <https://github.com/sorawee/my-website/blob/master/coq-tactics/pollen.rkt#L66> > which is used to generate this page > <https://homes.cs.washington.edu/~sorawee/en/coq-tactics/>. > > On Thu, Feb 14, 2019 at 3:09 PM William J. Bowman <w...@williamjbowman.com> > wrote: > > > Does anyone have work adapting or hi-jacking scribble/examples to run code > > from > > other languages, particularly for non-sexpr languages that require calling > > out > > to an external interpreter? > > > > In particular, I want to make it work for Coq programs so I can write nice > > scribble documents with embedded Coq examples. > > I could partially reimplement a scribble/examples-like macro that spins up > > a > > subprocess to interact with coqtop, but I was hoping someone might have > > some > > work I can reuse. > > > > -- > > William J. Bowman > > > > -- > > 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.
