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 <[email protected]> > 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 [email protected]. > > 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 [email protected]. For more options, visit https://groups.google.com/d/optout.
