From 13c778a32691135dd5ec3e95623e3c549f1fe1ba Mon Sep 17 00:00:00 2001 From: Michael Norrish Date: Mon, 6 Jan 2020 17:05:42 +1100 Subject: [PATCH] emacs-mode: fixes for holscript-mode - Remove erorrs arising at start and end of file - Improve sexp-navigation by adopting suggestion from Stefan Monnier at https://emacs.stackexchange.com/questions/54464/smie-and-backward-up-list - Colour THEN properly, colour THEN1. --- tools/holscript-mode.el | 29 +++++++++++++++++++---------- 1 file changed, 19 insertions(+), 10 deletions(-) diff --git a/tools/holscript-mode.el b/tools/holscript-mode.el index 5525958fd5..dd2223dcc9 100644 --- a/tools/holscript-mode.el +++ b/tools/holscript-mode.el @@ -9,7 +9,8 @@ '("^Definition\\>\\|^\\(Co\\)?Inductive\\>\\|^Termination\\>\\|^End\\>" . 'holscript-definition-syntax) '("^Datatype\\>" . 'holscript-definition-syntax) - '("\\" . 'holscript-then-syntax) + '("^THEN[1L]?\\>" . 'holscript-then-syntax) + '("[^A-Za-z0-9_']\\(THEN[1L]?\\)\\>" 1 'holscript-then-syntax) '("\\S.\\(>[->|]\\|\\\\\\\\\\)\\S." 1 'holscript-then-syntax) "^Type\\>" "^Overload\\>" @@ -654,25 +655,30 @@ On existing quotes, toggles between ‘-’ and “-” pairs. Otherwise, inser (smie-prec2->grammar (smie-bnf->prec2 '((id) - (decl ("Theorem" id ":" quotedmaterial "Proof" tactic "QED") - ("Definition" id ":" quotedmaterial "Termination" tactic "End") - ("Definition" id ":" quotedmaterial "End") + (decl ("Theorem" theorem-contents "QED") + ("Definition" definition-contents "End") ("Datatype:" quotedmaterial "End")) + (theorem-contents (id-quoted "Proof" tactic)) + (definition-contents (id-quoted "Termination" tactic) (id-quoted)) + (id-quoted (id ":" quotedmaterial)) (quotedmaterial) (tactic (tactic ">>" tactic) (tactic "\\\\" tactic) (tactic ">-" tactic) (tactic ">|" tactic) + (tactic "THEN" tactic) + (tactic "THEN1" tactic) + (tactic "THENL" tactic) ("[" tactics "]")) (tactics (tactic) (tactics "," tactics))) '((assoc ",")) - '((assoc ">>" "\\\\" ">-" ">|"))))) + '((assoc ">>" "\\\\" ">-" ">|" "THEN" "THEN1" "THENL"))))) (defvar holscript-smie-keywords-regexp (regexp-opt '("Definition" "Theorem" "Proof" "QED" ">>" ">-" "\\\\" ">|" "Termination" ":"))) (defvar holscript-quotedmaterial-delimiter-regexp - (regexp-opt '("``" "`"))) + (regexp-opt '("“" "”" "‘" "’"))) (defun holscript-smie-forward-token () (forward-comment (point-max)) (cond @@ -682,7 +688,7 @@ On existing quotes, toggles between ‘-’ and “-” pairs. Otherwise, inser ((looking-at holscript-quotedmaterial-delimiter-regexp) (goto-char (match-end 0)) (match-string-no-properties 0)) - ((= 1 (syntax-class (syntax-after (point)))) + ((equal 1 (syntax-class (syntax-after (point)))) (buffer-substring-no-properties (point) (progn (skip-syntax-forward ".") (point)))) @@ -694,13 +700,16 @@ On existing quotes, toggles between ‘-’ and “-” pairs. Otherwise, inser (defun holscript-smie-backward-token () (forward-comment (- (point))) (cond - ((looking-back holscript-smie-keywords-regexp (- (point) 15) t) + (; am I just after a keyword? + (looking-back holscript-smie-keywords-regexp (- (point) 15) t) (goto-char (match-beginning 0)) (match-string-no-properties 0)) - ((looking-back holscript-quotedmaterial-delimiter-regexp (- (point) 1) t) + (; am I just after a quotation mark + (looking-back holscript-quotedmaterial-delimiter-regexp (- (point) 1) t) (goto-char (match-beginning 0)) (match-string-no-properties 0)) - ((= 1 (syntax-class (syntax-after (1- (point))))) + (; am I sitting after "punctuation" + (equal 1 (syntax-class (syntax-after (1- (point))))) (buffer-substring-no-properties (point) (progn (skip-syntax-backward ".") (point))))