From 3a9be64827bbed8e34d38803b5c44d8d4f6cd688 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Cl=C3=A9ment=20Pit--Claudel?= Date: Thu, 12 Jan 2017 20:26:04 -0500 Subject: [PATCH] Use a syntax-propertize-function to properly handle '(//' comments Fixes #42. --- fstar-mode.el | 30 +++++++++++++++++++++++------- 1 file changed, 23 insertions(+), 7 deletions(-) diff --git a/fstar-mode.el b/fstar-mode.el index b9d1899..8582f9e 100755 --- a/fstar-mode.el +++ b/fstar-mode.el @@ -423,15 +423,30 @@ If MUST-FIND-TYPE is nil, the :type part is not necessary." ;; Comments and strings (modify-syntax-entry ?\\ "\\" table) (modify-syntax-entry ?\" "\"" table) - (modify-syntax-entry ?* ". 23" table) - (modify-syntax-entry ?/ ". 12b" table) - (modify-syntax-entry ?\n "> b" table) - (modify-syntax-entry ?\^m "> b" table) - (modify-syntax-entry ?\( "()1n" table) - (modify-syntax-entry ?\) ")(4n" table) + ;; ‘/’ is handled by a `syntax-propertize-function'. For background on this + ;; see http://lists.gnu.org/archive/html/emacs-devel/2017-01/msg00144.html. + ;; The comment enders are left here, since they don't match the ‘(*’ openers. + ;; (modify-syntax-entry ?/ ". 12c" table) + (modify-syntax-entry ?\n ">" table) + (modify-syntax-entry ?\^m ">" table) + (modify-syntax-entry ?\( "()1nb" table) + (modify-syntax-entry ?* ". 23b" table) + (modify-syntax-entry ?\) ")(4nb" table) table) "Syntax table for F*.") +(defconst fstar-mode-syntax-propertize-function + (let ((opener-1 (string-to-syntax ". 1")) + (opener-2 (string-to-syntax ". 2"))) + (syntax-propertize-rules + ("//" (0 (let* ((pt (match-beginning 0)) + (state (syntax-ppss pt))) + (goto-char (match-end 0)) ;; syntax-ppss adjusts point + (unless (or (nth 3 state) (nth 4 state)) + (put-text-property pt (+ pt 1) 'syntax-table opener-1) + (put-text-property (+ pt 1) (+ pt 2) 'syntax-table opener-2) + (ignore (goto-char (point-at-eol)))))))))) + ;;; Mode map (defvar fstar-mode-map @@ -1228,7 +1243,8 @@ into blocks; process it as one large block instead." (setq-local comment-continue " *") (setq-local comment-end "*)") (setq-local comment-start-skip "\\(//+\\|(\\*+\\)[ \t]*") - (setq-local font-lock-syntactic-face-function #'fstar-syntactic-face-function)) + (setq-local font-lock-syntactic-face-function #'fstar-syntactic-face-function) + (setq-local syntax-propertize-function fstar-mode-syntax-propertize-function)) ;;; Main mode -- 2.7.4