Support for qrhl-tool theorem prover

[dominique-unruh]

Provides support for the theorem prover qrhl-tool (https://github.com/dominique-unruh/qrhl-tool).
Automatically activated for .qrhl files.

[hendriktews]

Hi! Thanks for your contribution! Setting the proof-tree variable should not be necessary - something seems to be odd. I do not see any require for loading the generic PG part - is there any reason why you don't do (require 'proof) as coq and easycrypt do and as it is recommended in appendix B of PG-adapting?

[hendriktews]

The doc-magic tests fail because you indirectly changed a variable documented in the manuals without updating the manuals. Please do make -C doc magic, check the changes, commit and upload. See also .github/workflows/test.yml.

[dominique-unruh]

Setting the proof-tree variable should not be necessary - something seems to be odd.

Do you mean proof-tree-external-display? I do not remember why I added it. A quick test now does not show any problems if I remove it. However, given that I wrote that PG fails without it in 80aac72, I would play it safe and keep it unless there is a reason why keeping it could be harmful.

I do not see any require for loading the generic PG part - is there any reason why you don't do (require 'proof) as coq and easycrypt do and as it is recommended in appendix B of PG-adapting?

No reason, I just didn't notice that it is necessary. I added (require 'proof) now. In Appendix B, it uses (require 'proof-easy-config) instead. Should I use that one?

Please do make -C doc magic, check the changes, commit and upload.

Done.

[hendriktews]

Do you mean proof-tree-external-display?

Yes, this variable is defined and managed inside generic/proof-tree.el. I believe without require 'proof you didn't load proof-tree.el and then proof-shell-exec-loop inside generic/proof-shell.el reports an undefined variable. require 'proof loads proof-tree.el and initializes proof-tree-external-display to nil. Therefore I recommend removing that line.

[hendriktews]

In Appendix B, it uses (require 'proof-easy-config) instead. Should I use that one?

You do use proof-easy-config, therefore I suggest to require both, proof and proof-easy-config.

@Matafou @erikmd @cpitclaudel Can one of you explain why B.1 only recommends to require proof-easy-config and that one requires much less than proof.el? To me it looks like easy-config was forgotten when adding require lines to proof.el.

Actually I am surprised the code in this PR works at all without requiring proof-easy-config. Do you have an idea who loads proof-easy-config in your setting (because I don't see any require proof-easy-config in Proof General)?

[dominique-unruh]

I believe without require 'proof you didn't load proof-tree.el and then proof-shell-exec-loop inside generic/proof-shell.el reports an undefined variable. require 'proof loads proof-tree.el and initializes proof-tree-external-display to nil.

Further experiments confirm your theory. I will remove proof-tree-external-display.

Also, requiring only proof-easy-config as suggested in Appendix B.1 is not enough. With that, I get an undefined error if I do not initialize proof-tree-external-display. So I think the example from Appendix B.1 should be updated to require proof.

Actually I am surprised the code in this PR works at all without requiring proof-easy-config. Do you have an idea who loads proof-easy-config in your setting (because I don't see any require proof-easy-config in Proof General)?

I load proof-site.el manually. proof-site requires proof-autoloads. That one defines an autoload for proof-easy-config.

You do use proof-easy-config, therefore I suggest to require both, proof and proof-easy-config.

Since proof.el also requires proof-site, proof-easy-config should be available (via autoload) when only loading proof. So at this point, I would think that I only need to require proof, but not proof-easy-config. Do you agree?

[monnier]

> Do you mean `proof-tree-external-display`? Yes, this variable is defined and managed inside generic/proof-tree.el. I believe without require 'proof you didn't load proof-tree.el and then proof-shell-exec-loop inside generic/proof-shell.el reports an undefined variable. require 'proof loads proof-tree.el and initializes proof-tree-external-display to nil. Therefore I recommend removing that line.

I recommend activating `flymake-mode` and paying attention to the warnings it shows. Stefan

[hendriktews]

Also, requiring only proof-easy-config as suggested in Appendix B.1 is not enough.

I suspected this, thanks for confirming.

I load proof-site.el manually. proof-site requires proof-autoloads.

I forgot about the autoloads, thanks for clarifying this.

I would think that I only need to require proof, but not proof-easy-config. Do you agree?

I agree.

[dominique-unruh]

Just checking: is there anything else I should fix or can we merge it? @hendriktews

[erikmd]

Hi, thanks a lot @dominique-unruh for your contribution!

Two remarks:

• before merging, you may want to update these lines of the README.md :)
• finally, just after the merge, you will have to open a PR in the MELPA repo so that the "qrhl" folder is deployed from PG's master by updating these lines of the corresponding "recipe". FWIW, the deployment is only performed several times per day.

(Apart from these remarks I just skimmed the PR, so, sorry for not having more time :/)

Anyway if @hendriktews, @Matafou, @cpitclaudel or @monnier are OK with merging, feel free to do so! 👍

[hendriktews]

Hi @dominique-unruh , we discussed this PR today in the PG maintainers telco. Because you want to add a new proof assistant and because PG is a spare time project for most of us we are a bit concerned about maintaining the qrhl support in the future. Can we assume that you or somebody from the qrhl community is motivated to maintain this code in the future?
Before merging, we would like to try to organize another review in the following days from somebody who is a bit more knowledgeable about adding new proof assistants.
What is your opinion about continuous integration, could you imagine to contribute fully automated tests in the not too far future that would reduce the risk that qrhl support is silently breaking?

[hendriktews]

Out of curiosity and unrelated to the decision of merging this PR we would like to ask the following: We saw that qrhl has a heavy dependence on Isabelle. Naively, we therefore thought it might have been simpler to add qrhl support to Isabelle/jEdit. Could you tell us why you decided for PG?

[dominique-unruh]

@hendriktews

Can we assume that you or somebody from the qrhl community is motivated to maintain this code in the future?

The current situation is such:

PG is the only way to interactively use qrhl-tool (except for using the REPL directly, but I would consider that unusable)
Currently, a patched PG is included as part of the qrhl-tool, together with a script that runs emacs with custom configuration.
The disadvantage is that this means that users end up with a bare-bone emacs, and without their usual emacs/PG customization.
This pull request is exactly the PG version included in qrhl-tool.

Since PG is the interface for using qrhl-tool, I will necessarily maintain it together with qrhl-tool, whether the pull request gets merged or not.
There are two situations in which I might stop maintaining it:
If qrhl-tool itself is ever abandoned, or if a different IDE will be designed or adapted for qrhl-tool (like when Isabelle transitioned from PG to jEdit).
In both cases, it would make sense to official withdraw the qrhl-tool PG interface because it would not be worth the effort to maintain two different IDEs.
Other than those cases, I would commit to maintaining the qrhl-tool part of PG. (And feel free to assign any qrhl related issues to me.)

What is your opinion about continuous integration, could you imagine to contribute fully automated tests in the not too far future that would reduce the risk that qrhl support is silently breaking?

Some "continuous integration" testing would happen "automatically" if I set up my own Emacs to automatically use the newest melpa package. :D
Besides that, I'm not very experienced in how one would test the interactive behavior. That is, I have no clue what unit tests one would set up.
If you have some examples that are not too specific to the requirements of a specific theorem prover, I'd be happy to adapt them.
However, there is one problem when it comes to CI test that actually need to run the prover: due to the Isabelle process in the background, and the large number of Isabelle theories that are compiled, qrhl-tool is too much for most public CI servers. (The first run takes maybe an hour or more to compile Isabelle theories. And since public CI servers usually start every job with a clean slate, this is a problem.)

[dominique-unruh]

@hendriktews

Out of curiosity and unrelated to the decision of merging this PR we would like to ask the following: We saw that qrhl has a heavy dependence on Isabelle. Naively, we therefore thought it might have been simpler to add qrhl support to Isabelle/jEdit. Could you tell us why you decided for PG?

I think the dependence of qrhl on Isabelle would not have made things easier because Isabelle is used under the hood, qrhl has its own files and syntax.
I think Isabelle/jEdit can be used to support other theorem provers. At least the underlying PIDE protocol is supposed to be generic.
However, in practice I think this is very difficult because the PIDE protocol is not very explicitly documented (there is a lot of documentation by source, I think) and much more heavyweight than PG.
I think the only way to reasonably get a jEdit interface would be to convince Makarius to do most of the work.

[dominique-unruh]

@hendriktews Any update? Is the commitment I can give sufficient?

[Matafou]

Hi.
Yes your commitment is sufficient.
We will spend a few more days to have a last look at your PR, then we will merge.
Then we can discuss how to have automatic tests (you can have a look at ci directory).
Thanks again for this contribution!

[dominique-unruh]

@Matafou @erikmd @monnier
I'm through with the comments you made (see the various answers above).

There is one (non-critical) issue: Currently, if the user starts qrhl-mode, then changes the variable qrhl-prog-name, and then starts the prover, the new value is not used because the proof-easy-config sets the proof-prog-name when loading the mode. In fact, as far as I can tell, the user needs to restart emacs altogether to make the new value take effect. Is there a way using proof-easy-config to read the variable qrhl-prog-name each time the prover is started? (The example in the documentation does not help because it uses a non-configurable name.)

[monnier]

Dominique Unruh [2022-02-14 12:39:21] wrote:

> Also, I wonder why you have ;;;###autoload cookies on defgroup and defcustom. Without them, I cannot customize the qrhl-options before opening a qrhl-file. (E.g., if I want to change the input method or the prog-name, with autoloaded defcustom's, I can open emacs, change the option, then open the .qrhl-file. Without autoload, I have to open the .qrhl-file, change the options, close the .qrhl-file again, and reopen it to make the changed options active. Seems like a bad user experience.)

That's an Emacs problem, so better not try and solve specifically for qrhl since it affects every other variable provided by every other ELisp package. You might want to request this feature with `M-x report-emacs-bug`. [ We already allow you to `C-h f <functionname> RET` and get that function's docstring even if the function is not autoloaded, so most of the infrastructure is there already. ]

[dominique-unruh]

@monnier, concerning autoload:

That's an Emacs problem, so better not try and solve specifically for qrhl since it affects every other variable provided by every other ELisp package.

I had assumed that autoloading defcustom is the recommended behavior because defcustom is explicitly mentioned in the documentation of the autoload cookie. However, "when to use autoload" explicitly advises against it, so I removed the autoload. (df40137)

[Matafou]

We are almost ready to merge I think. Is the license and copyright of the new files OK?

[dominique-unruh]

@monnier

After you've added your own code like you did, you also hold some part
of the copyright over the resulting file so you could add your name to
the copyright lines if you want.

Added copyright of my employer (360b6c2).

[dominique-unruh]

@monnier

It shouldn't be hard to make the new version work in Emacs-25 so as to avoid the duplication. [of qrhl-input.el]

I agree but I prefer to keep it this way. Reason: while the code has more duplication (bad) it is easier to read the diffs between the original latin-ltx.el and this input method (good if at some point the existing version is not compatible with an upcoming emacs). Overall, I think this approach makes maintaining easier. (If I'm wrong, we can always refactor this code later instead of now.)

[dominique-unruh]

@Matafou

We are almost ready to merge I think. Is the license and copyright of the new files OK?

Now it is. From my side, all is ready for merging.

[Matafou]

Is there something else to do before merging?

[monnier]

Is there something else to do before merging?

Not on my side.

[erikmd]

OK for me as well!

And regarding Stefan's question

It shouldn't be hard to make the new version work in Emacs-25 so as to avoid the duplication. [of qrhl-input.el]

I agree but I prefer to keep it this way. Reason: … Overall, I think this approach makes maintaining easier.

+1: I agree with @dominique-unruh that the file splitting is not an issue (including the day when we'll have to drop the compatibility with Emacs 25 !)

[erikmd]

So, everything looks fine! but just to let @hendriktews also comment if need be, I propose that we merge the PR no later than on next Monday (unless someone objects by then).

[Matafou]

Merged! Thanks again @dominique-unruh!

[erikmd]

Thanks @Matafou !

I've just opened PR melpa/melpa#7929 to update the MELPA recipe.

[erikmd]

Hi all. Just a heads-up to let you know that:

• PR Update recipe for proof-general: Add "qrhl" directory melpa/melpa#7929 has been merged yesterday
• As a result, the MELPA version of proof-general now contains "qrhl" support

[Matafou]

Thanks @erikmd.

[dominique-unruh]

I'm afraid the MELPA version of PG is now broken...

The first problem is: When installing, it tries to byte-compile all files in ProofGeneral. This includes the file qrhl-input-25.el which is for Emacs 25 only. This leads to a compilation error message. (I am not sure whether this is harmful, but at the very least it is quite alarming for the user, especially because the error message contains a 3MB long line.)

One solution would probably be to merge Emacs 25 & 26 files into one that always compiles. I could do that. But maybe there is some way to mark the file as excluded from compilation in Emacs 26+. Any clue?

The second problem (and I don't know whether that is a consequence of the first) is: When loading ProofGeneral with qRHL support, I get the message byte-code: Symbol’s function definition is void: proof-easy-config-check-setup. Only if I manually load ...../generic/proof-easy-config.el can I activate the qRHL mode. Maybe it is needed to include (require 'proof-easy-config)? (We decided not to, see here) In any case, I have no clue why this only happens when using the MELPA install.

[dominique-unruh]

The second problem (and I don't know whether that is a consequence of the first) is: When loading ProofGeneral with qRHL support, I get the message byte-code: Symbol’s function definition is void: proof-easy-config-check-setup. Only if I manually load ...../generic/proof-easy-config.el can I activate the qRHL mode. Maybe it is needed to include (require 'proof-easy-config)? (We decided not to, see here) In any case, I have no clue why this only happens when using the MELPA install.

The second problem is not MELPA install specific. It also occurs if I run PG from the git repo, but only if I compile the lisp files first. Still unsure why, but at least that makes experiments easier.

[dominique-unruh]

The second problem is not MELPA install specific. It also occurs if I run PG from the git repo, but only if I compile the lisp files first. Still unsure why, but at least that makes experiments easier.

Mystery partially solved (124db99): (require 'proof-easy-config) is indeed needed and fixes the problem, but only needed when running from byte-compiled code. Maybe a good idea to clarify that in the manual (the easy-config example)?

[erikmd]

Hi @dominique-unruh, OK thanks a lot for your testing and feedback!

Regarding the first issue: I'm not aware of a better solution than what you propose (merge the two files in a single one), maybe @monnier would have other ideas? (because the current file-splitting was nice to ease maintenance…)

Regarding the second issue: I'm unsure if you'd like to also use (eval-when-compile …); anyway also updating the manual would be nice indeed;

Feel free to open a new single PR fixing both blocking issues (not necessarily updating the manual at once, as you want anyway); and we'll merge it quickly…

[dominique-unruh]

Feel free to open a new single PR fixing both blocking issues (not necessarily updating the manual at once, as you want anyway); and we'll merge it quickly…

I'm making a new PR and moving the open questions there. (#643)

[erikmd]

Thanks @dominique-unruh!

[monnier]

Regarding the first issue: I'm not aware of a better solution than what you propose (merge the two files in a single one), maybe @monnier would have other ideas? (because the current file-splitting was nice to ease maintenance…)

The patch below includes the local changes I have to fix compilation issues in the qrhl-input files.

regarding the second issue: I'm unsure if you'd like to use `(eval-when-compile …)`; anyway also updating the manual would be nice indeed;

I think it's a bug in proof-easy-config (which I tried to fix in the untested patch below). Stefan diff --git a/generic/proof-easy-config.el b/generic/proof-easy-config.el index 6639e9b266..dd81745c15 100644 --- a/generic/proof-easy-config.el +++ b/generic/proof-easy-config.el @@ -1,9 +1,9 @@ -;;; proof-easy-config.el --- Easy configuration for Proof General +;;; proof-easy-config.el --- Easy configuration for Proof General -*- lexical-binding: t; -*- ;; This file is part of Proof General. ;; Portions © Copyright 1994-2012 David Aspinall and University of Edinburgh -;; Portions © Copyright 2003, 2012, 2014 Free Software Foundation, Inc. +;; Portions © Copyright 2003-2022 Free Software Foundation, Inc. ;; Portions © Copyright 2001-2017 Pierre Courtieu ;; Portions © Copyright 2010, 2016 Erik Martin-Dorel ;; Portions © Copyright 2011-2013, 2016-2017 Hendrik Tews @@ -51,15 +51,15 @@ ;; (modsyn (intern (concat "proof-" suffixnm "-syntax-table-entries"))) (fullbody (append - (if (and (boundp modsyn) (eval modsyn)) + (if (and (boundp modsyn) (eval modsyn t)) (list `(let ((syn ,modsyn)) (while syn (modify-syntax-entry (car syn) (cadr syn)) (setq syn (cddr syn)))))) body))) - (eval - `(define-derived-mode ,mode ,parent ,modename nil ***@***.***))))) + (eval ;;FIXME: Yuck! + `(define-derived-mode ,mode ,parent ,modename nil ***@***.***) t)))) (defun proof-easy-config-check-setup (sym name) "Perform a number of simple checks. @@ -99,7 +99,9 @@ The proof assistant is denoted by symbol SYM and string NAME." The symbol SYM and string name NAME must match those given in the `proof-assistant-table', which see. Additional arguments are taken into account as a setq BODY." + (declare (indent 2) (debug (form form &rest [symbolp form]))) `(progn + (require 'proof-easy-config) (proof-easy-config-check-setup ,sym ,name) (setq ***@***.***) diff --git a/qrhl/qrhl-input-25.el b/qrhl/qrhl-input-25.el index 6d9fb574ac..b90ec5676d 100644 --- a/qrhl/qrhl-input-25.el +++ b/qrhl/qrhl-input-25.el @@ -1,8 +1,7 @@ ;;; qrhl-input.el --- Quail package for TeX-style input for qrhl-tool in ProofGeneral -*- lexical-binding: t -*- -;; Copyright (C) 2001-2017 Free Software Foundation, Inc. -;; Copyright (C) 2001, 2002, 2003, 2004, 2005, 2006, 2007, 2008, 2009, -;; 2010, 2011 +;; Copyright (C) 2001-2022 Free Software Foundation, Inc. +;; Copyright (C) 2001-2011 ;; National Institute of Advanced Industrial Science and Technology (AIST) ;; Registration Number H14PRO021 ;; Copyright (C) 2017-2022 University of Tartu @@ -74,15 +73,19 @@ (`(,_ ,(pred characterp)) (push rule newrules)) ;; Normal quail rule. (`(,seq ,re) (let ((count 0) - (re (eval re t))) - (dolist (pair (ucs-names)) + (re (eval re t)) + (ucs-names (ucs-names))) + ;; More recent Emacsen have `ucs-names' return a hash-table. + ;; We don't need to run this code there, but we do want to avoid + ;; signaling a silly error during compilation. + (dolist (pair (if (listp ucs-names) ucs-names)) (let ((name (car pair)) (char (cdr pair))) (when (and (characterp char) ;; Ignore char-ranges. (string-match re name)) (let ((keys (if (stringp seq) (replace-match seq nil nil name) - (funcall seq name char)))) + (funcall (eval seq t) name char)))) (if (listp keys) (dolist (x keys) (setq count (1+ count)) diff --git a/qrhl/qrhl-input.el b/qrhl/qrhl-input.el index 8cc520425c..b2dca3696b 100644 --- a/qrhl/qrhl-input.el +++ b/qrhl/qrhl-input.el @@ -1,8 +1,7 @@ -;;; qrhl-input.el --- Quail package for TeX-style input for qrhl-tool in ProofGeneral -*-coding: utf-8;-*- +;;; qrhl-input.el --- Quail package for TeX-style input for qrhl-tool in ProofGeneral -*- lexical-binding: t; -*- -;; Copyright (C) 2001-2018 Free Software Foundation, Inc. -;; Copyright (C) 2001, 2002, 2003, 2004, 2005, 2006, 2007, 2008, 2009, -;; 2010, 2011 +;; Copyright (C) 2001-2022 Free Software Foundation, Inc. +;; Copyright (C) 2001-2011 ;; National Institute of Advanced Industrial Science and Technology (AIST) ;; Registration Number H14PRO021 ;; Copyright (C) 2017-2022 University of Tartu @@ -79,7 +78,7 @@ (string-match re name)) (let ((keys (if (stringp seq) (replace-match seq nil nil name) - (funcall seq name char)))) + (funcall (eval seq t) name char)))) (if (listp keys) (dolist (x keys) (setq count (1+ count)) diff --git a/qrhl/qrhl.el b/qrhl/qrhl.el index bd0ec6290b..43f670e8e7 100644 --- a/qrhl/qrhl.el +++ b/qrhl/qrhl.el @@ -14,15 +14,19 @@ ;;; Code: +(require 'proof-script) ;For proof-generic-count-undos. + (if (version< emacs-version "26") (require 'qrhl-input-25) (require 'qrhl-input)) -(defcustom qrhl-input-method "qrhl" "Input method to use when editing qRHL proof scripts" +(defcustom qrhl-input-method "qrhl" + "Input method to use when editing qRHL proof scripts" :type '(string) :group 'qrhl) -(defcustom qrhl-prog-name "qrhl" "Name/path of the qrhl-prover command. (Restart Emacs after changing this.)" +(defcustom qrhl-prog-name "qrhl" + "Name/path of the qrhl-prover command. (Restart Emacs after changing this.)" :type '(string) :group 'qrhl) (defun qrhl-find-and-forget (span) @@ -44,8 +48,9 @@ (and (looking-at regex) (goto-char (match-end 0)) t)) (defun qrhl-parse-regular-command () - "Finds the period-terminated command starting at the point (and moves to its end). - Returns t if this worked." + "Find the period-terminated command starting at point. +Moves to its end. +Returns t if this worked." (let ((pos (save-excursion (progn @@ -86,33 +91,36 @@ "Font-lock configuration for qRHL proof scripts") (proof-easy-config 'qrhl "qRHL" - proof-prog-name qrhl-prog-name - ; We need to give some option here, otherwise proof-prog-name is interpreted - ; as a shell command which leads to problems if the path contains spaces - ; (see the documentation for proof-prog-name) - qrhl-prog-args '("--emacs") - ;proof-script-command-end-regexp "\\.[ \t]*$" - proof-script-parse-function 'qrhl-proof-script-parse-function - proof-shell-annotated-prompt-regexp "^\\(\\.\\.\\.\\|qrhl\\)> " - ;proof-script-comment-start-regexp "#" - ;proof-script-comment-end "\n" - proof-shell-error-regexp "^\\(\\[ERROR\\]\\|Exception\\)" - proof-undo-n-times-cmd "undo %s." - proof-find-and-forget-fn 'qrhl-find-and-forget - proof-shell-start-goals-regexp "^[0-9]+ subgoals:\\|^Goal:\\|^No current goal\\.\\|^In cheat mode\\.\\|^No focused goals (use " - proof-shell-proof-completed-regexp "^No current goal.$" - proof-shell-eager-annotation-start "\\*\\*\\* " - proof-shell-eager-annotation-start-length 4 - proof-no-fully-processed-buffer t - proof-shell-filename-escapes '(("\\\\" . "\\\\") ("\"" . "\\\"")) - proof-shell-cd-cmd "changeDirectory \"%s\"." - proof-save-command-regexp "^adfuaisdfaoidsfasd" ; ProofGeneral produces warning when this is not set. But we don't want goal/save commands to be recognized because that makes ProofGeneral do an atomic undo. - proof-tree-external-display nil - proof-script-font-lock-keywords qrhl-font-lock-keywords - proof-goals-font-lock-keywords qrhl-font-lock-keywords - proof-response-font-lock-keywords qrhl-font-lock-keywords - proof-shell-unicode t - ) + proof-prog-name qrhl-prog-name + ;; We need to give some option here, otherwise `proof-prog-name' is + ;; interpreted as a shell command which leads to problems if the file name + ;; contains spaces (see the documentation for `proof-prog-name'). + qrhl-prog-args '("--emacs") + ;;proof-script-command-end-regexp "\\.[ \t]*$" + proof-script-parse-function #'qrhl-proof-script-parse-function + proof-shell-annotated-prompt-regexp "^\\(\\.\\.\\.\\|qrhl\\)> " + ;;proof-script-comment-start-regexp "#" + ;;proof-script-comment-end "\n" + proof-shell-error-regexp "^\\(\\[ERROR\\]\\|Exception\\)" + proof-undo-n-times-cmd "undo %s." + proof-find-and-forget-fn 'qrhl-find-and-forget + proof-shell-start-goals-regexp "^[0-9]+ subgoals:\\|^Goal:\\|^No current goal\\.\\|^In cheat mode\\.\\|^No focused goals (use " + proof-shell-proof-completed-regexp "^No current goal.$" + proof-shell-eager-annotation-start "\\*\\*\\* " + proof-shell-eager-annotation-start-length 4 + proof-no-fully-processed-buffer t + proof-shell-filename-escapes '(("\\\\" . "\\\\") ("\"" . "\\\"")) + proof-shell-cd-cmd "changeDirectory \"%s\"." + ;; ProofGeneral produces warning when this is not set. But we don't want + ;; goal/save commands to be recognized because that makes ProofGeneral do an + ;; atomic undo. + 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-response-font-lock-keywords qrhl-font-lock-keywords + proof-shell-unicode t + ) ; buttoning functions follow https://superuser.com/a/331896/748969 (define-button-type 'qrhl-find-file-button