From 6e1e83ff7b96c62e480729189bc27a6510f032dd Mon Sep 17 00:00:00 2001
From: rhiannon morris <rhi@rhiannon.website>
Date: Tue, 12 Jul 2022 21:19:03 +0200
Subject: [PATCH] beluga syntax

---
 style/page.css    |  22 +++++----
 syntax/beluga.xml | 123 ++++++++++++++++++++++++++++++++++++++++++++++
 2 files changed, 135 insertions(+), 10 deletions(-)
 create mode 100644 syntax/beluga.xml

diff --git a/style/page.css b/style/page.css
index 712ffb4..d04bd7b 100644
--- a/style/page.css
+++ b/style/page.css
@@ -393,13 +393,15 @@ aside {
 }
 
 
-/* syntax highlighting for maude
- * [todo] does this also look ok for other langs */
-.maude .pp { color: hsl(343deg, 100%, 40%); font-weight: 500; }
-.maude .dt { color: hsl(173deg, 100%, 24%); font-weight: 500; }
-.maude .fu { color: hsl(34deg,  100%, 30%); font-weight: 500; }
-.maude .va { color: hsl(203deg, 100%, 30%); font-weight: 500; }
-.maude .cf { color: hsl(276deg, 75%,  35%); font-weight: 500; }
-.maude .op { color: hsl(220deg, 10%,  28%); }
-.maude .co { color: hsl(221deg, 10%,  39%); font-style: italic; }
-.maude :is(.st, .fl, .dv, .sc) { color: hsl(143deg, 100%, 20%); }
+.kw { color: hsl(300deg, 60%,  30%); }
+.pp { color: hsl(343deg, 100%, 40%); font-weight: 500; }
+.dt { color: hsl(173deg, 100%, 24%); font-weight: 500; }
+.fu { color: hsl(34deg,  100%, 30%); font-weight: 500; }
+.va { color: hsl(203deg, 100%, 30%); font-weight: 500; }
+.cf { color: hsl(276deg, 75%,  35%); font-weight: 500; }
+.op { color: hsl(220deg, 40%,  33%); }
+.co { color: hsl(221deg, 10%,  39%); font-style: italic; }
+.bu { color: hsl(100deg, 85%,  30%); font-weight: 500; }
+:is(.st, .fl, .dv, .sc) { color: hsl(143deg, 100%, 20%); }
+.wa { color: hsl(350deg, 80%,  25%); text-decoration: wavy 1.5px underline; }
+.al { color: hsl(350deg, 80%,  25%); }
diff --git a/syntax/beluga.xml b/syntax/beluga.xml
new file mode 100644
index 0000000..fe93788
--- /dev/null
+++ b/syntax/beluga.xml
@@ -0,0 +1,123 @@
+<?xml version="1.0" encoding="UTF-8"?>
+<!DOCTYPE language SYSTEM "language.dtd" [
+  <!ENTITY tok_start "(?&lt;=^|\s|[(\[{}\]),:.])">
+  <!ENTITY tok_end   "(?=$|\s|[(\[{}\]),:.])">
+]>
+
+<language name="Beluga" section="Sources" extensions="*.bel"
+          version="1" kateversion="5.53">
+  <highlighting>
+    <list name="decls">
+      <item>LF</item>
+      <item>inductive</item> <item>coinductive</item>
+      <item>stratified</item> <item>typedef</item>
+      <item>schema</item>
+      <item>proof</item> <item>rec</item> <item>and</item>
+    </list>
+
+    <list name="univs"> <item>type</item> <item>ctype</item> </list>
+
+    <list name="modules">
+      <item>module</item> <item>struct</item> <item>end</item>
+    </list>
+
+    <list name="exprs">
+      <item>fn</item> <item>fun</item> <item>mlam</item>
+      <item>case</item> <item>of</item> <item>impossible</item>
+      <item>let</item> <item>in</item>
+    </list>
+
+    <list name="blocks"> <item>some</item> <item>block</item> </list>
+
+    <list name="total"> <item>total</item> </list>
+    <list name="trust"> <item>trust</item> </list>
+
+    <contexts>
+      <context attribute="default" lineEndContext="#stay" name="Default">
+        <keyword attribute="decls"     context="#stay" String="decls"     />
+        <keyword attribute="univs"     context="#stay" String="univs"     />
+        <keyword attribute="modules"   context="#stay" String="modules"   />
+        <keyword attribute="exprs"     context="#stay" String="exprs"     />
+        <keyword attribute="blocks"    context="#stay" String="blocks"    />
+        <keyword attribute="total"     context="#stay" String="total"     />
+        <keyword attribute="trust"     context="#stay" String="trust"     />
+
+        <RegExpr attribute="hole" context="#stay"
+          String="\?.+?&tok_end;" />
+
+        <RegExpr attribute="param_var" context="#stay"
+          String="&tok_start;#.+?&tok_end;" />
+        <RegExpr attribute="subst_var" context="#stay"
+          String="&tok_start;\$.+?&tok_end;" />
+
+        <RegExpr attribute="subst_const" context="#stay"
+          String="&tok_start;(\^|\.\.)&tok_end;" />
+
+        <RegExpr attribute="wildcards" context="#stay"
+          String="&tok_start;[#$]?_&tok_end;" />
+
+        <RegExpr attribute="proj" context="#stay"
+          String="\..+?&tok_end;" />
+
+        <RegExpr attribute="punc" context="#stay"
+          String="&tok_start;(:|\|-#?|-&gt;|=&gt;|\\|=|⇒|→|⊢)&tok_end;" />
+
+        <RegExpr attribute="delim" context="#stay"
+          String="[&lt;&gt;{}\[\](),|.;]" />
+
+        <DetectChar attribute="string" context="String" char="&quot;" />
+
+        <DetectChar attribute="comment" context="comment s" char="%" />
+        <Detect2Chars attribute="comment" context="comment m"
+                      char="%" char1="{" />
+      </context>
+
+      <context attribute="string" lineEndContext="#stay" name="String">
+        <!-- no escapes or whatever in strings -->
+        <DetectChar attribute="string" context="#pop" char="&quot;" />
+      </context>
+
+      <context attribute="comment" lineEndContext="#pop" name="comment s" />
+
+      <context attribute="comment" lineEndContext="#stay" name="comment m">
+        <Detect2Chars attribute="comment" context="comment m"
+                      char="%" char1="{" />
+        <Detect2Chars attribute="comment" context="#pop"
+                      char="}" char1="%" />
+      </context>
+    </contexts>
+
+    <itemDatas>
+      <itemData name="default"     defStyleNum="dsNormal"       />
+      <itemData name="decls"       defStyleNum="dsFunction"     />
+      <itemData name="univs"       defStyleNum="dsDataType"     />
+      <itemData name="modules"     defStyleNum="dsPreprocessor" />
+      <itemData name="exprs"       defStyleNum="dsControlFlow"  />
+      <itemData name="blocks"      defStyleNum="dsDataType"     />
+      <itemData name="total"       defStyleNum="dsKeyword"      />
+      <itemData name="trust"       defStyleNum="dsWarning"      />
+
+      <itemData name="hole"        defStyleNum="dsAlert"       />
+      <itemData name="param_var"   defStyleNum="dsString"       />
+      <itemData name="subst_var"   defStyleNum="dsDecVal"       />
+      <itemData name="subst_const" defStyleNum="dsBuiltIn"      />
+
+      <itemData name="wildcards"   defStyleNum="dsKeyword"      />
+      <itemData name="proj"        defStyleNum="dsVariable"     />
+
+      <itemData name="punc"        defStyleNum="dsOperator"     />
+      <itemData name="delim"       defStyleNum="dsNormal"       />
+
+      <itemData name="string"      defStyleNum="dsString"       />
+
+      <itemData name="comment"     defStyleNum="dsComment"      />
+    </itemDatas>
+  </highlighting>
+
+  <general>
+    <keywords
+      casesensitive="true"
+      additionalDeliminators="[]{}(), &#9;"
+      wordWrapDeliminators=" " />
+  </general>
+</language>