--- a/src/Pure/General/symbol.ML Mon Nov 26 20:09:51 2012 +0100
+++ b/src/Pure/General/symbol.ML Mon Nov 26 20:29:40 2012 +0100
@@ -230,147 +230,149 @@
datatype kind = Letter | Digit | Quasi | Blank | Other;
local
- val symbol_kinds = Symtab.make
- [("\\<A>", Letter),
- ("\\<B>", Letter),
- ("\\<C>", Letter),
- ("\\<D>", Letter),
- ("\\<E>", Letter),
- ("\\<F>", Letter),
- ("\\<G>", Letter),
- ("\\<H>", Letter),
- ("\\<I>", Letter),
- ("\\<J>", Letter),
- ("\\<K>", Letter),
- ("\\<L>", Letter),
- ("\\<M>", Letter),
- ("\\<N>", Letter),
- ("\\<O>", Letter),
- ("\\<P>", Letter),
- ("\\<Q>", Letter),
- ("\\<R>", Letter),
- ("\\<S>", Letter),
- ("\\<T>", Letter),
- ("\\<U>", Letter),
- ("\\<V>", Letter),
- ("\\<W>", Letter),
- ("\\<X>", Letter),
- ("\\<Y>", Letter),
- ("\\<Z>", Letter),
- ("\\<a>", Letter),
- ("\\<b>", Letter),
- ("\\<c>", Letter),
- ("\\<d>", Letter),
- ("\\<e>", Letter),
- ("\\<f>", Letter),
- ("\\<g>", Letter),
- ("\\<h>", Letter),
- ("\\<i>", Letter),
- ("\\<j>", Letter),
- ("\\<k>", Letter),
- ("\\<l>", Letter),
- ("\\<m>", Letter),
- ("\\<n>", Letter),
- ("\\<o>", Letter),
- ("\\<p>", Letter),
- ("\\<q>", Letter),
- ("\\<r>", Letter),
- ("\\<s>", Letter),
- ("\\<t>", Letter),
- ("\\<u>", Letter),
- ("\\<v>", Letter),
- ("\\<w>", Letter),
- ("\\<x>", Letter),
- ("\\<y>", Letter),
- ("\\<z>", Letter),
- ("\\<AA>", Letter),
- ("\\<BB>", Letter),
- ("\\<CC>", Letter),
- ("\\<DD>", Letter),
- ("\\<EE>", Letter),
- ("\\<FF>", Letter),
- ("\\<GG>", Letter),
- ("\\<HH>", Letter),
- ("\\<II>", Letter),
- ("\\<JJ>", Letter),
- ("\\<KK>", Letter),
- ("\\<LL>", Letter),
- ("\\<MM>", Letter),
- ("\\<NN>", Letter),
- ("\\<OO>", Letter),
- ("\\<PP>", Letter),
- ("\\<QQ>", Letter),
- ("\\<RR>", Letter),
- ("\\<SS>", Letter),
- ("\\<TT>", Letter),
- ("\\<UU>", Letter),
- ("\\<VV>", Letter),
- ("\\<WW>", Letter),
- ("\\<XX>", Letter),
- ("\\<YY>", Letter),
- ("\\<ZZ>", Letter),
- ("\\<aa>", Letter),
- ("\\<bb>", Letter),
- ("\\<cc>", Letter),
- ("\\<dd>", Letter),
- ("\\<ee>", Letter),
- ("\\<ff>", Letter),
- ("\\<gg>", Letter),
- ("\\<hh>", Letter),
- ("\\<ii>", Letter),
- ("\\<jj>", Letter),
- ("\\<kk>", Letter),
- ("\\<ll>", Letter),
- ("\\<mm>", Letter),
- ("\\<nn>", Letter),
- ("\\<oo>", Letter),
- ("\\<pp>", Letter),
- ("\\<qq>", Letter),
- ("\\<rr>", Letter),
- ("\\<ss>", Letter),
- ("\\<tt>", Letter),
- ("\\<uu>", Letter),
- ("\\<vv>", Letter),
- ("\\<ww>", Letter),
- ("\\<xx>", Letter),
- ("\\<yy>", Letter),
- ("\\<zz>", Letter),
- ("\\<alpha>", Letter),
- ("\\<beta>", Letter),
- ("\\<gamma>", Letter),
- ("\\<delta>", Letter),
- ("\\<epsilon>", Letter),
- ("\\<zeta>", Letter),
- ("\\<eta>", Letter),
- ("\\<theta>", Letter),
- ("\\<iota>", Letter),
- ("\\<kappa>", Letter),
- ("\\<lambda>", Other), (*sic!*)
- ("\\<mu>", Letter),
- ("\\<nu>", Letter),
- ("\\<xi>", Letter),
- ("\\<pi>", Letter),
- ("\\<rho>", Letter),
- ("\\<sigma>", Letter),
- ("\\<tau>", Letter),
- ("\\<upsilon>", Letter),
- ("\\<phi>", Letter),
- ("\\<chi>", Letter),
- ("\\<psi>", Letter),
- ("\\<omega>", Letter),
- ("\\<Gamma>", Letter),
- ("\\<Delta>", Letter),
- ("\\<Theta>", Letter),
- ("\\<Lambda>", Letter),
- ("\\<Xi>", Letter),
- ("\\<Pi>", Letter),
- ("\\<Sigma>", Letter),
- ("\\<Upsilon>", Letter),
- ("\\<Phi>", Letter),
- ("\\<Psi>", Letter),
- ("\\<Omega>", Letter),
- ("\\<^isub>", Letter),
- ("\\<^isup>", Letter)];
+ val letter_symbols =
+ Symtab.make_set [
+ "\\<A>",
+ "\\<B>",
+ "\\<C>",
+ "\\<D>",
+ "\\<E>",
+ "\\<F>",
+ "\\<G>",
+ "\\<H>",
+ "\\<I>",
+ "\\<J>",
+ "\\<K>",
+ "\\<L>",
+ "\\<M>",
+ "\\<N>",
+ "\\<O>",
+ "\\<P>",
+ "\\<Q>",
+ "\\<R>",
+ "\\<S>",
+ "\\<T>",
+ "\\<U>",
+ "\\<V>",
+ "\\<W>",
+ "\\<X>",
+ "\\<Y>",
+ "\\<Z>",
+ "\\<a>",
+ "\\<b>",
+ "\\<c>",
+ "\\<d>",
+ "\\<e>",
+ "\\<f>",
+ "\\<g>",
+ "\\<h>",
+ "\\<i>",
+ "\\<j>",
+ "\\<k>",
+ "\\<l>",
+ "\\<m>",
+ "\\<n>",
+ "\\<o>",
+ "\\<p>",
+ "\\<q>",
+ "\\<r>",
+ "\\<s>",
+ "\\<t>",
+ "\\<u>",
+ "\\<v>",
+ "\\<w>",
+ "\\<x>",
+ "\\<y>",
+ "\\<z>",
+ "\\<AA>",
+ "\\<BB>",
+ "\\<CC>",
+ "\\<DD>",
+ "\\<EE>",
+ "\\<FF>",
+ "\\<GG>",
+ "\\<HH>",
+ "\\<II>",
+ "\\<JJ>",
+ "\\<KK>",
+ "\\<LL>",
+ "\\<MM>",
+ "\\<NN>",
+ "\\<OO>",
+ "\\<PP>",
+ "\\<QQ>",
+ "\\<RR>",
+ "\\<SS>",
+ "\\<TT>",
+ "\\<UU>",
+ "\\<VV>",
+ "\\<WW>",
+ "\\<XX>",
+ "\\<YY>",
+ "\\<ZZ>",
+ "\\<aa>",
+ "\\<bb>",
+ "\\<cc>",
+ "\\<dd>",
+ "\\<ee>",
+ "\\<ff>",
+ "\\<gg>",
+ "\\<hh>",
+ "\\<ii>",
+ "\\<jj>",
+ "\\<kk>",
+ "\\<ll>",
+ "\\<mm>",
+ "\\<nn>",
+ "\\<oo>",
+ "\\<pp>",
+ "\\<qq>",
+ "\\<rr>",
+ "\\<ss>",
+ "\\<tt>",
+ "\\<uu>",
+ "\\<vv>",
+ "\\<ww>",
+ "\\<xx>",
+ "\\<yy>",
+ "\\<zz>",
+ "\\<alpha>",
+ "\\<beta>",
+ "\\<gamma>",
+ "\\<delta>",
+ "\\<epsilon>",
+ "\\<zeta>",
+ "\\<eta>",
+ "\\<theta>",
+ "\\<iota>",
+ "\\<kappa>",
+ (*"\\<lambda>", sic!*)
+ "\\<mu>",
+ "\\<nu>",
+ "\\<xi>",
+ "\\<pi>",
+ "\\<rho>",
+ "\\<sigma>",
+ "\\<tau>",
+ "\\<upsilon>",
+ "\\<phi>",
+ "\\<chi>",
+ "\\<psi>",
+ "\\<omega>",
+ "\\<Gamma>",
+ "\\<Delta>",
+ "\\<Theta>",
+ "\\<Lambda>",
+ "\\<Xi>",
+ "\\<Pi>",
+ "\\<Sigma>",
+ "\\<Upsilon>",
+ "\\<Phi>",
+ "\\<Psi>",
+ "\\<Omega>",
+ "\\<^isub>",
+ "\\<^isup>"
+ ];
in
fun kind s =
if is_ascii_letter s then Letter
@@ -378,7 +380,8 @@
else if is_ascii_quasi s then Quasi
else if is_ascii_blank s then Blank
else if is_char s then Other
- else the_default Other (Symtab.lookup symbol_kinds s);
+ else if Symtab.defined letter_symbols s then Letter
+ else Other;
end;
fun is_letter s = kind s = Letter;