try and fail to fix maude tokenising

Makefile

@@ -36,8 +36,8 @@ EXECS = \
 CABAL_FLAGS ?= -O -v0
 
 SYNTAXDIR := syntax
-SYNTAXFLAGS = \
-  $(patsubst %,--syntax-definition=%,$(shell find $(SYNTAXDIR) -name '*.xml'))
+SYNTAXFILES != find $(SYNTAXDIR) -name *.xml
+SYNTAXFLAGS = $(patsubst %,--syntax-definition=%,$(SYNTAXFILES))
 
 .PHONY: all
 all: build
@@ -46,7 +46,7 @@ all: build
 build: $(EXECS) $(OUTPUT)
 
 
-POSTDEPS = $(TEMPLATEDIR)/* $(LANGFILTER) $(LAANTAS_SCRIPT)
+POSTDEPS = $(TEMPLATEDIR)/* $(LANGFILTER) $(LAANTAS_SCRIPT) $(SYNTAXFILES)
 
 $(TMPDIR)/all-tags.md $(TMPDIR)/tags.mk &: $(POSTS) $(ALL_TAGS)
 	@echo "[all-tags]"

lang

@@ -1 +1 @@
-Subproject commit 3a878590c2a15764d5b6e8d4c80bfbc92714f2ae
+Subproject commit 604da055e463ebe3990334485a7e08f6c900992c

posts/2022-03-14-digitle-in-maude.md

@@ -40,24 +40,31 @@ going into one. since digitle involves numbers, i'm also importing the `NAT`
 module, and saying that any time `M` or `N` show up in equations or rewrite
 rules they stand for single numbers.
 
-<aside>
-  **why is importing called `protecting`?** in maude, sorts (approximately,
-  types) aren't necessarily closed. you can add a new constructor, or equations
-  between constructor forms, at any time. unlike in languages like haskell or
-  rust, constructors don't have to be _free_, which means you can have equations
-  like `s (s (s (s z))) = z` and pow you've got $\mathbb{Z}/4\mathbb{Z}$.
+:::aside
+**why is importing called `protecting`?** in maude, sorts (approximately,
+types) aren't necessarily closed. you can add a new constructor, or equations
+between constructor forms, at any time. unlike in languages like haskell or
+rust, constructors don't have to be _free_, which means you can have equations
+between them. like to get `ℤ/4ℤ` you can just do something like
 
-  but when you're importing a module, most of the time you don't want to do any
-  of that. so there are three ways of importing a module to express how much you
-  intend to mess with it. `protecting` says you are not adding new constructors
-  or conflating existing ones. `extending` lets you add new constructors, but
-  not new equations. `including` lets you do whatever. since i'm just using
-  _normal_ numbers, `protecting` is what i want.
+```maude
+fmod NAT4 is
+  including NAT .
+  eq 4 = 0 .
+endfm
+```
 
-  an important caveat is that it is not possible for maude itself to check you
-  are telling the truth here, but it can ask `yices` or `cvc4` for help. please
-  don't press me for more detail i have never used this
-</aside>
+but when you're importing a module, most of the time you don't want to do any
+of that. so there are three ways of importing a module to express how much you
+intend to mess with it. `protecting` says you are not adding new constructors
+or conflating existing ones. `extending` lets you add new constructors, but
+not new equations. `including` lets you do whatever. since i'm just using
+_normal_ numbers, `protecting` is what i want.
+
+an important caveat is that it is not possible for maude itself to check you
+are telling the truth here, but it can ask `yices` or `cvc4` for help. please
+don't press me for more detail i have never used this
+:::
 
 the first thing i need is a ~~type~~ sort for the pool of numbers we currently
 have. it's a _multiset_: the number of copies of each number matters, but the
@@ -93,13 +100,13 @@ mean, so later when i have some equations and rewrite rules that match on the
 beginning of a list, it knows that it can actually pick those numbers from
 _anywhere_, without needing extra rules to shuffle the list around manually.
 
-<aside>
-  **the name `__` is pretty weird!** generally operator names are written with an
-  underscore where the arguments go, so the name of the addition operator is
-  `_+_`. in this case, there _is_ no operator, it's just two things next to each
-  other (in a context where a `Pool` value is expected, anyway), so it's just
-  two underscores.
-</aside>
+:::aside
+**the name `__` is pretty weird!** generally operator names are written with an
+underscore where the arguments go, so the name of the addition operator is
+`_+_`. in this case, there _is_ no operator, it's just two things next to each
+other (in a context where a `Pool` value is expected, anyway), so it's just
+two underscores.
+:::
 
 from here, we *could* just define the rewrite rules and be done. something like
 this would work:
@@ -111,9 +118,14 @@ rl  [mul] : M N  =>  M * N .
 crl [div] : M N  =>  M quo N if M rem N = 0 .
 ```
 
-<aside>
-  **`sd`** is "symmetric difference"---e.g. `sd(1, 4) = sd(4, 1) = 3`.
-</aside>
+:::aside
+**`sd`** is "symmetric difference"---e.g. `sd(1, 4) = sd(4, 1) = 3`. \
+(it is also [a declaration form][sd] which is why it's purple.
+i don't know how to distinguish the two in pandoc/kate's syntax highlighting
+format sorry)
+
+[sd]: https://maude.lcc.uma.es/maude321-manual-html/maude-manualch10.html
+:::
 
 the first three rules just pick two numbers from our pool (any two, because of
 `comm`; they don't have to be next to each other), and replace them with the
@@ -200,10 +212,10 @@ op _,_ : Steps Steps -> Steps [assoc id: nil prec 20] .
 var Ss : Steps .
 ```
 
-<aside>
-  **`prec N`** is parsing/printing precedence (higher is looser, same as coq,
-  opposite of haskell/agda/idris).
-</aside>
+:::aside
+**`prec N`** is parsing/printing precedence (higher is looser, same as coq,
+opposite of haskell/agda/idris).
+:::
 
 so solution traces are written like
 `2 + 9 → 11,4 × 8 → 32,11 × 75 → 825,825 - 32 → 793`
@@ -235,11 +247,11 @@ eq (N Ps & Ss) has N = true .
 eq S           has N = false [otherwise] .
 ```
 
-<aside>
-  it could even skip the `false` line with a slightly different signature but
-  then i would have to explain more about the sort & kind system... this is good
-  enough.
-</aside>
+:::aside
+it could even skip the `false` line with a slightly different signature but
+then i would have to explain more about the sort & kind system... this is good
+enough.
+:::
 
 
 the new rewrite rules (delete the other ones) have the same behaviour for the

syntax/maude.xml

@@ -1,5 +1,8 @@
 <?xml version="1.0" encoding="UTF-8"?>
-<!DOCTYPE language SYSTEM "language.dtd">
+<!DOCTYPE language SYSTEM "language.dtd" [
+  <!ENTITY tok_start "(?&lt;=^|\s|[(\[{}\]),])">
+  <!ENTITY tok_end   "(?=$|\s|[(\[{}\]),])">
+]>
 
 <language name="Maude" section="Sources" extensions="*.maude"
           version="1" kateversion="5.53">
@@ -45,22 +48,26 @@
         <keyword attribute="eqs"     context="#stay" String="eqs"     />
         <keyword attribute="rules"   context="#stay" String="rules"   />
         <keyword attribute="members" context="#stay" String="members" />
+        <keyword attribute="strats"  context="#stay" String="strats"  />
+        <keyword attribute="sds"     context="#stay" String="sds"     />
 
         <keyword attribute="if" context="#stay" String="if" />
         <RegExpr attribute="if" context="#stay" String="/\\" />
 
         <RegExpr attribute="punc" context="#stay"
-          String="(?&lt;=^|\s)(?::[:=]?|->|&lt;-|=>|=(?:=|/=)?|@)(?=\s|$)" />
+          String="&tok_start;(?::[:=]?|->|&lt;-|=>|=(?:=|/=)?|@)&tok_end;" />
 
         <RegExpr attribute="delim" context="#stay"
           String="[{}\[\](),]|(?&lt;=^|\s)\.(?=\s|$)" />
 
         <DetectChar attribute="string" context="String" char="&quot;" />
 
-        <Float   attribute="float" context="#stay" />
+        <RegExpr attribute="rat"   context="#stay"
+          String="&tok_start;-?\d+(?:/\d+)?&tok_end;" />
         <RegExpr attribute="float" context="#stay"
-          String="(?&lt;=^|\s|[(\[{])-?Infinity(?=$|\s|[)\]}])" />
-        <RegExpr attribute="rat"   context="#stay" String="-?\d+(?:/\d+)?" />
+          String="&tok_start;-?\d*\.\d+(?:[eE][+-]?\d+)?&tok_end;" />
+        <RegExpr attribute="float" context="#stay"
+          String="&tok_start;-?Infinity&tok_end;" />
 
         <RegExpr attribute="comment" context="comment s"
           String="(?:---|\*\*\*)(?!\()" />
@@ -110,6 +117,9 @@
   </highlighting>
 
   <general>
-    <keywords casesensitive="true" />
+    <keywords
+      casesensitive="true"
+      additionalDeliminators="[]{}(), &#9;"
+      wordWrapDeliminators=" " />
   </general>
 </language>