[isabelle-dev] colored TeX-snippets

[Christian Sternagel]

Dear all,

when preparing slides I often want to have colored TeX-snippets. In the 
past what I often did, was write my Isabelle snippet by hand and color 
it using e.g. the listings package of LaTeX. That's of course a bit 
error-prone and inconvenient.

To this end, I wanted to write an isabellecolor.sty package which just 
uses some user defined colors (by default the same colors as jEdit) for 
TeX-snippets.

There where several obstacles (some of which I could not overcome (yet)):

1) The current document preparation system does not have markups for, 
e.g., bound variables, free variables, constants, ...

Thus I applied the trivial patch:

diff -r 72efd6b4038d src/Pure/Thy/latex.ML
--- a/src/Pure/Thy/latex.ML     Mon Nov 12 23:24:40 2012 +0100
+++ b/src/Pure/Thy/latex.ML     Tue Nov 13 16:35:30 2012 +0900
@@ -182,6 +182,20 @@
      then ("\\isacommand{", "}")
    else if s = Isabelle_Markup.keywordN orelse s = 
Isabelle_Markup.keyword2N
      then ("\\isakeyword{", "}")
+  else if s = Isabelle_Markup.constantN
+    then ("\\isaconstant{", "}")
+  else if s = Isabelle_Markup.tfreeN
+    then ("\\isatfree{", "}")
+  else if s = Isabelle_Markup.tvarN
+    then ("\\isatvar{", "}")
+  else if s = Isabelle_Markup.freeN
+    then ("\\isafree{", "}")
+  else if s = Isabelle_Markup.skolemN
+    then ("\\isaskolem{", "}")
+  else if s = Isabelle_Markup.boundN
+    then ("\\isabound{", "}")
+  else if s = Isabelle_Markup.varN
+    then ("\\isavar{", "}")
    else Markup.no_output;

to src/Pure/Thy/latex.ML and added the following to isabelle.sty:

% identifier markup
\newcommand{\isaconstant}[1]{#1}
\newcommand{\isatfree}[1]{#1}
\newcommand{\isatvar}[1]{#1}
\newcommand{\isafree}[1]{#1}
\newcommand{\isaskolem}[1]{#1}
\newcommand{\isabound}[1]{#1}
\newcommand{\isavar}[1]{#1}

i.e., the default is to do nothing. On top of this I added 
isabellecolor.sty as attached. For plain antiquotations this works well, 
however ...

2) Theory sources (and hence also TeX-snippets from theory sources that 
are not produced via antiquotations) do not seem to include markup 
information. Obviously this information is available at some point 
(e.g., the highlighted source text inside Isabelle/jEdit). Now, my 
questions:
   - what are the Isabelle/Scala files that use markup information to 
color source text in jEdit?
   - is there already a plan to use the same machinery for document 
preparation? if not, would there be interest in having such a thing?
-------------- next part --------------
A non-text attachment was scrubbed...
Name: isabellecolor.sty
Type: text/x-tex
Size: 2689 bytes
Desc: not available
URL: <https://mailmanbroy.informatik.tu-muenchen.de/pipermail/isabelle-dev/attachments/20121113/03085bf1/attachment.sty>