228 (* standard symbol kinds *) |
228 (* standard symbol kinds *) |
229 |
229 |
230 datatype kind = Letter | Digit | Quasi | Blank | Other; |
230 datatype kind = Letter | Digit | Quasi | Blank | Other; |
231 |
231 |
232 local |
232 local |
233 val symbol_kinds = Symtab.make |
233 val letter_symbols = |
234 [("\\<A>", Letter), |
234 Symtab.make_set [ |
235 ("\\<B>", Letter), |
235 "\\<A>", |
236 ("\\<C>", Letter), |
236 "\\<B>", |
237 ("\\<D>", Letter), |
237 "\\<C>", |
238 ("\\<E>", Letter), |
238 "\\<D>", |
239 ("\\<F>", Letter), |
239 "\\<E>", |
240 ("\\<G>", Letter), |
240 "\\<F>", |
241 ("\\<H>", Letter), |
241 "\\<G>", |
242 ("\\<I>", Letter), |
242 "\\<H>", |
243 ("\\<J>", Letter), |
243 "\\<I>", |
244 ("\\<K>", Letter), |
244 "\\<J>", |
245 ("\\<L>", Letter), |
245 "\\<K>", |
246 ("\\<M>", Letter), |
246 "\\<L>", |
247 ("\\<N>", Letter), |
247 "\\<M>", |
248 ("\\<O>", Letter), |
248 "\\<N>", |
249 ("\\<P>", Letter), |
249 "\\<O>", |
250 ("\\<Q>", Letter), |
250 "\\<P>", |
251 ("\\<R>", Letter), |
251 "\\<Q>", |
252 ("\\<S>", Letter), |
252 "\\<R>", |
253 ("\\<T>", Letter), |
253 "\\<S>", |
254 ("\\<U>", Letter), |
254 "\\<T>", |
255 ("\\<V>", Letter), |
255 "\\<U>", |
256 ("\\<W>", Letter), |
256 "\\<V>", |
257 ("\\<X>", Letter), |
257 "\\<W>", |
258 ("\\<Y>", Letter), |
258 "\\<X>", |
259 ("\\<Z>", Letter), |
259 "\\<Y>", |
260 ("\\<a>", Letter), |
260 "\\<Z>", |
261 ("\\<b>", Letter), |
261 "\\<a>", |
262 ("\\<c>", Letter), |
262 "\\<b>", |
263 ("\\<d>", Letter), |
263 "\\<c>", |
264 ("\\<e>", Letter), |
264 "\\<d>", |
265 ("\\<f>", Letter), |
265 "\\<e>", |
266 ("\\<g>", Letter), |
266 "\\<f>", |
267 ("\\<h>", Letter), |
267 "\\<g>", |
268 ("\\<i>", Letter), |
268 "\\<h>", |
269 ("\\<j>", Letter), |
269 "\\<i>", |
270 ("\\<k>", Letter), |
270 "\\<j>", |
271 ("\\<l>", Letter), |
271 "\\<k>", |
272 ("\\<m>", Letter), |
272 "\\<l>", |
273 ("\\<n>", Letter), |
273 "\\<m>", |
274 ("\\<o>", Letter), |
274 "\\<n>", |
275 ("\\<p>", Letter), |
275 "\\<o>", |
276 ("\\<q>", Letter), |
276 "\\<p>", |
277 ("\\<r>", Letter), |
277 "\\<q>", |
278 ("\\<s>", Letter), |
278 "\\<r>", |
279 ("\\<t>", Letter), |
279 "\\<s>", |
280 ("\\<u>", Letter), |
280 "\\<t>", |
281 ("\\<v>", Letter), |
281 "\\<u>", |
282 ("\\<w>", Letter), |
282 "\\<v>", |
283 ("\\<x>", Letter), |
283 "\\<w>", |
284 ("\\<y>", Letter), |
284 "\\<x>", |
285 ("\\<z>", Letter), |
285 "\\<y>", |
286 ("\\<AA>", Letter), |
286 "\\<z>", |
287 ("\\<BB>", Letter), |
287 "\\<AA>", |
288 ("\\<CC>", Letter), |
288 "\\<BB>", |
289 ("\\<DD>", Letter), |
289 "\\<CC>", |
290 ("\\<EE>", Letter), |
290 "\\<DD>", |
291 ("\\<FF>", Letter), |
291 "\\<EE>", |
292 ("\\<GG>", Letter), |
292 "\\<FF>", |
293 ("\\<HH>", Letter), |
293 "\\<GG>", |
294 ("\\<II>", Letter), |
294 "\\<HH>", |
295 ("\\<JJ>", Letter), |
295 "\\<II>", |
296 ("\\<KK>", Letter), |
296 "\\<JJ>", |
297 ("\\<LL>", Letter), |
297 "\\<KK>", |
298 ("\\<MM>", Letter), |
298 "\\<LL>", |
299 ("\\<NN>", Letter), |
299 "\\<MM>", |
300 ("\\<OO>", Letter), |
300 "\\<NN>", |
301 ("\\<PP>", Letter), |
301 "\\<OO>", |
302 ("\\<QQ>", Letter), |
302 "\\<PP>", |
303 ("\\<RR>", Letter), |
303 "\\<QQ>", |
304 ("\\<SS>", Letter), |
304 "\\<RR>", |
305 ("\\<TT>", Letter), |
305 "\\<SS>", |
306 ("\\<UU>", Letter), |
306 "\\<TT>", |
307 ("\\<VV>", Letter), |
307 "\\<UU>", |
308 ("\\<WW>", Letter), |
308 "\\<VV>", |
309 ("\\<XX>", Letter), |
309 "\\<WW>", |
310 ("\\<YY>", Letter), |
310 "\\<XX>", |
311 ("\\<ZZ>", Letter), |
311 "\\<YY>", |
312 ("\\<aa>", Letter), |
312 "\\<ZZ>", |
313 ("\\<bb>", Letter), |
313 "\\<aa>", |
314 ("\\<cc>", Letter), |
314 "\\<bb>", |
315 ("\\<dd>", Letter), |
315 "\\<cc>", |
316 ("\\<ee>", Letter), |
316 "\\<dd>", |
317 ("\\<ff>", Letter), |
317 "\\<ee>", |
318 ("\\<gg>", Letter), |
318 "\\<ff>", |
319 ("\\<hh>", Letter), |
319 "\\<gg>", |
320 ("\\<ii>", Letter), |
320 "\\<hh>", |
321 ("\\<jj>", Letter), |
321 "\\<ii>", |
322 ("\\<kk>", Letter), |
322 "\\<jj>", |
323 ("\\<ll>", Letter), |
323 "\\<kk>", |
324 ("\\<mm>", Letter), |
324 "\\<ll>", |
325 ("\\<nn>", Letter), |
325 "\\<mm>", |
326 ("\\<oo>", Letter), |
326 "\\<nn>", |
327 ("\\<pp>", Letter), |
327 "\\<oo>", |
328 ("\\<qq>", Letter), |
328 "\\<pp>", |
329 ("\\<rr>", Letter), |
329 "\\<qq>", |
330 ("\\<ss>", Letter), |
330 "\\<rr>", |
331 ("\\<tt>", Letter), |
331 "\\<ss>", |
332 ("\\<uu>", Letter), |
332 "\\<tt>", |
333 ("\\<vv>", Letter), |
333 "\\<uu>", |
334 ("\\<ww>", Letter), |
334 "\\<vv>", |
335 ("\\<xx>", Letter), |
335 "\\<ww>", |
336 ("\\<yy>", Letter), |
336 "\\<xx>", |
337 ("\\<zz>", Letter), |
337 "\\<yy>", |
338 ("\\<alpha>", Letter), |
338 "\\<zz>", |
339 ("\\<beta>", Letter), |
339 "\\<alpha>", |
340 ("\\<gamma>", Letter), |
340 "\\<beta>", |
341 ("\\<delta>", Letter), |
341 "\\<gamma>", |
342 ("\\<epsilon>", Letter), |
342 "\\<delta>", |
343 ("\\<zeta>", Letter), |
343 "\\<epsilon>", |
344 ("\\<eta>", Letter), |
344 "\\<zeta>", |
345 ("\\<theta>", Letter), |
345 "\\<eta>", |
346 ("\\<iota>", Letter), |
346 "\\<theta>", |
347 ("\\<kappa>", Letter), |
347 "\\<iota>", |
348 ("\\<lambda>", Other), (*sic!*) |
348 "\\<kappa>", |
349 ("\\<mu>", Letter), |
349 (*"\\<lambda>", sic!*) |
350 ("\\<nu>", Letter), |
350 "\\<mu>", |
351 ("\\<xi>", Letter), |
351 "\\<nu>", |
352 ("\\<pi>", Letter), |
352 "\\<xi>", |
353 ("\\<rho>", Letter), |
353 "\\<pi>", |
354 ("\\<sigma>", Letter), |
354 "\\<rho>", |
355 ("\\<tau>", Letter), |
355 "\\<sigma>", |
356 ("\\<upsilon>", Letter), |
356 "\\<tau>", |
357 ("\\<phi>", Letter), |
357 "\\<upsilon>", |
358 ("\\<chi>", Letter), |
358 "\\<phi>", |
359 ("\\<psi>", Letter), |
359 "\\<chi>", |
360 ("\\<omega>", Letter), |
360 "\\<psi>", |
361 ("\\<Gamma>", Letter), |
361 "\\<omega>", |
362 ("\\<Delta>", Letter), |
362 "\\<Gamma>", |
363 ("\\<Theta>", Letter), |
363 "\\<Delta>", |
364 ("\\<Lambda>", Letter), |
364 "\\<Theta>", |
365 ("\\<Xi>", Letter), |
365 "\\<Lambda>", |
366 ("\\<Pi>", Letter), |
366 "\\<Xi>", |
367 ("\\<Sigma>", Letter), |
367 "\\<Pi>", |
368 ("\\<Upsilon>", Letter), |
368 "\\<Sigma>", |
369 ("\\<Phi>", Letter), |
369 "\\<Upsilon>", |
370 ("\\<Psi>", Letter), |
370 "\\<Phi>", |
371 ("\\<Omega>", Letter), |
371 "\\<Psi>", |
372 ("\\<^isub>", Letter), |
372 "\\<Omega>", |
373 ("\\<^isup>", Letter)]; |
373 "\\<^isub>", |
|
374 "\\<^isup>" |
|
375 ]; |
374 in |
376 in |
375 fun kind s = |
377 fun kind s = |
376 if is_ascii_letter s then Letter |
378 if is_ascii_letter s then Letter |
377 else if is_ascii_digit s then Digit |
379 else if is_ascii_digit s then Digit |
378 else if is_ascii_quasi s then Quasi |
380 else if is_ascii_quasi s then Quasi |
379 else if is_ascii_blank s then Blank |
381 else if is_ascii_blank s then Blank |
380 else if is_char s then Other |
382 else if is_char s then Other |
381 else the_default Other (Symtab.lookup symbol_kinds s); |
383 else if Symtab.defined letter_symbols s then Letter |
|
384 else Other; |
382 end; |
385 end; |
383 |
386 |
384 fun is_letter s = kind s = Letter; |
387 fun is_letter s = kind s = Letter; |
385 fun is_digit s = kind s = Digit; |
388 fun is_digit s = kind s = Digit; |
386 fun is_quasi s = kind s = Quasi; |
389 fun is_quasi s = kind s = Quasi; |