From 4a020a712157cc94411048378b78d7832a8630c5 Mon Sep 17 00:00:00 2001 From: Dominique Unruh Date: Sat, 19 Feb 2022 01:33:49 +0200 Subject: [PATCH 1/7] qrhl: Improved font-lock mode: - sub/subscript symbols reappear when the following symbol is removed - sub/subscript symbols are not themselves sub/superscripted - all commands/tactics are fontified - different fonts (faces) for commands and tactics - better recognition of the commands/tactics (e.g., not as substrings of other words, only at beginning of line) - no highlighting of commands/tactics in reponse/goal buffers - keywords/tactics are recognized also after other commands. - comments are fontified. --- qrhl/qrhl.el | 28 +++++++++++++++++++++------- 1 file changed, 21 insertions(+), 7 deletions(-) diff --git a/qrhl/qrhl.el b/qrhl/qrhl.el index d5af5661c..5cac31178 100644 --- a/qrhl/qrhl.el +++ b/qrhl/qrhl.el @@ -74,19 +74,32 @@ (and (qrhl-parse-regular-command) 'cmd))) (defvar qrhl-font-lock-subsuperscript - '(("\\(⇩\\)\\([^[:space:]]\\)" . + '(("\\(⇩\\)\\([^⇩⇧[:space:]]\\)" . ((2 '(face subscript display (raise -0.3))) (1 '(face nil display "")))) - ("\\(⇧\\)\\([^[:space:]]\\)" . + ("\\(⇧\\)\\([^⇩⇧[:space:]]\\)" . ((2 '(face superscript display (raise 0.3))) (1 '(face nil display ""))))) "Font-lock configuration for displaying sub/superscripts that are prefixed by ⇩/⇧") (defvar qrhl-font-lock-keywords - ; Very simple configuration of keywords: highlights all occurrences, even if they are not actually keywords (e.g., when they are part of a term) - (append qrhl-font-lock-subsuperscript - '("lemma" "qrhl" "include" "quantum" "program" "equal" "simp" "isabelle" "isa" "var" "qed" - "skip")) + ; Regexp explanation: match the keyword/tactic after another command, and also if there are {}+*- in between (focusing commands) + (cl-flet ((mk-regexp (word) (concat "\\(?:^\\|\\.[ \t]\\)[ \t{}+*-]*\\b\\(" word "\\)\\b"))) + (append qrhl-font-lock-subsuperscript + (mapcar (lambda (keyword) `(,(mk-regexp keyword) . (1 'font-lock-keyword-face))) + '("debug:" "isabelle" "quantum\\s +var" "classical\\s +var" "ambient\\s +var" + "program" "adversary" "qrhl" "lemma" "include" "qed" "cheat" "print")) + + (mapcar (lambda (tactic) `(,(mk-regexp tactic) . (1 'font-lock-function-name-face))) + '("admit" "wp" "swap" "simp" "rule" "clear" "skip" "inline" "seq" "conseq\\s +pre" + "conseq\\s +post" "conseq\\s +qrhl" "equal" "rnd" + "byqrhl" "casesplit" "case" "fix" "squash" "frame" "measure" "o2h" "semiclassical" + "sym" "local\\s +remove" "local\\s +up" "rename" "if" "isa" + )) + + ; Regexp explanation: Match comment after + '(("\\(?:^\\|[ \t]\\)[ \t]*\\(#.*\\)" . (1 'font-lock-comment-face))) + )) "Font-lock configuration for qRHL proof scripts") (proof-easy-config 'qrhl "qRHL" @@ -116,8 +129,9 @@ proof-save-command-regexp "\\`a\\`" ;AKA `regexp-unmatchable' in Emacs-27 proof-tree-external-display nil proof-script-font-lock-keywords qrhl-font-lock-keywords - proof-goals-font-lock-keywords qrhl-font-lock-keywords + proof-goals-font-lock-keywords qrhl-font-lock-subsuperscript proof-response-font-lock-keywords qrhl-font-lock-keywords + font-lock-extra-managed-props '(display) proof-shell-unicode t ) From a2bd550a2ab1d749b9a5e549d21d48025f8846ec Mon Sep 17 00:00:00 2001 From: Dominique Unruh Date: Sat, 19 Feb 2022 01:36:39 +0200 Subject: [PATCH 2/7] qrhl: Added more abbreviations and symbols in input method. --- qrhl/qrhl-input.el | 18 +++++++++++++++++- 1 file changed, 17 insertions(+), 1 deletion(-) diff --git a/qrhl/qrhl-input.el b/qrhl/qrhl-input.el index 8d7bc41e4..ff6bd8ca5 100644 --- a/qrhl/qrhl-input.el +++ b/qrhl/qrhl-input.el @@ -411,7 +411,7 @@ ("\\heartsuit" ?♥) ("\\hookleftarrow" ?↩) ("\\hookrightarrow" ?↪) - ("\\iff" ?⇔) + ;("\\iff" ?⇔) ;; Defined below now ("\\imath" ?ı) ("\\in" ?∈) ("\\infty" ?∞) @@ -758,6 +758,22 @@ (">>" ?») ("\\Cla" ["ℭ𝔩𝔞"]) ("\\qeq" ["≡𝔮"]) + ("\\equiv_q" ["≡𝔮"]) + ("\\sub" ?⇩) + ("\\sup" ?⇧) + ("*_C" ["*⇩C"]) + ("*_V" ["*⇩V"]) + ("o_CL" ["o⇩C⇩L"]) + ("*_S" ["*⇩S"]) + ("\\ox_l" ["⊗⇩l"]) + ("\\ox_o" ["⊗⇩o"]) + ("\\ox_S" ["⊗⇩S"]) + ("\\in_q" ["∈⇩𝔮"]) + ("=_q" ["=⇩𝔮"]) + ("\\fun" ["⇒"]) + ("\\fun_CL" ["⇒⇩C⇩L"]) + ("\\implies" ?⟶) + ("\\iff" ?⟷) ) (provide 'qrhl-input) From ab7b2745978f82a665939a41d490844c396edda8 Mon Sep 17 00:00:00 2001 From: Dominique Unruh Date: Tue, 22 Feb 2022 02:45:26 +0200 Subject: [PATCH 3/7] qrhl: Removed leftover debug output. --- qrhl/qrhl.el | 1 - 1 file changed, 1 deletion(-) diff --git a/qrhl/qrhl.el b/qrhl/qrhl.el index 5cac31178..84283387b 100644 --- a/qrhl/qrhl.el +++ b/qrhl/qrhl.el @@ -60,7 +60,6 @@ )) (and (qrhl-forward-regex "\\.") (point)) )))) - (princ pos) (and pos (goto-char pos) t))) (defun qrhl-parse-focus-command () From 3b5d65d340c74218e758066cad50e2b4433b3b5e Mon Sep 17 00:00:00 2001 From: Dominique Unruh Date: Tue, 15 Mar 2022 19:16:28 +0200 Subject: [PATCH 4/7] qrhl: Remove comments from within multiline commands before sending them to qrhl-tool. --- qrhl/qrhl.el | 12 +++++++++--- 1 file changed, 9 insertions(+), 3 deletions(-) diff --git a/qrhl/qrhl.el b/qrhl/qrhl.el index 84283387b..262b2c163 100644 --- a/qrhl/qrhl.el +++ b/qrhl/qrhl.el @@ -43,13 +43,13 @@ (defun qrhl-forward-regex (regex) "If text starting at point matches REGEX, move to end of the match and return t. - Otherwise return nil" +Otherwise return nil" (and (looking-at regex) (goto-char (match-end 0)) t)) (defun qrhl-parse-regular-command () "Find the period-terminated command starting at point. - Moves to its end. - Returns t if this worked." +Moves to its end. +Returns t if this worked." (let ((pos (save-excursion (progn @@ -101,6 +101,11 @@ )) "Font-lock configuration for qRHL proof scripts") +(defun qrhl-proof-script-preprocess (file start end cmd) + "Strips comments from the command CMD. +Called before sending CMD to the prover." + (list (replace-regexp-in-string "\\(?:^\\|[ \t]\\)[ \t]*#.*$" "" cmd))) + (proof-easy-config 'qrhl "qRHL" proof-prog-name qrhl-prog-name ;; We need to give some option here, otherwise `proof-prog-name' is @@ -132,6 +137,7 @@ proof-response-font-lock-keywords qrhl-font-lock-keywords font-lock-extra-managed-props '(display) proof-shell-unicode t + proof-script-preprocess #'qrhl-proof-script-preprocess ) ; buttoning functions follow https://superuser.com/a/331896/748969 From 06e85d8f23f6300294dcc3f2a85188750b36812c Mon Sep 17 00:00:00 2001 From: Dominique Unruh Date: Sat, 19 Mar 2022 02:48:04 +0200 Subject: [PATCH 5/7] qrhl: Automatic indentation. --- qrhl/qrhl.el | 70 +++++++++++++++++++++++++++++++++++++++++++++++++++- 1 file changed, 69 insertions(+), 1 deletion(-) diff --git a/qrhl/qrhl.el b/qrhl/qrhl.el index 262b2c163..7bc51b9ad 100644 --- a/qrhl/qrhl.el +++ b/qrhl/qrhl.el @@ -28,6 +28,10 @@ "Name/path of the qrhl-prover command. (Restart Emacs after changing this.)" :type '(string) :group 'qrhl) +(defcustom qrhl-indentation-level 2 + "Indentation level in qRHL scripts" + :group 'qrhl) + (defun qrhl-find-and-forget (span) (proof-generic-count-undos span)) @@ -157,10 +161,74 @@ Called before sending CMD to the prover." (while (re-search-forward "include\s*\"\\([^\"]+\\)\"\s*\\." nil t) (make-button (match-beginning 1) (match-end 1) :type 'qrhl-find-file-button)))) + + +(defun qrhl-current-line-rel-indent () + "Determins by how much to indent the current line relative to the previous + indentation level. (Taking into account only the current line.)" + (save-excursion + (let ((qrhl-qed-pattern "^[ \t]*qed\\b") + (closing-brace-pattern "^[ \t]*}")) + (beginning-of-line) + ;; Analyse the current line and decide relative indentation accordingly + (cond + ;; qed - unindent by 2 + ((looking-at qrhl-qed-pattern) (- qrhl-indentation-level)) + ;; } - unindent by 2 + ((looking-at closing-brace-pattern) (- qrhl-indentation-level)) + ;; indent as previous + (t 0))))) + +(defun qrhl-indent-line () + "Indent current line as qRHL proof script" + (interactive) + + (let ((not-found t) (previous-indent nil) (previous-offset 0) rel-indent + (lemma-pattern "^[ \t]*\\(lemma\\|qrhl\\)\\b") + (comment-pattern "^[ \t]*#") + (empty-line-pattern "^[ \t]*$") + (brace-pattern "^[ \t]*{") + (focus-pattern "^[ \t{}+*-]*[+*-][ \t]*")) + + (beginning-of-line) ;; Throughout this function, we will always be at the beginning of a line + + ;; Identify preceding indented line (relative to which we indent) + (save-excursion + (while (and not-found (not (bobp))) + (forward-line -1) + (cond + ((and (not previous-indent) (looking-at comment-pattern)) + (setq previous-indent (current-indentation))) + ((looking-at empty-line-pattern) ()) + (t + (progn + (setq previous-indent (current-indentation)) + (setq not-found nil) + (cond + ((looking-at lemma-pattern) (setq previous-offset qrhl-indentation-level)) + ((looking-at focus-pattern) (setq previous-offset (- (match-end 0) (point) previous-indent))) + ((looking-at brace-pattern) (setq previous-offset qrhl-indentation-level))) + ))))) + (if (not previous-indent) (setq previous-indent 0)) + + ;; Now previous-indent contains the indentation-level of the preceding non-comment non-blank line + ;; If there is such line, it contains the indentation-level of the preceding non-blank line + ;; If there is no such line, it contains 0 + + ;; And previous-offset contains the offset that that line adds to following lines + ;; (i.e., 0 for normal lines, positive for qed and {, negative for }) + + (setq rel-indent (qrhl-current-line-rel-indent)) + + ;; Indent relative to previous-indent by rel-indent and previous-offset + (indent-line-to (max (+ previous-indent rel-indent previous-offset) 0)))) + + (add-hook 'qrhl-mode-hook (lambda () (set-input-method qrhl-input-method) - (set-variable 'electric-indent-mode nil t) + (setq electric-indent-inhibit t) ;; Indentation is not reliable enough for electric indent + (setq indent-line-function 'qrhl-indent-line) (qrhl-buttonize-buffer))) (provide 'qrhl) From a49cded675de3a714bbe302b07faf99e7b17a811 Mon Sep 17 00:00:00 2001 From: Dominique Unruh Date: Sun, 20 Feb 2022 21:18:17 +0200 Subject: [PATCH 6/7] qrhl: Added more keywords to syntax highlighting: `rewrite`, `print goal`, `sp`, `isabelle_cmd`. --- qrhl/qrhl.el | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/qrhl/qrhl.el b/qrhl/qrhl.el index 7bc51b9ad..46f0c8d8f 100644 --- a/qrhl/qrhl.el +++ b/qrhl/qrhl.el @@ -90,12 +90,12 @@ Returns t if this worked." (cl-flet ((mk-regexp (word) (concat "\\(?:^\\|\\.[ \t]\\)[ \t{}+*-]*\\b\\(" word "\\)\\b"))) (append qrhl-font-lock-subsuperscript (mapcar (lambda (keyword) `(,(mk-regexp keyword) . (1 'font-lock-keyword-face))) - '("debug:" "isabelle" "quantum\\s +var" "classical\\s +var" "ambient\\s +var" - "program" "adversary" "qrhl" "lemma" "include" "qed" "cheat" "print")) + '("isabelle_cmd" "debug:" "isabelle" "quantum\\s +var" "classical\\s +var" "ambient\\s +var" + "program" "adversary" "qrhl" "lemma" "include" "qed" "cheat" "print\\s +goal" "print")) (mapcar (lambda (tactic) `(,(mk-regexp tactic) . (1 'font-lock-function-name-face))) - '("admit" "wp" "swap" "simp" "rule" "clear" "skip" "inline" "seq" "conseq\\s +pre" - "conseq\\s +post" "conseq\\s +qrhl" "equal" "rnd" + '("admit" "wp" "sp" "swap" "simp" "rule" "clear" "skip" "inline" "seq" "conseq\\s +pre" + "conseq\\s +post" "conseq\\s +qrhl" "equal" "rnd" "rewrite" "byqrhl" "casesplit" "case" "fix" "squash" "frame" "measure" "o2h" "semiclassical" "sym" "local\\s +remove" "local\\s +up" "rename" "if" "isa" )) From c844c00d8c88120f927dd633c92e042250c69527 Mon Sep 17 00:00:00 2001 From: Dominique Unruh Date: Thu, 24 Nov 2022 22:25:47 +0200 Subject: [PATCH 7/7] qrhl: made `font-lock-extra-managed-props` buffer-local. --- qrhl/qrhl.el | 7 ++++++- 1 file changed, 6 insertions(+), 1 deletion(-) diff --git a/qrhl/qrhl.el b/qrhl/qrhl.el index 46f0c8d8f..d67c57541 100644 --- a/qrhl/qrhl.el +++ b/qrhl/qrhl.el @@ -139,7 +139,6 @@ Called before sending CMD to the prover." proof-script-font-lock-keywords qrhl-font-lock-keywords proof-goals-font-lock-keywords qrhl-font-lock-subsuperscript proof-response-font-lock-keywords qrhl-font-lock-keywords - font-lock-extra-managed-props '(display) proof-shell-unicode t proof-script-preprocess #'qrhl-proof-script-preprocess ) @@ -229,6 +228,12 @@ Called before sending CMD to the prover." (set-input-method qrhl-input-method) (setq electric-indent-inhibit t) ;; Indentation is not reliable enough for electric indent (setq indent-line-function 'qrhl-indent-line) + ;; This ensures that the fontification from qrhl-font-lock-subsuperscript is updated correctly + ;; when editing text (when re-fontifying). + ;; We only add it in qrhl-mode, not qrhl-response-mode or qrhl-goals-mode because in the latter two, + ;; text is never edited, only replaced as a while, so refontification doesn't happen there and + ;; is not needed. + (setq-local font-lock-extra-managed-props '(display)) (qrhl-buttonize-buffer))) (provide 'qrhl)