[isabelle-dev] colored TeX-snippets

[Makarius]

On Tue, 13 Nov 2012, Christian Sternagel wrote:

> 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.

Note that these editor color schemes are not very persistent of time.  I 
remember when people were imitating the "classic" XEmacs 21.4 + PG 3.x 
scheme in their slides, just before the switch to GNU Emacs 22 + PG 4. 
And of course, the one true style is XEmacs 21.1 + PG 2.x, as seen in this 
screenshot from 1999: 
http://isabelle.in.tum.de/Isar/pg-isar-screenshot.png

jEdit default colors are occasionally seen in popular culture, but there 
are many specific Isabelle/jEdit colors and I've recently added plugin 
options to change all that.


> 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;

The function patched above is Latex.latex_markup and installed via 
Markup.add_mode, so it can be easily changed in user space, by inventing a 
new print mode and including that in the list of active modes when 
producing the document.

There might have been reasons for not having this markup in the output, 
but I can't remember it on the spot.  The Isabelle document preparation 
system is still awaiting many reforms and catching up.

The next big reform will probably expose the XML document tree to some 
user functions to be mangled in arbitrary ways.


> 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?

That is all part of the next reform.  The document markup is accumulated 
on the Isabelle/Scala side, but document preparation happens in 
Isabelle/ML, so some rethinking is required.  See 
http://isabelle.in.tum.de/repos/isabelle/file/dea9363887a6/src/Tools/jEdit/src/rendering.scala 
for the interpretation of document markup in terms of GUI metaphors of 
Java Graphics2D, Swing, jEdit.  The latex output works quite differently 
at the moment.

When I get a chance to revisit the document preparation problem, the next 
step will be to re-unify HTML generation with the editor view, probably by 
pulling it to the Scala side.

The Latex part is much harder to change, also because so many smart tricks 
have been devised over the years to achieve certain effects.  Tiny changes 
there easily invoke the wrath of followers of that black art.


 	Makarius