my forest
1\import{shiki-macros}
2\date{2025-11-09}
3\title{Syntax Highlighting in Forester for Isabelle (and More)}
4\author{liamoc}
5\p{Similar to my [theme plugin for Gregorian Chants](loc-0015), I've implemented a simple plugin for syntax highlighted blocks using the [Shiki](https://shiki.style) 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. }
6\p{I didn't use any other syntax-highlighting gizmos for Forester because I plan to write [lecture notes](isa-0001) for my upcoming [course at the LSS](loc-0028) and this would require me to support Isabelle code. The advantage of Shiki is that it supports textMate grammars, and [[gklein]] made [one for Isabelle](https://github.com/lsf37/Isabelle.tmbundle).}
7\p{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:}
8\put\shiki/language{Isabelle Theory}
9\shiki{theory Main imports Pure
10begin
11typedecl bool
12judgment Trueprop :: ‹bool ⇒ prop› ("(_)" 5)
13
14axiomatization
15 False :: ‹bool› and True :: ‹bool› and
16 conj :: ‹bool ⇒ bool ⇒ bool› (infixr "∧" 35) and
17 disj :: ‹bool ⇒ bool ⇒ bool› (infixr "∨" 30) and
18 implies :: ‹bool ⇒ bool ⇒ bool› (infixr "⟶" 25) and
19 not :: ‹bool ⇒ bool› ("¬ _" [40] 40)
20where
21 (* Conjunction *)
22 conjI : "⟦ A ; B ⟧ ⟹ (A ∧ B)" and
23 conjunct1 : "A ∧ B ⟹ A" and
24 conjunct2 : "A ∧ B ⟹ B"
25end}
26\p{(If it doesn't display correctly, you may need to clear your browser cache.)}