Syntax Highlighting in Forester for Isabelle (and More) [loc-0029]

Similar to my theme plugin for Gregorian Chants, I've implemented a simple plugin for syntax highlighted blocks using the Shiki library. Unlike the chant plugin, it doesn't self-host all the required JS but instead loads from a CDN. If this becomes problematic later I will investigate self-hosting it, but it seems that self-hosting Shiki is somewhat complicated.

I didn't use any other syntax-highlighting gizmos for Forester because I plan to write lecture notes for my upcoming course at the LSS and this would require me to support Isabelle code. The advantage of Shiki is that it supports textMate grammars, and Gerwin Klein made one for Isabelle.

Like the chant plugin, it consists of a single drop-in module of JavaScript, some changes to the stylesheet and a macro definition tree. As can be seen below, the results are quite nice:

theory Main imports Pure begin typedecl bool judgment Trueprop :: ‹bool ⇒ prop› ("(_)" 5) axiomatization False :: ‹bool› and True :: ‹bool› and conj :: ‹bool ⇒ bool ⇒ bool› (infixr "∧" 35) and disj :: ‹bool ⇒ bool ⇒ bool› (infixr "∨" 30) and implies :: ‹bool ⇒ bool ⇒ bool› (infixr "⟶" 25) and not :: ‹bool ⇒ bool› ("¬ _" [40] 40) where (* Conjunction *) conjI : "⟦ A ; B ⟧ ⟹ (A ∧ B)" and conjunct1 : "A ∧ B ⟹ A" and conjunct2 : "A ∧ B ⟹ B" end

(If it doesn't display correctly, you may need to clear your browser cache.)