Though SMIE seems to be indenting my little language very nicely, and
forward-sexp also works well, I don't get
backward-up-list working as desired.
(defvar holscript-smie-grammar (smie-prec2->grammar (smie-bnf->prec2 '((id) (decl ("Theorem" id ":" quotedmaterial "Proof" tactic "QED") ("Definition" id ":" quotedmaterial "Termination" tactic "End") ("Definition" id ":" quotedmaterial "End") ("Datatype:" quotedmaterial "End")) (quotedmaterial) (tactic (tactic ">>" tactic) (tactic "\\\\" tactic) (tactic ">-" tactic) (tactic ">|" tactic))) '((assoc ">>" "\\\\" ">-" ">|")))))
If I have my cursor inside a
* below, say):
Theorem name: statement Proof tactic1 `*` >> tactic2 QED
then I can navigate along the tactics nicely. If I have the cursor on
Theorem I can use
C-M-b to navigate a sequence of
Theorems nicely too. But if I'm between the
QED keywords (or the
Proof keywords), I can't use
backward-up-list to get me to the top level of that phrase. Instead, I get a
Scan error: "Unbalanced parentheses", and I shoot to the top of the whole file.
It seems to me as if the grammar is defining the
QED syntax as a sexp-like thing (and wrt to
forward-sexp this also seems true), but
backward-up-list doesn't seem to agree...