From d6225641adbf169c2300b3cf72484491be327881 Mon Sep 17 00:00:00 2001 From: David Aspinall Date: Fri, 13 Mar 2015 19:16:35 +0000 Subject: Summary: FAQ about copying output into new buffers --- FAQ | 17 +++++++++++++++-- 1 file changed, 15 insertions(+), 2 deletions(-) diff --git a/FAQ b/FAQ index c96e6d48..92370801 100644 --- a/FAQ +++ b/FAQ @@ -1,5 +1,5 @@ -FAQs for using Proof General -============================ +FAQs for using/installing Proof General +======================================= With thanks to the anonymous authors of questions/answers below. @@ -8,6 +8,19 @@ Please also check the BUGS file. ----------------------------------------------------------------- +Q. The prover process produces some useful output I'd like to + keep a note of, how do I do that? + +A. Some people cut and paste into comments in their source files. + But you can easily make new files or temporary buffers in Emacs: + + * copy text from *response* or *goals* buffer + * C-x b RET + * Switch to correct mode, e.g.: M-x isar-response-mode RET + * Paste text, the highlighting/sumbols should appear correctly. + +----------------------------------------------------------------- + Q. Proof General fails to load with an error message on start-up, containing text like this: -- cgit v1.2.3