From 72eeead8935ddf733022b2427c2cf2797126f570 Mon Sep 17 00:00:00 2001 From: David Aspinall Date: Mon, 30 Apr 2012 13:17:14 +0000 Subject: Change default Unicode Tokens font back to DejaVU Sans, more reliable without installing STIX. --- FAQ | 95 +++++++++++++++++++++++++++++-------------------- etc/isar/TokensAcid.thy | 92 +++++++++++++++++++++++++---------------------- isar/Example-Tokens.thy | 2 +- lib/unicode-tokens.el | 7 ++-- 4 files changed, 110 insertions(+), 86 deletions(-) diff --git a/FAQ b/FAQ index 734f6c8f..c96e6d48 100644 --- a/FAQ +++ b/FAQ @@ -31,6 +31,62 @@ A. We distribute compiled .elcs for one version of Emacs, but other ----------------------------------------------------------------- +Q. I have just installed Emacs, ProofGeneral and a proof assistant. + It works but Tokens (e.g. \) are not being displayed + as symbols. + +A. You need to enable Unicode Tokens by the menu item: + + Proof-General -> Options -> Unicode Tokens + + To enable it automatically every time you use Proof General, + use + + Proof-General -> Options -> Save Options + + after doing this. + + 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 Tokens + from any location, and you can enable it by passing the option + "-x true". + +----------------------------------------------------------------- + + +Q. With Unicode symbols enabled, the symbols look a mess, e.g. + compressed and overlap one another. + +A. Unfortunately this is a bug in the display engine inside + certain versions of Emacs, for example the default version + of emacs, Emacs 23.3.1 on Ubuntu 11.10, suffers. + + The solution is to switch to another version (e.g. Emacs 23.2). + (See Trac#409: http://proofgeneral.inf.ed.ac.uk/trac/ticket/409) + + You may be able to get better results with different fonts, even + without upgrading Emacs. + + Proof General uses Deja Vu Sans Mono by default because + this often works out-of-the-box. But STIX is better if you + install it. See http://www.stixfonts.org/. On Ubuntu try: + + sudo apt-get install fonts-stix + + To change to STIX, either + + M-x customize face RET unicode-tokens-symbol-font-face RET + + and edit to set the family name to "STIXGeneral", or edit + the line beginning "(defface unicode-tokens-symbol-font-face" in + lib/unicode-tokens.el. + + +----------------------------------------------------------------- + Q. Help, I'm stuck!! Emacs keeps telling me "Cannot switch buffers in a dedicated window" @@ -74,45 +130,6 @@ A. Unfortunately the architecture of Proof General is designed so ------------------------------------------------------------------ - -Q. I have just installed Emacs, ProofGeneral and a proof assistant. - It works but Tokens (e.g. \) are not being displayed - as symbols. - -A. You need to enable Unicode Tokens by the menu item: - - Proof-General -> Options -> Unicode Tokens - - To enable it automatically every time you use Proof General, - use - - Proof-General -> Options -> Save Options - - after doing this. - - 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 Tokens - from any location, and you can enable it by passing the option - "-x true". - - ------------------------------------------------------------------ - - -Q. With Unicode symbols enabled, arrows and other symbols appear - compressed and overlap one another. - -A. Unfortunately this is a bug in the display engine inside - certain versions of Emacs, for example the default version - of emacs, Emacs 23.3.1 on Ubuntu 11.10, suffers. - - The solution is to switch to another version (e.g. Emacs 23.2). - (See Trac#409). - ----------------------------------------------------------------- diff --git a/etc/isar/TokensAcid.thy b/etc/isar/TokensAcid.thy index 8b37d951..17597181 100644 --- a/etc/isar/TokensAcid.thy +++ b/etc/isar/TokensAcid.thy @@ -22,52 +22,58 @@ begin I recommend using StixGeneral for symbols. See http://www.stixfonts.org/ - This is the default for the symbol font if you have it installed. + To install on Ubuntu, try: + + sudo apt-get install fonts-stix + Other good choices are: Lucida Grande, Lucida Sans Unicode, or DejaVuLGC Sans Mono. - 1. \ \ \ \ \ \ \ \ \ \ - 2. \ \ \ \ \ \ \ \ \ \ - 3. \ \ \ \ \ \ \ \ \ \ - 4. \ \ \ \ \ \ \ \ \ \ - 5. \ \ \ \ \ \ \ \ \ \ - 6. \ \ \ \ \ \ \ \ \ \ - 7. \ \ \ \ \ \ \ \ \ \ - 8. \ \ \ \ \ \ \ \ \ \ - 9. \ \ \ \ \ \ \ \ \ \ - 10. \ \ \ \ \ \ \ \ \ \ - 11. \ \ \ \ \ \ \ \ \ \ - 12. \ \ \ \ \ \ \ \ \ \
- 13. \ \ \ \ \ \ \ \ \ \ - 14. \ \ \ \ \ \ \ \ \ \ - 15. \ \ \ \ \ \ \ \ \ \ - 16. \ \ \ \ \ \ \ \ \ \ - 17. \ \ \ \ \ \ \ \ \ \ - 18. \ \ \ \ \ \ \
\ \ \ - 19. \ \ \ \ \ \ \ \ \ \ - 20. \ \ \ \ \ \ \ \ \ \ - 21. \ \ \ \ \ \ \ \ \ \ - 22. \ \ \ \ \ \ \ \ \ \ - 23. \ \ \ \ \ \ \ \ \ \ - 24. \ \ \ \ \ \ \ \ \ \ - 25. \ \ \ \ \ \ \ \ \ \ - 26. \ \ \ \ \ \ \ \ \ \ - 27. \ \ \ \ \ \ \ \ \ \ - 28. \ \ \ \ \ \ \ \ \ \ - 29. \ \ \ \ \ \ \ \ \ \ - 30. \ \ \ \ \ \ \ \ \ \ - 31. \ \ \ \ \ \ \ \ \ \ - 32. \ \ \ \ \ \ \ \ \ \ - 33. \ \ \ \ \ \ \

\ \ \ \ \ \ \ - 37. \ \ \ \ \ \ \

\ \ \ - 38. \ \ \ \ \ \ \ \ \ \ - 39. \ \ \ \ \ \ \ \ \ \ - 40. \ \ \
\ \ \ \ \ \ \ - 41. \ \ \ \ \ \ \ \ \ \ - 42. \ \ \ \ \ + Unfortunately + + + 1. \ \ \ \ \ \ \ \ \ \ + 2. \ \ \ \ \ \ \ \ \ \ + 3. \ \ \ \ \ \ \ \ \ \ + 4. \ \ \ \ \ \ \ \ \ \ + 5. \ \ \ \ \ \ \ \ \ \ + 6. \ \ \ \ \ \ \ \ \ \ + 7. \ \ \ \ \ \ \ \ \ \ + 8. \ \ \ \ \ \ \ \ \ \ + 9. \ \ \ \ \ \ \ \ \ \ +10. \ \ \ \ \ \ \ \ \ \ +11. \ \ \ \ \ \ \ \ \ \ +12. \ \ \ \ \ \ \ \ \ \
+13. \ \ \ \ \ \ \ \ \ \ +14. \ \ \ \ \ \ \ \ \ \ +15. \ \ \ \ \ \ \ \ \ \ +16. \ \ \ \ \ \ \ \ \ \ +17. \ \ \ \ \ \ \ \ \ \ +18. \ \ \ \ \ \ \
\ \ \ +19. \ \ \ \ \ \ \ \ \ \ +20. \ \ \ \ \ \ \ \ \ \ +21. \ \ \ \ \ \ \ \ \ \ +22. \ \ \ \ \ \ \ \ \ \ +23. \ \ \ \ \ \ \ \ \ \ +24. \ \ \ \ \ \ \ \ \ \ +25. \ \ \ \ \ \ \ \ \ \ +26. \ \ \ \ \ \ \ \ \ \ +27. \ \ \ \ \ \ \ \ \ \ +28. \ \ \ \ \ \ \ \ \ \ +29. \ \ \ \ \ \ \ \ \ \ +30. \ \ \ \ \ \ \ \ \ \ +31. \ \ \ \ \ \ \ \ \ \ +32. \ \ \ \ \ \ \ \ \ \ +33. \ \ \ \ \ \ \

\ \ \ \ \ \ \ +37. \ \ \ \ \ \ \

\ \ \ +38. \ \ \ \ \ \ \ \ \ \ +39. \ \ \ \ \ \ \ \ \ \ +40. \ \ \
\ \ \ \ \ \ \ +41. \ \ \ \ \ \ \ \ \ \ +42. \ \ \ \ \ *) (* Tokens controlling layout and fonts: regions. diff --git a/isar/Example-Tokens.thy b/isar/Example-Tokens.thy index 2106ccaf..46c9a2cc 100644 --- a/isar/Example-Tokens.thy +++ b/isar/Example-Tokens.thy @@ -4,7 +4,7 @@ View and process this document with Unicode Tokens engaged. For a more exhaustive test of token display, visit the test - file etc/isar/TokensAcid.thy + file etc/isar/TokensAcid.thy. Check the FAQ for more advice. $Id$ *) diff --git a/lib/unicode-tokens.el b/lib/unicode-tokens.el index 8b6e065b..92f78cf4 100644 --- a/lib/unicode-tokens.el +++ b/lib/unicode-tokens.el @@ -260,8 +260,8 @@ This is used for an approximate reverse mapping, see `unicode-tokens-paste'.") ;; (defconst unicode-tokens-font-family-alternatives '(("STIXGeneral" - "Lucida Grande" "Lucida Sans Unicode" - "DejaVu Sans Mono" "DejaVuLGC Sans Mono" "Apple Symbols") + "DejaVu Sans Mono" "DejaVuLGC Sans Mono" + "Lucida Grande" "Lucida Sans Unicode" "Apple Symbols") ("Script" "Lucida Calligraphy" "URW Chancery L" "Zapf Chancery") ("Fraktur" @@ -274,7 +274,8 @@ This is used for an approximate reverse mapping, see `unicode-tokens-paste'.") unicode-tokens-font-family-alternatives))) (defface unicode-tokens-symbol-font-face - '((t :family "STIXGeneral")) + '((t :family "STIXGeneral")) ;; best, but needs installation/config +; '((t :family "DejaVu Sans Mono")) ;; more reliable default on Ubuntu "The default font used for symbols. Only :family and :slant attributes are used." :group 'unicode-tokens-faces) -- cgit v1.2.3

\ \ \ +34. \ \ \ \ \ \ \ \ \ \ +35. \ \ \ \ \ \ \ \ \ \ +36. \ \ \

\ \ \ - 34. \ \ \ \ \ \ \ \ \ \ - 35. \ \ \ \ \ \ \ \ \ \ - 36. \ \ \