diff options
author | David Aspinall <da@inf.ed.ac.uk> | 2002-07-18 20:17:41 +0000 |
---|---|---|
committer | David Aspinall <da@inf.ed.ac.uk> | 2002-07-18 20:17:41 +0000 |
commit | 17cc59d137d559d474bfe72e45b8b8197912ea20 (patch) | |
tree | b24c53e7b6f6842baec55d80a4337da838bfa722 | |
parent | 9f942b1ea6ad239e93a33fb4d4cc7161a551592b (diff) |
Add FAQ about enabling X-Symbol.
-rw-r--r-- | FAQ | 25 |
1 files changed, 25 insertions, 0 deletions
@@ -7,6 +7,31 @@ For latest version, see http://www.proofgeneral.org/ProofGeneral/FAQ ----------------------------------------------------------------- +Q. I have just installed Emacs, ProofGeneral and a proof assistant. + It works but X-Symbol is not being activated. + +A. Once X-Symbol is picked up by Emacs (e.g. is working for TeX), + you should enable it inside Proof General by the menu item: + + Proof-General -> Options -> X-Symbol + + To enable it automatically every time you use Proof General, + type + + M-x customize-variable RET isar-x-symbol-enable RET + + and change/set/save the setting to `on'. + + Note that we don't do this by default, because from the system's + perspective it is difficult to determine if this will succeed --- + or just produce funny characters that confuse new users even more. + + If you are using Isabelle, the wrapper script will load X-Symbol + from any location, and you can enable it by passing the option + "-x true". + +----------------------------------------------------------------- + Q. I'm afraid I got stuck very early on. I sent the following line: by (swap_res_tac [psubsetI] 1; Notice that I forgot the right bracket. The line went pink, the |