0

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.

My grammar:

(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 Theorem (at * 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 Proof and QED keywords (or the Theorem and 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 Theorem-Proof-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...

1

It's a known bug (aka limitation) of SMIE's support for (backward-)up-list. To fix it right we need to make changes to (backward-)up-list, or otherwise redirect those commands to SMIE versions of them.

IIRC, you can partly avoid the problem by replacing things like

(decl
 ...
 ("Theorem" id ":" quotedmaterial "Proof" tactic "QED")
 ...)

with something like:

(decl
 ...
 ("Theorem" theorem-contents "QED")
 ...)
(theorem-contents
 (theorem-head "Proof" tactic))
(theorem-head (id ":" quotedmaterial))
3
  • Thanks for that; I will hack together a poor man’s approximation. Dec 29 '19 at 2:00
  • @MichaelNorrish: I added a suggestion that can sometimes work around the problem.
    – Stefan
    Dec 29 '19 at 16:40
  • Thanks! That has definitely helped! Jan 6 '20 at 6:01

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.