Re: [isabelle] Juxtaposed cartouche error in session run; okay in PIDE



On Sat, 14 Nov 2015, Gottfried Barrow wrote:

I end this mentioning three "features", some outer syntax commands that get interpreted as LaTeX newtheorem environments, where the source that follows is put in a fancyverb environment with line numbers, directly underneath the newtheorem title. The 3rd feature would be "subtle" syntax that gets interpreted as a very specific LaTeX equation environment.

I ask, "Do these features exist?", and, "If they don't, should you make implementing them a priority just for me?"

There is already a "tag" feature that allows to wrap Isabelle document commands (like 'text') or other formal command (e.g. proof commands) in a LaTeX environment.

An example can be seen here:
http://isabelle.in.tum.de/repos/isabelle/file/Isabelle2015/src/Doc/Implementation/ML.thy#l563
http://isabelle.in.tum.de/repos/isabelle/file/Isabelle2015/src/Doc/Implementation/document/style.sty#l39


Maybe that is already sufficient to implement all 3 points above.


	Makarius




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