Add a syntax highlighting prototype

utensil · May 27, 2024 · 9fed6cc · 9fed6cc
1 parent bc72620
commit 9fed6cc
Show file tree

Hide file tree

Showing 9 changed files with 383 additions and 8 deletions.
diff --git a/assets/latex.xsl b/assets/latex.xsl
@@ -2,6 +2,7 @@
 <!-- SPDX-License-Identifier: CC0-1.0 -->
 <xsl:stylesheet version="1.0"
                 xmlns:xsl="http://www.w3.org/1999/XSL/Transform"
+                xmlns:html="http://www.w3.org/1999/xhtml"
                 xmlns:f="http://www.jonmsterling.com/jms-005P.xml">
 
   <xsl:template match="/f:tree/f:backmatter/f:references">
@@ -221,5 +222,13 @@
     <xsl:text>}</xsl:text>
     <xsl:text>}</xsl:text>
   </xsl:template>
+
+  <xsl:template match="html:code">
+    <xsl:text>\begin{lstlisting}[mathescape=true,language=</xsl:text>
+    <xsl:value-of select="@class" />
+    <xsl:text>]</xsl:text>
+    <xsl:apply-templates />
+    <xsl:text>\end{lstlisting}</xsl:text>
+  </xsl:template>
 
 </xsl:stylesheet>
diff --git a/assets/shiki.js b/assets/shiki.js
@@ -0,0 +1,44 @@
+import { getHighlighter } from 'https://esm.sh/[email protected]'
+
+document.addEventListener('DOMContentLoaded', async () => {
+
+    const lean4res = await fetch('https://cdn.jsdelivr.net/gh/leanprover/vscode-lean4@master/vscode-lean4/syntaxes/lean4.json')
+
+    console.log(lean4res)
+
+    if(!lean4res.ok) {
+        console.error('Failed to fetch lean4.json')
+    }
+    let lean4json;
+    try {
+        lean4json = await lean4res.json()
+    } catch(err) {
+      console.error(err);
+    }
+
+    const codes = document.querySelectorAll('code')
+        codes.forEach(async code => {
+            let lang = code.getAttribute('class') || 'plaintext'
+            let langAlias = {}
+
+            if((lang == 'lean4' || lang == 'lean') && lean4json) {
+                lang = lean4json
+                langAlias = { 
+                    lean4: 'Lean 4',
+                    lean: 'Lean 4'
+                }
+            }
+
+            const highlighter = await getHighlighter({
+                langs: [lang],
+                langAlias,
+                themes: ['one-dark-pro'],
+            })
+
+            const html = await highlighter.codeToHtml(
+                code.textContent.replaceAll(/^\n/g, '').replaceAll(/\n$/g, ''),
+                { lang, theme: 'one-dark-pro' }
+            )
+            code.innerHTML = html
+        })
+})
diff --git a/assets/uts-layout.xsl b/assets/uts-layout.xsl
@@ -30,6 +30,8 @@
           <xsl:value-of select="/f:tree/f:frontmatter/f:title" />
         </title>
         <script src="https://cdn.jsdelivr.net/gh/iconfu/[email protected]/dist/svg-inject.min.js"></script>
+        <script type="module" src="shiki.js">
+        </script>
         <script src="uts-forester.js"></script>
       </head>
       <body>

diff --git a/trees/ca-0001.tree b/trees/ca-0001.tree
@@ -65,4 +65,8 @@
       }
     }
   }
+}
+
+\block{Scracthpad}{
+  \transclude{math-0001}
 }
diff --git a/trees/code.tex b/trees/code.tex
@@ -0,0 +1,13 @@
+\usepackage{listings}
+
+% handle Lean code highlighting following https://lean-lang.org/lean4/doc/syntax_highlight_in_latex.html
+\definecolor{keywordcolor}{rgb}{0.7, 0.1, 0.1}   % red
+\definecolor{tacticcolor}{rgb}{0.0, 0.1, 0.6}    % blue
+\definecolor{commentcolor}{rgb}{0.4, 0.4, 0.4}   % grey
+\definecolor{symbolcolor}{rgb}{0.0, 0.1, 0.6}    % blue
+\definecolor{sortcolor}{rgb}{0.1, 0.5, 0.1}      % green
+\definecolor{attributecolor}{rgb}{0.7, 0.1, 0.1} % red
+
+\def\lstlanguagefiles{../trees/lstlean.tex}
+% set default language
+\lstset{language=lean}
diff --git a/trees/lstlean.tex b/trees/lstlean.tex
@@ -0,0 +1,289 @@
+% Listing style definition for the Lean Theorem Prover.
+% Defined by Jeremy Avigad, 2015, by modifying Assia Mahboubi's SSR style.
+% Unicode replacements taken from Olivier Verdier's unixode.sty
+
+\lstdefinelanguage{lean} {
+
+% Anything between $ becomes LaTeX math mode
+mathescape=false,
+% Comments may or not include Latex commands
+texcl=false,
+
+% keywords, list taken from lean-syntax.el
+morekeywords=[1]{
+import, prelude, protected, private, noncomputable, definition, meta, renaming,
+hiding, parameter, parameters, begin, constant, constants,
+lemma, variable, variables, theory,
+print, theorem, example,
+open, as, export, override, axiom, axioms, inductive, with,
+structure, record, universe, universes,
+alias, help, precedence, reserve, declare_trace, add_key_equivalence,
+match, infix, infixl, infixr, notation, postfix, prefix, instance,
+eval, reduce, check, end, this,
+using, using_well_founded, namespace, section,
+attribute, local, set_option, extends, include, omit, class,
+raw, replacing,
+calc, have, show, suffices, by, in, at, let, forall, Pi, fun,
+exists, if, dif, then, else, assume, obtain, from, register_simp_ext, unless, break, continue,
+mutual, do, def, run_cmd, const,
+partial, mut, where, macro, syntax, deriving,
+return, try, catch, for, macro_rules, declare_syntax_cat, abbrev},
+
+% Sorts
+morekeywords=[2]{Sort, Type, Prop},
+
+% tactics, list taken from lean-syntax.el
+morekeywords=[3]{
+assumption,
+apply, intro, intros, allGoals,
+generalize, clear, revert, done, exact,
+refine, repeat, cases, rewrite, rw,
+simp, simp_all, contradiction,
+constructor, injection,
+induction,
+},
+
+% modifiers, taken from lean-syntax.el
+% note: 'otherkeywords' is needed because these use a different symbol.
+% this command doesn't allow us to specify a number -- they are put with [1]
+% otherkeywords={
+% [persistent], [notation], [visible], [instance], [trans_instance],
+% [class], [parsing-only], [coercion], [unfold_full], [constructor],
+% [reducible], [irreducible], [semireducible], [quasireducible], [wf],
+% [whnf], [multiple_instances], [none], [decl], [declaration],
+% [relation], [symm], [subst], [refl], [trans], [simp], [congr], [unify],
+% [backward], [forward], [no_pattern], [begin_end], [tactic], [abbreviation],
+% [reducible], [unfold], [alias], [eqv], [intro], [intro!], [elim], [grinder],
+% [localrefinfo], [recursor]
+% },
+
+% Various symbols
+literate=
+{α}{{\ensuremath{\mathrm{\alpha}}}}1
+{β}{{\ensuremath{\mathrm{\beta}}}}1
+{γ}{{\ensuremath{\mathrm{\gamma}}}}1
+{δ}{{\ensuremath{\mathrm{\delta}}}}1
+{ε}{{\ensuremath{\mathrm{\varepsilon}}}}1
+{ζ}{{\ensuremath{\mathrm{\zeta}}}}1
+{η}{{\ensuremath{\mathrm{\eta}}}}1
+{θ}{{\ensuremath{\mathrm{\theta}}}}1
+{ι}{{\ensuremath{\mathrm{\iota}}}}1
+{κ}{{\ensuremath{\mathrm{\kappa}}}}1
+{μ}{{\ensuremath{\mathrm{\mu}}}}1
+{ν}{{\ensuremath{\mathrm{\nu}}}}1
+{ξ}{{\ensuremath{\mathrm{\xi}}}}1
+{π}{{\ensuremath{\mathrm{\mathnormal{\pi}}}}}1
+{ρ}{{\ensuremath{\mathrm{\rho}}}}1
+{σ}{{\ensuremath{\mathrm{\sigma}}}}1
+{τ}{{\ensuremath{\mathrm{\tau}}}}1
+{φ}{{\ensuremath{\mathrm{\varphi}}}}1
+{χ}{{\ensuremath{\mathrm{\chi}}}}1
+{ψ}{{\ensuremath{\mathrm{\psi}}}}1
+{ω}{{\ensuremath{\mathrm{\omega}}}}1
+
+{Γ}{{\ensuremath{\mathrm{\Gamma}}}}1
+{Δ}{{\ensuremath{\mathrm{\Delta}}}}1
+{Θ}{{\ensuremath{\mathrm{\Theta}}}}1
+{Λ}{{\ensuremath{\mathrm{\Lambda}}}}1
+{Σ}{{\ensuremath{\mathrm{\Sigma}}}}1
+{Φ}{{\ensuremath{\mathrm{\Phi}}}}1
+{Ξ}{{\ensuremath{\mathrm{\Xi}}}}1
+{Ψ}{{\ensuremath{\mathrm{\Psi}}}}1
+{Ω}{{\ensuremath{\mathrm{\Omega}}}}1
+
+{ℵ}{{\ensuremath{\aleph}}}1
+
+{≤}{{\ensuremath{\leq}}}1
+{≥}{{\ensuremath{\geq}}}1
+{≠}{{\ensuremath{\neq}}}1
+{≈}{{\ensuremath{\approx}}}1
+{≡}{{\ensuremath{\equiv}}}1
+{≃}{{\ensuremath{\simeq}}}1
+
+{≤}{{\ensuremath{\leq}}}1
+{≥}{{\ensuremath{\geq}}}1
+
+{∂}{{\ensuremath{\partial}}}1
+{∆}{{\ensuremath{\triangle}}}1 % or \laplace?
+
+{∫}{{\ensuremath{\int}}}1
+{∑}{{\ensuremath{\mathrm{\Sigma}}}}1
+{Π}{{\ensuremath{\mathrm{\Pi}}}}1
+
+{⊥}{{\ensuremath{\perp}}}1
+{∞}{{\ensuremath{\infty}}}1
+{∂}{{\ensuremath{\partial}}}1
+
+{∓}{{\ensuremath{\mp}}}1
+{±}{{\ensuremath{\pm}}}1
+{×}{{\ensuremath{\times}}}1
+
+{⊕}{{\ensuremath{\oplus}}}1
+{⊗}{{\ensuremath{\otimes}}}1
+{⊞}{{\ensuremath{\boxplus}}}1
+
+{∇}{{\ensuremath{\nabla}}}1
+{√}{{\ensuremath{\sqrt}}}1
+
+{⬝}{{\ensuremath{\cdot}}}1
+{•}{{\ensuremath{\cdot}}}1
+{∘}{{\ensuremath{\circ}}}1
+
+%{⁻}{{\ensuremath{^{\textup{\kern1pt\rule{2pt}{0.3pt}\kern-1pt}}}}}1
+{⁻}{{\ensuremath{^{-}}}}1
+{▸}{{\ensuremath{\blacktriangleright}}}1
+
+{∧}{{\ensuremath{\wedge}}}1
+{∨}{{\ensuremath{\vee}}}1
+{¬}{{\ensuremath{\neg}}}1
+{⊢}{{\ensuremath{\vdash}}}1
+
+%{⟨}{{\ensuremath{\left\langle}}}1
+%{⟩}{{\ensuremath{\right\rangle}}}1
+{⟨}{{\ensuremath{\langle}}}1
+{⟩}{{\ensuremath{\rangle}}}1
+
+{↦}{{\ensuremath{\mapsto}}}1
+{←}{{\ensuremath{\leftarrow}}}1
+{<-}{{\ensuremath{\leftarrow}}}1
+{→}{{\ensuremath{\rightarrow}}}1
+{↔}{{\ensuremath{\leftrightarrow}}}1
+{⇒}{{\ensuremath{\Rightarrow}}}1
+{⟹}{{\ensuremath{\Longrightarrow}}}1
+{⇐}{{\ensuremath{\Leftarrow}}}1
+{⟸}{{\ensuremath{\Longleftarrow}}}1
+
+{∩}{{\ensuremath{\cap}}}1
+{∪}{{\ensuremath{\cup}}}1
+{⊂}{{\ensuremath{\subseteq}}}1
+{⊆}{{\ensuremath{\subseteq}}}1
+{⊄}{{\ensuremath{\nsubseteq}}}1
+{⊈}{{\ensuremath{\nsubseteq}}}1
+{⊃}{{\ensuremath{\supseteq}}}1
+{⊇}{{\ensuremath{\supseteq}}}1
+{⊅}{{\ensuremath{\nsupseteq}}}1
+{⊉}{{\ensuremath{\nsupseteq}}}1
+{∈}{{\ensuremath{\in}}}1
+{∉}{{\ensuremath{\notin}}}1
+{∋}{{\ensuremath{\ni}}}1
+{∌}{{\ensuremath{\notni}}}1
+{∅}{{\ensuremath{\emptyset}}}1
+
+{∖}{{\ensuremath{\setminus}}}1
+{†}{{\ensuremath{\dag}}}1
+
+{ℕ}{{\ensuremath{\mathbb{N}}}}1
+{ℤ}{{\ensuremath{\mathbb{Z}}}}1
+{ℝ}{{\ensuremath{\mathbb{R}}}}1
+{ℚ}{{\ensuremath{\mathbb{Q}}}}1
+{ℂ}{{\ensuremath{\mathbb{C}}}}1
+{⌞}{{\ensuremath{\llcorner}}}1
+{⌟}{{\ensuremath{\lrcorner}}}1
+{⦃}{{\ensuremath{\{\!|}}}1
+{⦄}{{\ensuremath{|\!\}}}}1
+
+{‖}{{\ensuremath{\|}}}1
+{₁}{{\ensuremath{_1}}}1
+{₂}{{\ensuremath{_2}}}1
+{₃}{{\ensuremath{_3}}}1
+{₄}{{\ensuremath{_4}}}1
+{₅}{{\ensuremath{_5}}}1
+{₆}{{\ensuremath{_6}}}1
+{₇}{{\ensuremath{_7}}}1
+{₈}{{\ensuremath{_8}}}1
+{₉}{{\ensuremath{_9}}}1
+{₀}{{\ensuremath{_0}}}1
+{ᵢ}{{\ensuremath{_i}}}1
+{ⱼ}{{\ensuremath{_j}}}1
+{ₐ}{{\ensuremath{_a}}}1
+
+{¹}{{\ensuremath{^1}}}1
+
+{ₙ}{{\ensuremath{_n}}}1
+{ₘ}{{\ensuremath{_m}}}1
+{ₚ}{{\ensuremath{_p}}}1
+{↑}{{\ensuremath{\uparrow}}}1
+{↓}{{\ensuremath{\downarrow}}}1
+
+{...}{{\ensuremath{\ldots}}}1
+{·}{{\ensuremath{\cdot}}}1
+
+{▸}{{\ensuremath{\triangleright}}}1
+
+{Σ}{{\color{symbolcolor}\ensuremath{\Sigma}}}1
+{Π}{{\color{symbolcolor}\ensuremath{\Pi}}}1
+{∀}{{\color{symbolcolor}\ensuremath{\forall}}}1
+{∃}{{\color{symbolcolor}\ensuremath{\exists}}}1
+{λ}{{\color{symbolcolor}\ensuremath{\mathrm{\lambda}}}}1
+{\$}{{\color{symbolcolor}\$}}1
+
+{:=}{{\color{symbolcolor}:=}}1
+{=}{{\color{symbolcolor}=}}1
+{<|>}{{\color{symbolcolor}<|>}}1
+{<\$>}{{\color{symbolcolor}<\$>}}1
+{+}{{\color{symbolcolor}+}}1
+{*}{{\color{symbolcolor}*}}1,
+
+% Comments
+%comment=[s][\itshape \color{commentcolor}]{/-}{-/},
+morecomment=[s][\color{commentcolor}]{/-}{-/},
+morecomment=[l][\itshape \color{commentcolor}]{--},
+
+% Spaces are not displayed as a special character
+showstringspaces=false,
+
+% keep spaces
+keepspaces=true,
+
+% String delimiters
+morestring=[b]",
+morestring=[d],
+
+% Size of tabulations
+tabsize=3,
+
+% Enables ASCII chars 128 to 255
+extendedchars=false,
+
+% Case sensitivity
+sensitive=true,
+
+% Automatic breaking of long lines
+breaklines=true,
+breakatwhitespace=true,
+
+% Default style fors listingsred
+basicstyle=\ttfamily\small,
+
+% Position of captions is bottom
+captionpos=b,
+
+% Full flexible columns
+columns=[l]fullflexible,
+
+
+% Style for (listings') identifiers
+identifierstyle={\ttfamily\color{black}},
+% Note : highlighting of Coq identifiers is done through a new
+% delimiter definition through an lstset at the beginning of the
+% document. Don't know how to do better.
+
+% Style for declaration keywords
+keywordstyle=[1]{\ttfamily\color{keywordcolor}},
+
+% Style for sorts
+keywordstyle=[2]{\ttfamily\color{sortcolor}},
+
+% Style for tactics keywords
+keywordstyle=[3]{\ttfamily\color{tacticcolor}},
+
+% Style for attributes
+keywordstyle=[4]{\ttfamily\color{attributecolor}},
+
+% Style for strings
+stringstyle=\ttfamily,
+
+% Style for comments
+commentstyle={\ttfamily\footnotesize },
+
+}
-Original file line number
+Diff line change
@@ Expand Up / @@ -65,4 +65,8 @@ @@
           }
         }
       }
+    }
+    \block{Scracthpad}{
+      \transclude{math-0001}
     }