Change default Unicode Tokens font back to DejaVU Sans, more reliable without installing STIX.

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. \<Longrightarrow>) 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"  
 
@@ -76,45 +132,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. \<Longrightarrow>) 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).
-
------------------------------------------------------------------
-
 
 Q. I'm afraid I got stuck very early on.  I sent the following line:
 
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.  \<leftarrow>	\<rightarrow>	\<Leftarrow>	\<Rightarrow>	\<leftrightarrow>	\<Leftrightarrow>	\<mapsto>	\<longleftarrow>	\<Longleftarrow>	\<longrightarrow>
-   2.  \<Longrightarrow>	\<longleftrightarrow>	\<Longleftrightarrow>	\<longmapsto>	\<midarrow>	\<Midarrow>	\<hookleftarrow>	\<hookrightarrow>	\<leftharpoondown>	\<rightharpoondown>
-   3.  \<leftharpoonup>	\<rightharpoonup>	\<rightleftharpoons>	\<leadsto>	\<downharpoonleft>	\<downharpoonright>	\<upharpoonleft>	\<upharpoonright>	\<restriction>	\<Colon>
-   4.  \<up>	\<Up>	\<down>	\<Down>	\<updown>	\<Updown>	\<langle>	\<rangle>	\<lceil>	\<rceil>
-   5.  \<lfloor>	\<rfloor>	\<lparr>	\<rparr>	\<lbrakk>	\<rbrakk>	\<lbrace>	\<rbrace>	\<guillemotleft>	\<guillemotright>
-   6.  \<bottom>	\<top>	\<and>	\<And>	\<or>	\<Or>	\<forall>	\<exists>	\<nexists>	\<not>
-   7.  \<box>	\<diamond>	\<turnstile>	\<Turnstile>	\<tturnstile>	\<TTurnstile>	\<stileturn>	\<surd>	\<le>	\<ge>
-   8.  \<lless>	\<ggreater>	\<lesssim>	\<greatersim>	\<lessapprox>	\<greaterapprox>	\<in>	\<notin>	\<subset>	\<supset>
-   9.  \<subseteq>	\<supseteq>	\<sqsubset>	\<sqsupset>	\<sqsubseteq>	\<sqsupseteq>	\<inter>	\<Inter>	\<union>	\<Union>
-  10.  \<squnion>	\<Squnion>	\<sqinter>	\<Sqinter>	\<setminus>	\<propto>	\<uplus>	\<Uplus>	\<noteq>	\<sim>
-  11.  \<doteq>	\<simeq>	\<approx>	\<asymp>	\<cong>	\<smile>	\<equiv>	\<frown>	\<Join>	\<bowtie>
-  12.  \<prec>	\<succ>	\<preceq>	\<succeq>	\<parallel>	\<bar>	\<plusminus>	\<minusplus>	\<times>	\<div>
-  13.  \<cdot>	\<star>	\<bullet>	\<circ>	\<dagger>	\<ddagger>	\<lhd>	\<rhd>	\<unlhd>	\<unrhd>
-  14.  \<triangleleft>	\<triangleright>	\<triangle>	\<triangleq>	\<oplus>	\<Oplus>	\<otimes>	\<Otimes>	\<odot>	\<Odot>
-  15.  \<ominus>	\<oslash>	\<dots>	\<cdots>	\<Sum>	\<Prod>	\<Coprod>	\<infinity>	\<integral>	\<ointegral>
-  16.  \<clubsuit>	\<diamondsuit>	\<heartsuit>	\<spadesuit>	\<aleph>	\<emptyset>	\<nabla>	\<partial>	\<Re>	\<Im>
-  17.  \<flat>	\<natural>	\<sharp>	\<angle>	\<copyright>	\<registered>	\<hyphen>	\<inverse>	\<onesuperior>	\<twosuperior>
-  18.  \<threesuperior>	\<onequarter>	\<onehalf>	\<threequarters>	\<ordmasculine>	\<ordfeminine>	\<section>	\<paragraph>	\<exclamdown>	\<questiondown>
-  19.  \<euro>	\<pounds>	\<yen>	\<cent>	\<currency>	\<degree>	\<amalg>	\<mho>	\<lozenge>	\<wp>
-  20.  \<wrong>	\<struct>	\<acute>	\<index>	\<dieresis>	\<cedilla>	\<hungarumlaut>	\<spacespace>	\<module>	\<some>
-  21.  \<stareq>	\<defeq>	\<questioneq>	\<vartheta>	\<varpi>	\<varrho>	\<varsigma>	\<varphi>	\<hbar>	\<ell>
-  22.  \<ast>	\<bigcirc>	\<bigtriangleup>	\<bigtriangledown>	\<ni>	\<mid>	\<notlt>	\<notle>	\<notprec>	\<notpreceq>
-  23.  \<notsubset>	\<notsubseteq>	\<notsqsubseteq>	\<notgt>	\<notge>	\<notsucc>	\<notsucceq>	\<notsupset>	\<notsupseteq>	\<notsqsupseteq>
-  24.  \<notequiv>	\<notsim>	\<notsimeq>	\<notapprox>	\<notcong>	\<notasymp>	\<nearrow>	\<searrow>	\<swarrow>	\<nwarrow>
-  25.  \<vdots>	\<ddots>	\<closequote>	\<openquote>	\<opendblquote>	\<closedblquote>	\<emdash>	\<prime>	\<doubleprime>	\<tripleprime>
-  26.  \<quadrupleprime>	\<nbspace>	\<thinspace>	\<notni>	\<colonequals>	\<foursuperior>	\<fivesuperior>	\<sixsuperior>	\<sevensuperior>	\<eightsuperior>
-  27.  \<ninesuperior>	\<bool>	\<complex>	\<nat>	\<rat>	\<real>	\<int>	\<alpha>	\<beta>	\<gamma>
-  28.  \<delta>	\<epsilon>	\<zeta>	\<eta>	\<theta>	\<iota>	\<kappa>	\<lambda>	\<mu>	\<nu>
-  29.  \<xi>	\<pi>	\<rho>	\<sigma>	\<tau>	\<upsilon>	\<phi>	\<chi>	\<psi>	\<omega>
-  30.  \<Gamma>	\<Delta>	\<Theta>	\<Lambda>	\<Xi>	\<Pi>	\<Sigma>	\<Upsilon>	\<Phi>	\<Psi>
-  31.  \<Omega>	\<zero>	\<one>	\<two>	\<three>	\<four>	\<five>	\<six>	\<seven>	\<eight>
-  32.  \<nine>	\<A>	\<B>	\<C>	\<D>	\<E>	\<F>	\<G>	\<H>	\<I>
-  33.  \<J>	\<K>	\<L>	\<M>	\<N>	\<O>	\<P>	\<Q>	\<R>	\<S>
-  34.  \<T>	\<U>	\<V>	\<W>	\<X>	\<Y>	\<Z>	\<a>	\<b>	\<c>
-  35.  \<d>	\<e>	\<f>	\<g>	\<h>	\<i>	\<j>	\<k>	\<l>	\<m>
-  36.  \<n>	\<o>	\<p>	\<q>	\<r>	\<s>	\<t>	\<u>	\<v>	\<w>
-  37.  \<x>	\<y>	\<z>	\<AA>	\<BB>	\<CC>	\<DD>	\<EE>	\<FF>	\<GG>
-  38.  \<HH>	\<II>	\<JJ>	\<KK>	\<LL>	\<MM>	\<NN>	\<OO>	\<PP>	\<QQ>
-  39.  \<RR>	\<SS>	\<TT>	\<UU>	\<VV>	\<WW>	\<XX>	\<YY>	\<ZZ>	\<aa>
-  40.  \<bb>	\<cc>	\<dd>	\<ee>	\<ff>	\<gg>	\<hh>	\<ii>	\<jj>	\<kk>
-  41.  \<ll>	\<mm>	\<nn>	\<oo>	\<pp>	\<qq>	\<rr>	\<ss>	\<tt>	\<uu>
-  42.  \<vv>	\<ww>	\<xx>	\<yy>	\<zz>	 	 	 	 	 
+   Unfortunately 
+
+
+ 1.  \<leftarrow>	\<rightarrow>	\<Leftarrow>	\<Rightarrow>	\<leftrightarrow>	\<Leftrightarrow>	\<mapsto>	\<longleftarrow>	\<Longleftarrow>	\<longrightarrow>
+ 2.  \<Longrightarrow>	\<longleftrightarrow>	\<Longleftrightarrow>	\<longmapsto>	\<midarrow>	\<Midarrow>	\<hookleftarrow>	\<hookrightarrow>	\<leftharpoondown>	\<rightharpoondown>
+ 3.  \<leftharpoonup>	\<rightharpoonup>	\<rightleftharpoons>	\<leadsto>	\<downharpoonleft>	\<downharpoonright>	\<upharpoonleft>	\<upharpoonright>	\<restriction>	\<Colon>
+ 4.  \<up>	\<Up>	\<down>	\<Down>	\<updown>	\<Updown>	\<langle>	\<rangle>	\<lceil>	\<rceil>
+ 5.  \<lfloor>	\<rfloor>	\<lparr>	\<rparr>	\<lbrakk>	\<rbrakk>	\<lbrace>	\<rbrace>	\<guillemotleft>	\<guillemotright>
+ 6.  \<bottom>	\<top>	\<and>	\<And>	\<or>	\<Or>	\<forall>	\<exists>	\<nexists>	\<not>
+ 7.  \<box>	\<diamond>	\<turnstile>	\<Turnstile>	\<tturnstile>	\<TTurnstile>	\<stileturn>	\<surd>	\<le>	\<ge>
+ 8.  \<lless>	\<ggreater>	\<lesssim>	\<greatersim>	\<lessapprox>	\<greaterapprox>	\<in>	\<notin>	\<subset>	\<supset>
+ 9.  \<subseteq>	\<supseteq>	\<sqsubset>	\<sqsupset>	\<sqsubseteq>	\<sqsupseteq>	\<inter>	\<Inter>	\<union>	\<Union>
+10.  \<squnion>	\<Squnion>	\<sqinter>	\<Sqinter>	\<setminus>	\<propto>	\<uplus>	\<Uplus>	\<noteq>	\<sim>
+11.  \<doteq>	\<simeq>	\<approx>	\<asymp>	\<cong>	\<smile>	\<equiv>	\<frown>	\<Join>	\<bowtie>
+12.  \<prec>	\<succ>	\<preceq>	\<succeq>	\<parallel>	\<bar>	\<plusminus>	\<minusplus>	\<times>	\<div>
+13.  \<cdot>	\<star>	\<bullet>	\<circ>	\<dagger>	\<ddagger>	\<lhd>	\<rhd>	\<unlhd>	\<unrhd>
+14.  \<triangleleft>	\<triangleright>	\<triangle>	\<triangleq>	\<oplus>	\<Oplus>	\<otimes>	\<Otimes>	\<odot>	\<Odot>
+15.  \<ominus>	\<oslash>	\<dots>	\<cdots>	\<Sum>	\<Prod>	\<Coprod>	\<infinity>	\<integral>	\<ointegral>
+16.  \<clubsuit>	\<diamondsuit>	\<heartsuit>	\<spadesuit>	\<aleph>	\<emptyset>	\<nabla>	\<partial>	\<Re>	\<Im>
+17.  \<flat>	\<natural>	\<sharp>	\<angle>	\<copyright>	\<registered>	\<hyphen>	\<inverse>	\<onesuperior>	\<twosuperior>
+18.  \<threesuperior>	\<onequarter>	\<onehalf>	\<threequarters>	\<ordmasculine>	\<ordfeminine>	\<section>	\<paragraph>	\<exclamdown>	\<questiondown>
+19.  \<euro>	\<pounds>	\<yen>	\<cent>	\<currency>	\<degree>	\<amalg>	\<mho>	\<lozenge>	\<wp>
+20.  \<wrong>	\<struct>	\<acute>	\<index>	\<dieresis>	\<cedilla>	\<hungarumlaut>	\<spacespace>	\<module>	\<some>
+21.  \<stareq>	\<defeq>	\<questioneq>	\<vartheta>	\<varpi>	\<varrho>	\<varsigma>	\<varphi>	\<hbar>	\<ell>
+22.  \<ast>	\<bigcirc>	\<bigtriangleup>	\<bigtriangledown>	\<ni>	\<mid>	\<notlt>	\<notle>	\<notprec>	\<notpreceq>
+23.  \<notsubset>	\<notsubseteq>	\<notsqsubseteq>	\<notgt>	\<notge>	\<notsucc>	\<notsucceq>	\<notsupset>	\<notsupseteq>	\<notsqsupseteq>
+24.  \<notequiv>	\<notsim>	\<notsimeq>	\<notapprox>	\<notcong>	\<notasymp>	\<nearrow>	\<searrow>	\<swarrow>	\<nwarrow>
+25.  \<vdots>	\<ddots>	\<closequote>	\<openquote>	\<opendblquote>	\<closedblquote>	\<emdash>	\<prime>	\<doubleprime>	\<tripleprime>
+26.  \<quadrupleprime>	\<nbspace>	\<thinspace>	\<notni>	\<colonequals>	\<foursuperior>	\<fivesuperior>	\<sixsuperior>	\<sevensuperior>	\<eightsuperior>
+27.  \<ninesuperior>	\<bool>	\<complex>	\<nat>	\<rat>	\<real>	\<int>	\<alpha>	\<beta>	\<gamma>
+28.  \<delta>	\<epsilon>	\<zeta>	\<eta>	\<theta>	\<iota>	\<kappa>	\<lambda>	\<mu>	\<nu>
+29.  \<xi>	\<pi>	\<rho>	\<sigma>	\<tau>	\<upsilon>	\<phi>	\<chi>	\<psi>	\<omega>
+30.  \<Gamma>	\<Delta>	\<Theta>	\<Lambda>	\<Xi>	\<Pi>	\<Sigma>	\<Upsilon>	\<Phi>	\<Psi>
+31.  \<Omega>	\<zero>	\<one>	\<two>	\<three>	\<four>	\<five>	\<six>	\<seven>	\<eight>
+32.  \<nine>	\<A>	\<B>	\<C>	\<D>	\<E>	\<F>	\<G>	\<H>	\<I>
+33.  \<J>	\<K>	\<L>	\<M>	\<N>	\<O>	\<P>	\<Q>	\<R>	\<S>
+34.  \<T>	\<U>	\<V>	\<W>	\<X>	\<Y>	\<Z>	\<a>	\<b>	\<c>
+35.  \<d>	\<e>	\<f>	\<g>	\<h>	\<i>	\<j>	\<k>	\<l>	\<m>
+36.  \<n>	\<o>	\<p>	\<q>	\<r>	\<s>	\<t>	\<u>	\<v>	\<w>
+37.  \<x>	\<y>	\<z>	\<AA>	\<BB>	\<CC>	\<DD>	\<EE>	\<FF>	\<GG>
+38.  \<HH>	\<II>	\<JJ>	\<KK>	\<LL>	\<MM>	\<NN>	\<OO>	\<PP>	\<QQ>
+39.  \<RR>	\<SS>	\<TT>	\<UU>	\<VV>	\<WW>	\<XX>	\<YY>	\<ZZ>	\<aa>
+40.  \<bb>	\<cc>	\<dd>	\<ee>	\<ff>	\<gg>	\<hh>	\<ii>	\<jj>	\<kk>
+41.  \<ll>	\<mm>	\<nn>	\<oo>	\<pp>	\<qq>	\<rr>	\<ss>	\<tt>	\<uu>
+42.  \<vv>	\<ww>	\<xx>	\<yy>	\<zz>	 	 	 	 	 
 *)
 
 (* 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)