[isabelle] Poor man's LaTeX markup for Isabelle listings

Dear Isabelle community,

I frequently need to include Isabelle source code listings in my LaTeX
documents.  However I have not yet figured out how to make Isabelle's
document preparation machinery export LaTeX snippets.  I know it's
possible, but I haven't had the time.  Moreover I often need to deviate
from my verbatim formalisation for didactic purposes.

I'm sure this has been done before, and I'm sure one could realise a
more advanced solution by reusing parts of the *.sty files that come
with Isabelle, but anyway I quickly hacked this LaTeX package together
from scratch, which does part of the job:


If you check out https://github.com/clange/latex you may find a few more
useful LaTeX packages.  In
https://github.com/clange/latex/blob/master/lstsemantic.sty#L20 you will
see that I have also tried this with the "listings" package, but gave up
quite soon, because the result didn't look nice.



Christoph Lange, School of Computer Science, University of Birmingham
http://cs.bham.ac.uk/~langec/, Skype duke4701

→ Mathematics in Computer Science Special Issue on “Enabling Domain
  Experts to use Formalised Reasoning”; submission until 31 October.

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.