aboutsummaryrefslogtreecommitdiffhomepage
path: root/FAQ
diff options
context:
space:
mode:
authorGravatar David Aspinall <da@inf.ed.ac.uk>2005-04-27 11:01:12 +0000
committerGravatar David Aspinall <da@inf.ed.ac.uk>2005-04-27 11:01:12 +0000
commit01897d2fca56fa97aeb958ec6a7f73fb5fad612f (patch)
treedaf09afda51b0ee2d87d4aae20652ebe7410679f /FAQ
parent7ed80a2c480b694546eb5ab9fa7edede37a9a875 (diff)
Add FAQ about favourites
Diffstat (limited to 'FAQ')
-rw-r--r--FAQ23
1 files changed, 19 insertions, 4 deletions
diff --git a/FAQ b/FAQ
index 946ddb47..a687fb09 100644
--- a/FAQ
+++ b/FAQ
@@ -275,12 +275,18 @@ A. There are X-Symbol fonts at sizes of 12, 14, 18 and 24. The standard size
-----------------------------------------------------------------
+Q. The "Favourites" feature to insert/send fixed strings is great,
+ but I'd like to define a command which takes arguments.
-Q. I see spurious ^M characters at the end of lines in the
- windows showing output from the prover. How can I remove
- them?
+A. You can do that in Elisp with a command like this:
+
+ (proof-definvisible isar-theorem
+ '(format "thm %s" (read-string "theorem: "))
+ [(control t)])
+
+ (NB: it binds the key C-c C-a C-t). See the documentation for
+ `proof-definvisible' and `proof-defshortcut`.
-A. Customize the value of `proof-shell-strip-crs-from-output'.
-----------------------------------------------------------------
@@ -293,6 +299,15 @@ A. Your Emacs session has loaded a version of xml.el from somewhere other
-----------------------------------------------------------------
+Q. I see spurious ^M characters at the end of lines in the
+ windows showing output from the prover. How can I remove
+ them?
+
+A. Customize the value of `proof-shell-strip-crs-from-output'.
+
+-----------------------------------------------------------------
+
+
Q. Can I join any mailing lists for Proof General?
A. Of course, email "proofgeneral-request@informatics.ed.ac.uk"