proofcraft.org

Isabelle Syntax Highlighting in Markdown and HTML

The Short Version

The syntax highlighter pygments now supports Isabelle.

You can use it together with tools like pandoc to embed Isabelle code in markdown, html, or other pandoc source languages. You can even generate RTF documents with highlighted Isabelle code and talk to people who speak MS Word.

Example

In markdown source, text like the following

Sample text with inline `\<Gamma> \<turnstile> e :: t`{.isa} Isabelle formulas and
a fenced Isabelle code block.

```{.isa}
   definition x where "x \<equiv> y\<^sup>2"
```

turns into nicely rendered HTML:

Sample text with inline Γ ⊢ e :: t Isabelle formulas and a fenced Isabelle code block.

   definition x where "x ≡ y\<^sup>2"

Since pygments is fairly comfortable with Unicode, you can even just copy source from Isabelle/jEdit, including already rendered symbols, and paste it into markdown:

```{.isa}
lemma exec1_appendR: "P ⊢ c → c' ⟹ P@P' ⊢ c → c'"
```

becomes

lemma exec1_appendR: "P ⊢ c → c' ⟹ P@P' ⊢ c → c'"

Cool! What do I need to do?

The basics first:

• The current release version of pygments has support for highlighting, but not yet for symbols and sub/super scripts. If you want the latter, you will need to run the source version from my pygments development branch https://bitbucket.org/lsf37/pygments-main (pull requests are submitted to the pygments team, so hopefully this won’t be necessary any more in the not too distant future):

  hg clone https://bitbucket.org/lsf37/pygments-main

• Make sure you’re on the all branch:

  hg up all

• Add pygmentize to your PATH

  export PATH=~/pygments-main/:$PATH

• Run it on a theory file to test. E.g.:

  pygmentize ~/isabelle/src/HOL/Taylor.thy This should print the theory file highlighted on the terminal. You might need additional python packages. Any easy way to get them is to install standard pygments first on your system (e.g. through ports or homebrew on the Mac, or your system package manager in Linux).

• If your terminal font has Unicode symbols and you run

  pygmentize -F symbols ~/isabelle/src/HOL/Taylor.thy you should now see those symbols show up. If not, you’ll probably see boxes. (-F is the command line option for running a filter. The symbols filter replaces Isabelle symbol sequences with their Unicode counterparts.)

If the last two steps worked, you now have a working pygments install that understands Isabelle.

Markdown and HTML

Now, there is a lot of choice. You could run any markdown engine that natively supports pygments, there are plenty of these. You could also run pygments directly in html generators like jekyll.

I happen to like pandoc for markdown rendering, but you first have to tell it to use pygments instead of its own syntax highlighter. Which you can do by putting something like the following into a file pygdoc.hs:

#!/usr/bin/env runhaskell

-- A Pandoc filter for using pygments syntax highlighting
-- loosely based on Matti Pastell's 2011 filters in https://bitbucket.org/mpastell/pandoc-filters/

import Text.Pandoc.JSON
import System.Process (readProcess)
import System.IO.Unsafe

main :: IO ()
main = toJSONFilter highlight

highlight :: Block -> Block
highlight c@(CodeBlock (_, [] , _ ) code) = c
highlight (CodeBlock (_, "isa":options , _ ) code) = RawBlock (Format "html") (pygments code ("isabelle":options))
highlight (CodeBlock (_, opts@(lang:options) , _ ) code) = RawBlock (Format "html") (pygments code opts)
highlight x = x

highlightIn :: Inline -> Inline
highlightIn (Code (_, ["isa"] , _ ) code) = RawInline (Format "html") ("<code>" ++ pygments_nowrap code ++ "</code>")
highlightIn x = x

std_opts :: [String]
std_opts = ["-f", "html", "-F", "symbols"]

line_nos :: [String]
line_nos = ["-O", "linenos=inline"]

lang :: String-> [String]
lang lg = ["-l", lg]

invoke_pygments :: [String] -> String -> String
invoke_pygments params code = unsafePerformIO $ readProcess "pygmentize" (std_opts ++ params) code

pygments_nowrap :: String -> String
pygments_nowrap code = head (lines (invoke_pygments (lang "isabelle" ++ ["-O", "nowrap"]) code))

pygments :: String -> [String] -> String
pygments code [lg]      = invoke_pygments (lang lg) code
pygments code [lg,nums] = invoke_pygments (lang lg ++ line_nos) code
pygments code _         = error "other pygments options not implemented"

(I did say quick and dirty. Feel free to improve…). Compile it with

ghc --make pygdoc.hs

And run pandoc with something like

pandoc -s --css hilite.css --filter ./pygdoc -o README.html README.md

The options mean:

• -s: produce a standalone html file with headers etc
• --css hilite.css: include a link to the style file hilite.css
• --filter ./pygdoc: this slots in our pygments filter
• -o README.html: the output file
• README.md: the input file

You don’t have to write hilite.css yourself. You can generate it with pygments for the theme you like (here default) with

pygmentize -S default -f html > hilite.css	

Font

With Isabelle symbols, you might not want to trust that every user’s browser and its fonts support all Unicode symbols in exactly the way Isabelle/jEdit renders them. Luckily, the Isabelle font is part of the Isabelle distribution (lib/fonts/IsabelleText.ttf), and you can just include it in your own CSS with the @font-face directive. For instance:

@font-face {
    font-family: isabelle;
    src: url('IsabelleText.ttf');
}

.highlight pre {
    font-family: isabelle;
}

Github

Github now also recognizes Isabelle syntax and performs at least rudimentary highlighting (no symbol and sub/super script support here yet). For example, have a look at the List theory on github.

The highlighting is based on a TextMate grammar definition that I maintain on github. Of course, you can also just use this bundle to highlight Isabelle files in TextMate.

If you have ideas how to implement support symbols and sub/super scripts on github, let me know. It would definitely improve readability of Isabelle sources there.

Limitations

Obviously, an external highlighter like pygments will never have as much semantic information available as Isabelle itself (or any, really). The highlighting is mostly based on keywords and a few regular expressions, so don’t expect too much of it. It will passably recognize most of outer syntax, it won’t have any idea about inner syntax, type information, free or bound variables, declared constants or other semantic concepts. The idea is to increase readability a bit, not to rebuild an IDE in Python.

The inline code block support in the Haskell/pandoc filter above is a bit patchy: it expects an outer syntax entity like a definition (because pygments expects to render a .thy file), but often what you will want to mention in inline code blocks is actually a term fragment with a few symbols. In the form above, you’d have to at least sometimes include string quotes to indicate that pygments should render inner syntax (mostly just symbols). You could tweak the Haskell code to do that automatically for you if that is something that occurs frequently in your text.

The highlighter also renders RTF, LaTeX and other formats. RTF works surprisingly well. LaTeX support is less stellar (no sybmols at the moment), but for LaTeX you should use Isabelle’s excellent builtin antiquotations and formally checked sources for document generation anyway.

Feedback and improvements are welcome.

Happy highlighting!