author | wenzelm |
Fri, 31 Jul 1998 11:33:30 +0200 | |
changeset 5229 | 7c8abffc4413 |
parent 5112 | 9e74cf11e4a4 |
child 5870 | 5d4fc952be47 |
permissions | -rw-r--r-- |
4687
8cec457a8961
replaced Pure/Syntax/symbol_font.ML by Pure/Syntax/symbol.ML;
wenzelm
parents:
diff
changeset
|
1 |
(* Title: Pure/Syntax/symbol.ML |
8cec457a8961
replaced Pure/Syntax/symbol_font.ML by Pure/Syntax/symbol.ML;
wenzelm
parents:
diff
changeset
|
2 |
ID: $Id$ |
8cec457a8961
replaced Pure/Syntax/symbol_font.ML by Pure/Syntax/symbol.ML;
wenzelm
parents:
diff
changeset
|
3 |
Author: Markus Wenzel, TU Muenchen |
8cec457a8961
replaced Pure/Syntax/symbol_font.ML by Pure/Syntax/symbol.ML;
wenzelm
parents:
diff
changeset
|
4 |
|
4901 | 5 |
Generalized characters. |
4687
8cec457a8961
replaced Pure/Syntax/symbol_font.ML by Pure/Syntax/symbol.ML;
wenzelm
parents:
diff
changeset
|
6 |
*) |
8cec457a8961
replaced Pure/Syntax/symbol_font.ML by Pure/Syntax/symbol.ML;
wenzelm
parents:
diff
changeset
|
7 |
|
8cec457a8961
replaced Pure/Syntax/symbol_font.ML by Pure/Syntax/symbol.ML;
wenzelm
parents:
diff
changeset
|
8 |
signature SYMBOL = |
8cec457a8961
replaced Pure/Syntax/symbol_font.ML by Pure/Syntax/symbol.ML;
wenzelm
parents:
diff
changeset
|
9 |
sig |
8cec457a8961
replaced Pure/Syntax/symbol_font.ML by Pure/Syntax/symbol.ML;
wenzelm
parents:
diff
changeset
|
10 |
type symbol |
4901 | 11 |
val space: symbol |
4687
8cec457a8961
replaced Pure/Syntax/symbol_font.ML by Pure/Syntax/symbol.ML;
wenzelm
parents:
diff
changeset
|
12 |
val eof: symbol |
8cec457a8961
replaced Pure/Syntax/symbol_font.ML by Pure/Syntax/symbol.ML;
wenzelm
parents:
diff
changeset
|
13 |
val is_eof: symbol -> bool |
8cec457a8961
replaced Pure/Syntax/symbol_font.ML by Pure/Syntax/symbol.ML;
wenzelm
parents:
diff
changeset
|
14 |
val not_eof: symbol -> bool |
4938 | 15 |
val stopper: symbol * (symbol -> bool) |
4687
8cec457a8961
replaced Pure/Syntax/symbol_font.ML by Pure/Syntax/symbol.ML;
wenzelm
parents:
diff
changeset
|
16 |
val is_ascii: symbol -> bool |
8cec457a8961
replaced Pure/Syntax/symbol_font.ML by Pure/Syntax/symbol.ML;
wenzelm
parents:
diff
changeset
|
17 |
val is_letter: symbol -> bool |
8cec457a8961
replaced Pure/Syntax/symbol_font.ML by Pure/Syntax/symbol.ML;
wenzelm
parents:
diff
changeset
|
18 |
val is_digit: symbol -> bool |
8cec457a8961
replaced Pure/Syntax/symbol_font.ML by Pure/Syntax/symbol.ML;
wenzelm
parents:
diff
changeset
|
19 |
val is_quasi_letter: symbol -> bool |
8cec457a8961
replaced Pure/Syntax/symbol_font.ML by Pure/Syntax/symbol.ML;
wenzelm
parents:
diff
changeset
|
20 |
val is_letdig: symbol -> bool |
8cec457a8961
replaced Pure/Syntax/symbol_font.ML by Pure/Syntax/symbol.ML;
wenzelm
parents:
diff
changeset
|
21 |
val is_blank: symbol -> bool |
8cec457a8961
replaced Pure/Syntax/symbol_font.ML by Pure/Syntax/symbol.ML;
wenzelm
parents:
diff
changeset
|
22 |
val is_printable: symbol -> bool |
5112 | 23 |
val beginning: symbol list -> string |
4687
8cec457a8961
replaced Pure/Syntax/symbol_font.ML by Pure/Syntax/symbol.ML;
wenzelm
parents:
diff
changeset
|
24 |
val scan: string list -> symbol * string list |
8cec457a8961
replaced Pure/Syntax/symbol_font.ML by Pure/Syntax/symbol.ML;
wenzelm
parents:
diff
changeset
|
25 |
val explode: string -> symbol list |
5229 | 26 |
val length: symbol list -> int |
27 |
val size: string -> int |
|
4687
8cec457a8961
replaced Pure/Syntax/symbol_font.ML by Pure/Syntax/symbol.ML;
wenzelm
parents:
diff
changeset
|
28 |
val input: string -> string |
8cec457a8961
replaced Pure/Syntax/symbol_font.ML by Pure/Syntax/symbol.ML;
wenzelm
parents:
diff
changeset
|
29 |
val output: string -> string |
4959 | 30 |
val source: bool -> (string, 'a) Source.source -> |
31 |
(symbol, (string, 'a) Source.source) Source.source |
|
4687
8cec457a8961
replaced Pure/Syntax/symbol_font.ML by Pure/Syntax/symbol.ML;
wenzelm
parents:
diff
changeset
|
32 |
end; |
8cec457a8961
replaced Pure/Syntax/symbol_font.ML by Pure/Syntax/symbol.ML;
wenzelm
parents:
diff
changeset
|
33 |
|
8cec457a8961
replaced Pure/Syntax/symbol_font.ML by Pure/Syntax/symbol.ML;
wenzelm
parents:
diff
changeset
|
34 |
structure Symbol: SYMBOL = |
8cec457a8961
replaced Pure/Syntax/symbol_font.ML by Pure/Syntax/symbol.ML;
wenzelm
parents:
diff
changeset
|
35 |
struct |
8cec457a8961
replaced Pure/Syntax/symbol_font.ML by Pure/Syntax/symbol.ML;
wenzelm
parents:
diff
changeset
|
36 |
|
8cec457a8961
replaced Pure/Syntax/symbol_font.ML by Pure/Syntax/symbol.ML;
wenzelm
parents:
diff
changeset
|
37 |
|
8cec457a8961
replaced Pure/Syntax/symbol_font.ML by Pure/Syntax/symbol.ML;
wenzelm
parents:
diff
changeset
|
38 |
(** encoding table (isabelle-0) **) |
8cec457a8961
replaced Pure/Syntax/symbol_font.ML by Pure/Syntax/symbol.ML;
wenzelm
parents:
diff
changeset
|
39 |
|
8cec457a8961
replaced Pure/Syntax/symbol_font.ML by Pure/Syntax/symbol.ML;
wenzelm
parents:
diff
changeset
|
40 |
val enc_start = 160; |
8cec457a8961
replaced Pure/Syntax/symbol_font.ML by Pure/Syntax/symbol.ML;
wenzelm
parents:
diff
changeset
|
41 |
val enc_end = 255; |
8cec457a8961
replaced Pure/Syntax/symbol_font.ML by Pure/Syntax/symbol.ML;
wenzelm
parents:
diff
changeset
|
42 |
|
8cec457a8961
replaced Pure/Syntax/symbol_font.ML by Pure/Syntax/symbol.ML;
wenzelm
parents:
diff
changeset
|
43 |
val enc_vector = |
8cec457a8961
replaced Pure/Syntax/symbol_font.ML by Pure/Syntax/symbol.ML;
wenzelm
parents:
diff
changeset
|
44 |
[ |
8cec457a8961
replaced Pure/Syntax/symbol_font.ML by Pure/Syntax/symbol.ML;
wenzelm
parents:
diff
changeset
|
45 |
(* GENERATED TEXT FOLLOWS - Do not edit! *) |
8cec457a8961
replaced Pure/Syntax/symbol_font.ML by Pure/Syntax/symbol.ML;
wenzelm
parents:
diff
changeset
|
46 |
"\\<space2>", |
8cec457a8961
replaced Pure/Syntax/symbol_font.ML by Pure/Syntax/symbol.ML;
wenzelm
parents:
diff
changeset
|
47 |
"\\<Gamma>", |
8cec457a8961
replaced Pure/Syntax/symbol_font.ML by Pure/Syntax/symbol.ML;
wenzelm
parents:
diff
changeset
|
48 |
"\\<Delta>", |
8cec457a8961
replaced Pure/Syntax/symbol_font.ML by Pure/Syntax/symbol.ML;
wenzelm
parents:
diff
changeset
|
49 |
"\\<Theta>", |
8cec457a8961
replaced Pure/Syntax/symbol_font.ML by Pure/Syntax/symbol.ML;
wenzelm
parents:
diff
changeset
|
50 |
"\\<Lambda>", |
8cec457a8961
replaced Pure/Syntax/symbol_font.ML by Pure/Syntax/symbol.ML;
wenzelm
parents:
diff
changeset
|
51 |
"\\<Pi>", |
8cec457a8961
replaced Pure/Syntax/symbol_font.ML by Pure/Syntax/symbol.ML;
wenzelm
parents:
diff
changeset
|
52 |
"\\<Sigma>", |
8cec457a8961
replaced Pure/Syntax/symbol_font.ML by Pure/Syntax/symbol.ML;
wenzelm
parents:
diff
changeset
|
53 |
"\\<Phi>", |
8cec457a8961
replaced Pure/Syntax/symbol_font.ML by Pure/Syntax/symbol.ML;
wenzelm
parents:
diff
changeset
|
54 |
"\\<Psi>", |
8cec457a8961
replaced Pure/Syntax/symbol_font.ML by Pure/Syntax/symbol.ML;
wenzelm
parents:
diff
changeset
|
55 |
"\\<Omega>", |
8cec457a8961
replaced Pure/Syntax/symbol_font.ML by Pure/Syntax/symbol.ML;
wenzelm
parents:
diff
changeset
|
56 |
"\\<alpha>", |
8cec457a8961
replaced Pure/Syntax/symbol_font.ML by Pure/Syntax/symbol.ML;
wenzelm
parents:
diff
changeset
|
57 |
"\\<beta>", |
8cec457a8961
replaced Pure/Syntax/symbol_font.ML by Pure/Syntax/symbol.ML;
wenzelm
parents:
diff
changeset
|
58 |
"\\<gamma>", |
8cec457a8961
replaced Pure/Syntax/symbol_font.ML by Pure/Syntax/symbol.ML;
wenzelm
parents:
diff
changeset
|
59 |
"\\<delta>", |
8cec457a8961
replaced Pure/Syntax/symbol_font.ML by Pure/Syntax/symbol.ML;
wenzelm
parents:
diff
changeset
|
60 |
"\\<epsilon>", |
8cec457a8961
replaced Pure/Syntax/symbol_font.ML by Pure/Syntax/symbol.ML;
wenzelm
parents:
diff
changeset
|
61 |
"\\<zeta>", |
8cec457a8961
replaced Pure/Syntax/symbol_font.ML by Pure/Syntax/symbol.ML;
wenzelm
parents:
diff
changeset
|
62 |
"\\<eta>", |
8cec457a8961
replaced Pure/Syntax/symbol_font.ML by Pure/Syntax/symbol.ML;
wenzelm
parents:
diff
changeset
|
63 |
"\\<theta>", |
8cec457a8961
replaced Pure/Syntax/symbol_font.ML by Pure/Syntax/symbol.ML;
wenzelm
parents:
diff
changeset
|
64 |
"\\<kappa>", |
8cec457a8961
replaced Pure/Syntax/symbol_font.ML by Pure/Syntax/symbol.ML;
wenzelm
parents:
diff
changeset
|
65 |
"\\<lambda>", |
8cec457a8961
replaced Pure/Syntax/symbol_font.ML by Pure/Syntax/symbol.ML;
wenzelm
parents:
diff
changeset
|
66 |
"\\<mu>", |
8cec457a8961
replaced Pure/Syntax/symbol_font.ML by Pure/Syntax/symbol.ML;
wenzelm
parents:
diff
changeset
|
67 |
"\\<nu>", |
8cec457a8961
replaced Pure/Syntax/symbol_font.ML by Pure/Syntax/symbol.ML;
wenzelm
parents:
diff
changeset
|
68 |
"\\<xi>", |
8cec457a8961
replaced Pure/Syntax/symbol_font.ML by Pure/Syntax/symbol.ML;
wenzelm
parents:
diff
changeset
|
69 |
"\\<pi>", |
8cec457a8961
replaced Pure/Syntax/symbol_font.ML by Pure/Syntax/symbol.ML;
wenzelm
parents:
diff
changeset
|
70 |
"\\<rho>", |
8cec457a8961
replaced Pure/Syntax/symbol_font.ML by Pure/Syntax/symbol.ML;
wenzelm
parents:
diff
changeset
|
71 |
"\\<sigma>", |
8cec457a8961
replaced Pure/Syntax/symbol_font.ML by Pure/Syntax/symbol.ML;
wenzelm
parents:
diff
changeset
|
72 |
"\\<tau>", |
8cec457a8961
replaced Pure/Syntax/symbol_font.ML by Pure/Syntax/symbol.ML;
wenzelm
parents:
diff
changeset
|
73 |
"\\<phi>", |
8cec457a8961
replaced Pure/Syntax/symbol_font.ML by Pure/Syntax/symbol.ML;
wenzelm
parents:
diff
changeset
|
74 |
"\\<chi>", |
8cec457a8961
replaced Pure/Syntax/symbol_font.ML by Pure/Syntax/symbol.ML;
wenzelm
parents:
diff
changeset
|
75 |
"\\<psi>", |
8cec457a8961
replaced Pure/Syntax/symbol_font.ML by Pure/Syntax/symbol.ML;
wenzelm
parents:
diff
changeset
|
76 |
"\\<omega>", |
8cec457a8961
replaced Pure/Syntax/symbol_font.ML by Pure/Syntax/symbol.ML;
wenzelm
parents:
diff
changeset
|
77 |
"\\<not>", |
8cec457a8961
replaced Pure/Syntax/symbol_font.ML by Pure/Syntax/symbol.ML;
wenzelm
parents:
diff
changeset
|
78 |
"\\<and>", |
8cec457a8961
replaced Pure/Syntax/symbol_font.ML by Pure/Syntax/symbol.ML;
wenzelm
parents:
diff
changeset
|
79 |
"\\<or>", |
8cec457a8961
replaced Pure/Syntax/symbol_font.ML by Pure/Syntax/symbol.ML;
wenzelm
parents:
diff
changeset
|
80 |
"\\<forall>", |
8cec457a8961
replaced Pure/Syntax/symbol_font.ML by Pure/Syntax/symbol.ML;
wenzelm
parents:
diff
changeset
|
81 |
"\\<exists>", |
8cec457a8961
replaced Pure/Syntax/symbol_font.ML by Pure/Syntax/symbol.ML;
wenzelm
parents:
diff
changeset
|
82 |
"\\<And>", |
8cec457a8961
replaced Pure/Syntax/symbol_font.ML by Pure/Syntax/symbol.ML;
wenzelm
parents:
diff
changeset
|
83 |
"\\<lceil>", |
8cec457a8961
replaced Pure/Syntax/symbol_font.ML by Pure/Syntax/symbol.ML;
wenzelm
parents:
diff
changeset
|
84 |
"\\<rceil>", |
8cec457a8961
replaced Pure/Syntax/symbol_font.ML by Pure/Syntax/symbol.ML;
wenzelm
parents:
diff
changeset
|
85 |
"\\<lfloor>", |
8cec457a8961
replaced Pure/Syntax/symbol_font.ML by Pure/Syntax/symbol.ML;
wenzelm
parents:
diff
changeset
|
86 |
"\\<rfloor>", |
8cec457a8961
replaced Pure/Syntax/symbol_font.ML by Pure/Syntax/symbol.ML;
wenzelm
parents:
diff
changeset
|
87 |
"\\<turnstile>", |
8cec457a8961
replaced Pure/Syntax/symbol_font.ML by Pure/Syntax/symbol.ML;
wenzelm
parents:
diff
changeset
|
88 |
"\\<Turnstile>", |
8cec457a8961
replaced Pure/Syntax/symbol_font.ML by Pure/Syntax/symbol.ML;
wenzelm
parents:
diff
changeset
|
89 |
"\\<lbrakk>", |
8cec457a8961
replaced Pure/Syntax/symbol_font.ML by Pure/Syntax/symbol.ML;
wenzelm
parents:
diff
changeset
|
90 |
"\\<rbrakk>", |
8cec457a8961
replaced Pure/Syntax/symbol_font.ML by Pure/Syntax/symbol.ML;
wenzelm
parents:
diff
changeset
|
91 |
"\\<cdot>", |
8cec457a8961
replaced Pure/Syntax/symbol_font.ML by Pure/Syntax/symbol.ML;
wenzelm
parents:
diff
changeset
|
92 |
"\\<in>", |
8cec457a8961
replaced Pure/Syntax/symbol_font.ML by Pure/Syntax/symbol.ML;
wenzelm
parents:
diff
changeset
|
93 |
"\\<subseteq>", |
8cec457a8961
replaced Pure/Syntax/symbol_font.ML by Pure/Syntax/symbol.ML;
wenzelm
parents:
diff
changeset
|
94 |
"\\<inter>", |
8cec457a8961
replaced Pure/Syntax/symbol_font.ML by Pure/Syntax/symbol.ML;
wenzelm
parents:
diff
changeset
|
95 |
"\\<union>", |
8cec457a8961
replaced Pure/Syntax/symbol_font.ML by Pure/Syntax/symbol.ML;
wenzelm
parents:
diff
changeset
|
96 |
"\\<Inter>", |
8cec457a8961
replaced Pure/Syntax/symbol_font.ML by Pure/Syntax/symbol.ML;
wenzelm
parents:
diff
changeset
|
97 |
"\\<Union>", |
8cec457a8961
replaced Pure/Syntax/symbol_font.ML by Pure/Syntax/symbol.ML;
wenzelm
parents:
diff
changeset
|
98 |
"\\<sqinter>", |
8cec457a8961
replaced Pure/Syntax/symbol_font.ML by Pure/Syntax/symbol.ML;
wenzelm
parents:
diff
changeset
|
99 |
"\\<squnion>", |
8cec457a8961
replaced Pure/Syntax/symbol_font.ML by Pure/Syntax/symbol.ML;
wenzelm
parents:
diff
changeset
|
100 |
"\\<Sqinter>", |
8cec457a8961
replaced Pure/Syntax/symbol_font.ML by Pure/Syntax/symbol.ML;
wenzelm
parents:
diff
changeset
|
101 |
"\\<Squnion>", |
8cec457a8961
replaced Pure/Syntax/symbol_font.ML by Pure/Syntax/symbol.ML;
wenzelm
parents:
diff
changeset
|
102 |
"\\<bottom>", |
8cec457a8961
replaced Pure/Syntax/symbol_font.ML by Pure/Syntax/symbol.ML;
wenzelm
parents:
diff
changeset
|
103 |
"\\<doteq>", |
8cec457a8961
replaced Pure/Syntax/symbol_font.ML by Pure/Syntax/symbol.ML;
wenzelm
parents:
diff
changeset
|
104 |
"\\<equiv>", |
8cec457a8961
replaced Pure/Syntax/symbol_font.ML by Pure/Syntax/symbol.ML;
wenzelm
parents:
diff
changeset
|
105 |
"\\<noteq>", |
8cec457a8961
replaced Pure/Syntax/symbol_font.ML by Pure/Syntax/symbol.ML;
wenzelm
parents:
diff
changeset
|
106 |
"\\<sqsubset>", |
8cec457a8961
replaced Pure/Syntax/symbol_font.ML by Pure/Syntax/symbol.ML;
wenzelm
parents:
diff
changeset
|
107 |
"\\<sqsubseteq>", |
8cec457a8961
replaced Pure/Syntax/symbol_font.ML by Pure/Syntax/symbol.ML;
wenzelm
parents:
diff
changeset
|
108 |
"\\<prec>", |
8cec457a8961
replaced Pure/Syntax/symbol_font.ML by Pure/Syntax/symbol.ML;
wenzelm
parents:
diff
changeset
|
109 |
"\\<preceq>", |
8cec457a8961
replaced Pure/Syntax/symbol_font.ML by Pure/Syntax/symbol.ML;
wenzelm
parents:
diff
changeset
|
110 |
"\\<succ>", |
8cec457a8961
replaced Pure/Syntax/symbol_font.ML by Pure/Syntax/symbol.ML;
wenzelm
parents:
diff
changeset
|
111 |
"\\<approx>", |
8cec457a8961
replaced Pure/Syntax/symbol_font.ML by Pure/Syntax/symbol.ML;
wenzelm
parents:
diff
changeset
|
112 |
"\\<sim>", |
8cec457a8961
replaced Pure/Syntax/symbol_font.ML by Pure/Syntax/symbol.ML;
wenzelm
parents:
diff
changeset
|
113 |
"\\<simeq>", |
8cec457a8961
replaced Pure/Syntax/symbol_font.ML by Pure/Syntax/symbol.ML;
wenzelm
parents:
diff
changeset
|
114 |
"\\<le>", |
8cec457a8961
replaced Pure/Syntax/symbol_font.ML by Pure/Syntax/symbol.ML;
wenzelm
parents:
diff
changeset
|
115 |
"\\<Colon>", |
8cec457a8961
replaced Pure/Syntax/symbol_font.ML by Pure/Syntax/symbol.ML;
wenzelm
parents:
diff
changeset
|
116 |
"\\<leftarrow>", |
8cec457a8961
replaced Pure/Syntax/symbol_font.ML by Pure/Syntax/symbol.ML;
wenzelm
parents:
diff
changeset
|
117 |
"\\<midarrow>", |
8cec457a8961
replaced Pure/Syntax/symbol_font.ML by Pure/Syntax/symbol.ML;
wenzelm
parents:
diff
changeset
|
118 |
"\\<rightarrow>", |
8cec457a8961
replaced Pure/Syntax/symbol_font.ML by Pure/Syntax/symbol.ML;
wenzelm
parents:
diff
changeset
|
119 |
"\\<Leftarrow>", |
8cec457a8961
replaced Pure/Syntax/symbol_font.ML by Pure/Syntax/symbol.ML;
wenzelm
parents:
diff
changeset
|
120 |
"\\<Midarrow>", |
8cec457a8961
replaced Pure/Syntax/symbol_font.ML by Pure/Syntax/symbol.ML;
wenzelm
parents:
diff
changeset
|
121 |
"\\<Rightarrow>", |
8cec457a8961
replaced Pure/Syntax/symbol_font.ML by Pure/Syntax/symbol.ML;
wenzelm
parents:
diff
changeset
|
122 |
"\\<bow>", |
8cec457a8961
replaced Pure/Syntax/symbol_font.ML by Pure/Syntax/symbol.ML;
wenzelm
parents:
diff
changeset
|
123 |
"\\<mapsto>", |
8cec457a8961
replaced Pure/Syntax/symbol_font.ML by Pure/Syntax/symbol.ML;
wenzelm
parents:
diff
changeset
|
124 |
"\\<leadsto>", |
8cec457a8961
replaced Pure/Syntax/symbol_font.ML by Pure/Syntax/symbol.ML;
wenzelm
parents:
diff
changeset
|
125 |
"\\<up>", |
8cec457a8961
replaced Pure/Syntax/symbol_font.ML by Pure/Syntax/symbol.ML;
wenzelm
parents:
diff
changeset
|
126 |
"\\<down>", |
8cec457a8961
replaced Pure/Syntax/symbol_font.ML by Pure/Syntax/symbol.ML;
wenzelm
parents:
diff
changeset
|
127 |
"\\<notin>", |
8cec457a8961
replaced Pure/Syntax/symbol_font.ML by Pure/Syntax/symbol.ML;
wenzelm
parents:
diff
changeset
|
128 |
"\\<times>", |
8cec457a8961
replaced Pure/Syntax/symbol_font.ML by Pure/Syntax/symbol.ML;
wenzelm
parents:
diff
changeset
|
129 |
"\\<oplus>", |
8cec457a8961
replaced Pure/Syntax/symbol_font.ML by Pure/Syntax/symbol.ML;
wenzelm
parents:
diff
changeset
|
130 |
"\\<ominus>", |
8cec457a8961
replaced Pure/Syntax/symbol_font.ML by Pure/Syntax/symbol.ML;
wenzelm
parents:
diff
changeset
|
131 |
"\\<otimes>", |
8cec457a8961
replaced Pure/Syntax/symbol_font.ML by Pure/Syntax/symbol.ML;
wenzelm
parents:
diff
changeset
|
132 |
"\\<oslash>", |
8cec457a8961
replaced Pure/Syntax/symbol_font.ML by Pure/Syntax/symbol.ML;
wenzelm
parents:
diff
changeset
|
133 |
"\\<subset>", |
8cec457a8961
replaced Pure/Syntax/symbol_font.ML by Pure/Syntax/symbol.ML;
wenzelm
parents:
diff
changeset
|
134 |
"\\<infinity>", |
8cec457a8961
replaced Pure/Syntax/symbol_font.ML by Pure/Syntax/symbol.ML;
wenzelm
parents:
diff
changeset
|
135 |
"\\<box>", |
8cec457a8961
replaced Pure/Syntax/symbol_font.ML by Pure/Syntax/symbol.ML;
wenzelm
parents:
diff
changeset
|
136 |
"\\<diamond>", |
8cec457a8961
replaced Pure/Syntax/symbol_font.ML by Pure/Syntax/symbol.ML;
wenzelm
parents:
diff
changeset
|
137 |
"\\<circ>", |
8cec457a8961
replaced Pure/Syntax/symbol_font.ML by Pure/Syntax/symbol.ML;
wenzelm
parents:
diff
changeset
|
138 |
"\\<bullet>", |
8cec457a8961
replaced Pure/Syntax/symbol_font.ML by Pure/Syntax/symbol.ML;
wenzelm
parents:
diff
changeset
|
139 |
"\\<parallel>", |
8cec457a8961
replaced Pure/Syntax/symbol_font.ML by Pure/Syntax/symbol.ML;
wenzelm
parents:
diff
changeset
|
140 |
"\\<surd>", |
8cec457a8961
replaced Pure/Syntax/symbol_font.ML by Pure/Syntax/symbol.ML;
wenzelm
parents:
diff
changeset
|
141 |
"\\<copyright>" |
8cec457a8961
replaced Pure/Syntax/symbol_font.ML by Pure/Syntax/symbol.ML;
wenzelm
parents:
diff
changeset
|
142 |
(* END OF GENERATED TEXT *) |
8cec457a8961
replaced Pure/Syntax/symbol_font.ML by Pure/Syntax/symbol.ML;
wenzelm
parents:
diff
changeset
|
143 |
]; |
8cec457a8961
replaced Pure/Syntax/symbol_font.ML by Pure/Syntax/symbol.ML;
wenzelm
parents:
diff
changeset
|
144 |
|
8cec457a8961
replaced Pure/Syntax/symbol_font.ML by Pure/Syntax/symbol.ML;
wenzelm
parents:
diff
changeset
|
145 |
val enc_rel = enc_vector ~~ map chr (enc_start upto enc_end); |
8cec457a8961
replaced Pure/Syntax/symbol_font.ML by Pure/Syntax/symbol.ML;
wenzelm
parents:
diff
changeset
|
146 |
|
8cec457a8961
replaced Pure/Syntax/symbol_font.ML by Pure/Syntax/symbol.ML;
wenzelm
parents:
diff
changeset
|
147 |
val char_tab = Symtab.make enc_rel; |
8cec457a8961
replaced Pure/Syntax/symbol_font.ML by Pure/Syntax/symbol.ML;
wenzelm
parents:
diff
changeset
|
148 |
val symbol_tab = Symtab.make (map swap enc_rel); |
8cec457a8961
replaced Pure/Syntax/symbol_font.ML by Pure/Syntax/symbol.ML;
wenzelm
parents:
diff
changeset
|
149 |
|
8cec457a8961
replaced Pure/Syntax/symbol_font.ML by Pure/Syntax/symbol.ML;
wenzelm
parents:
diff
changeset
|
150 |
fun lookup_symbol c = |
8cec457a8961
replaced Pure/Syntax/symbol_font.ML by Pure/Syntax/symbol.ML;
wenzelm
parents:
diff
changeset
|
151 |
if ord c < enc_start then None |
8cec457a8961
replaced Pure/Syntax/symbol_font.ML by Pure/Syntax/symbol.ML;
wenzelm
parents:
diff
changeset
|
152 |
else Symtab.lookup (symbol_tab, c); |
8cec457a8961
replaced Pure/Syntax/symbol_font.ML by Pure/Syntax/symbol.ML;
wenzelm
parents:
diff
changeset
|
153 |
|
8cec457a8961
replaced Pure/Syntax/symbol_font.ML by Pure/Syntax/symbol.ML;
wenzelm
parents:
diff
changeset
|
154 |
|
8cec457a8961
replaced Pure/Syntax/symbol_font.ML by Pure/Syntax/symbol.ML;
wenzelm
parents:
diff
changeset
|
155 |
(* encode / decode *) |
8cec457a8961
replaced Pure/Syntax/symbol_font.ML by Pure/Syntax/symbol.ML;
wenzelm
parents:
diff
changeset
|
156 |
|
8cec457a8961
replaced Pure/Syntax/symbol_font.ML by Pure/Syntax/symbol.ML;
wenzelm
parents:
diff
changeset
|
157 |
fun char s = if_none (Symtab.lookup (char_tab, s)) s; |
8cec457a8961
replaced Pure/Syntax/symbol_font.ML by Pure/Syntax/symbol.ML;
wenzelm
parents:
diff
changeset
|
158 |
fun symbol c = if_none (lookup_symbol c) c; |
8cec457a8961
replaced Pure/Syntax/symbol_font.ML by Pure/Syntax/symbol.ML;
wenzelm
parents:
diff
changeset
|
159 |
|
8cec457a8961
replaced Pure/Syntax/symbol_font.ML by Pure/Syntax/symbol.ML;
wenzelm
parents:
diff
changeset
|
160 |
fun symbol' c = |
8cec457a8961
replaced Pure/Syntax/symbol_font.ML by Pure/Syntax/symbol.ML;
wenzelm
parents:
diff
changeset
|
161 |
(case lookup_symbol c of |
8cec457a8961
replaced Pure/Syntax/symbol_font.ML by Pure/Syntax/symbol.ML;
wenzelm
parents:
diff
changeset
|
162 |
None => c |
8cec457a8961
replaced Pure/Syntax/symbol_font.ML by Pure/Syntax/symbol.ML;
wenzelm
parents:
diff
changeset
|
163 |
| Some s => "\\" ^ s); |
8cec457a8961
replaced Pure/Syntax/symbol_font.ML by Pure/Syntax/symbol.ML;
wenzelm
parents:
diff
changeset
|
164 |
|
8cec457a8961
replaced Pure/Syntax/symbol_font.ML by Pure/Syntax/symbol.ML;
wenzelm
parents:
diff
changeset
|
165 |
|
8cec457a8961
replaced Pure/Syntax/symbol_font.ML by Pure/Syntax/symbol.ML;
wenzelm
parents:
diff
changeset
|
166 |
|
8cec457a8961
replaced Pure/Syntax/symbol_font.ML by Pure/Syntax/symbol.ML;
wenzelm
parents:
diff
changeset
|
167 |
(** type symbol **) |
8cec457a8961
replaced Pure/Syntax/symbol_font.ML by Pure/Syntax/symbol.ML;
wenzelm
parents:
diff
changeset
|
168 |
|
8cec457a8961
replaced Pure/Syntax/symbol_font.ML by Pure/Syntax/symbol.ML;
wenzelm
parents:
diff
changeset
|
169 |
type symbol = string; |
8cec457a8961
replaced Pure/Syntax/symbol_font.ML by Pure/Syntax/symbol.ML;
wenzelm
parents:
diff
changeset
|
170 |
|
4901 | 171 |
val space = " "; |
172 |
val eof = ""; |
|
173 |
||
4687
8cec457a8961
replaced Pure/Syntax/symbol_font.ML by Pure/Syntax/symbol.ML;
wenzelm
parents:
diff
changeset
|
174 |
|
8cec457a8961
replaced Pure/Syntax/symbol_font.ML by Pure/Syntax/symbol.ML;
wenzelm
parents:
diff
changeset
|
175 |
(* kinds *) |
8cec457a8961
replaced Pure/Syntax/symbol_font.ML by Pure/Syntax/symbol.ML;
wenzelm
parents:
diff
changeset
|
176 |
|
8cec457a8961
replaced Pure/Syntax/symbol_font.ML by Pure/Syntax/symbol.ML;
wenzelm
parents:
diff
changeset
|
177 |
fun is_eof s = s = eof; |
8cec457a8961
replaced Pure/Syntax/symbol_font.ML by Pure/Syntax/symbol.ML;
wenzelm
parents:
diff
changeset
|
178 |
fun not_eof s = s <> eof; |
4938 | 179 |
val stopper = (eof, is_eof); |
4687
8cec457a8961
replaced Pure/Syntax/symbol_font.ML by Pure/Syntax/symbol.ML;
wenzelm
parents:
diff
changeset
|
180 |
|
8cec457a8961
replaced Pure/Syntax/symbol_font.ML by Pure/Syntax/symbol.ML;
wenzelm
parents:
diff
changeset
|
181 |
fun is_ascii s = size s = 1 andalso ord s < 128; |
8cec457a8961
replaced Pure/Syntax/symbol_font.ML by Pure/Syntax/symbol.ML;
wenzelm
parents:
diff
changeset
|
182 |
|
8cec457a8961
replaced Pure/Syntax/symbol_font.ML by Pure/Syntax/symbol.ML;
wenzelm
parents:
diff
changeset
|
183 |
fun is_letter s = |
8cec457a8961
replaced Pure/Syntax/symbol_font.ML by Pure/Syntax/symbol.ML;
wenzelm
parents:
diff
changeset
|
184 |
size s = 1 andalso |
8cec457a8961
replaced Pure/Syntax/symbol_font.ML by Pure/Syntax/symbol.ML;
wenzelm
parents:
diff
changeset
|
185 |
(ord "A" <= ord s andalso ord s <= ord "Z" orelse |
8cec457a8961
replaced Pure/Syntax/symbol_font.ML by Pure/Syntax/symbol.ML;
wenzelm
parents:
diff
changeset
|
186 |
ord "a" <= ord s andalso ord s <= ord "z"); |
8cec457a8961
replaced Pure/Syntax/symbol_font.ML by Pure/Syntax/symbol.ML;
wenzelm
parents:
diff
changeset
|
187 |
|
8cec457a8961
replaced Pure/Syntax/symbol_font.ML by Pure/Syntax/symbol.ML;
wenzelm
parents:
diff
changeset
|
188 |
fun is_digit s = |
8cec457a8961
replaced Pure/Syntax/symbol_font.ML by Pure/Syntax/symbol.ML;
wenzelm
parents:
diff
changeset
|
189 |
size s = 1 andalso ord "0" <= ord s andalso ord s <= ord "9"; |
8cec457a8961
replaced Pure/Syntax/symbol_font.ML by Pure/Syntax/symbol.ML;
wenzelm
parents:
diff
changeset
|
190 |
|
8cec457a8961
replaced Pure/Syntax/symbol_font.ML by Pure/Syntax/symbol.ML;
wenzelm
parents:
diff
changeset
|
191 |
fun is_quasi_letter "_" = true |
8cec457a8961
replaced Pure/Syntax/symbol_font.ML by Pure/Syntax/symbol.ML;
wenzelm
parents:
diff
changeset
|
192 |
| is_quasi_letter "'" = true |
8cec457a8961
replaced Pure/Syntax/symbol_font.ML by Pure/Syntax/symbol.ML;
wenzelm
parents:
diff
changeset
|
193 |
| is_quasi_letter s = is_letter s; |
8cec457a8961
replaced Pure/Syntax/symbol_font.ML by Pure/Syntax/symbol.ML;
wenzelm
parents:
diff
changeset
|
194 |
|
8cec457a8961
replaced Pure/Syntax/symbol_font.ML by Pure/Syntax/symbol.ML;
wenzelm
parents:
diff
changeset
|
195 |
val is_blank = |
4715 | 196 |
fn " " => true | "\t" => true | "\n" => true | "\^L" => true |
197 |
| "\160" => true | "\\<space2>" => true |
|
4687
8cec457a8961
replaced Pure/Syntax/symbol_font.ML by Pure/Syntax/symbol.ML;
wenzelm
parents:
diff
changeset
|
198 |
| _ => false; |
8cec457a8961
replaced Pure/Syntax/symbol_font.ML by Pure/Syntax/symbol.ML;
wenzelm
parents:
diff
changeset
|
199 |
|
8cec457a8961
replaced Pure/Syntax/symbol_font.ML by Pure/Syntax/symbol.ML;
wenzelm
parents:
diff
changeset
|
200 |
val is_letdig = is_quasi_letter orf is_digit; |
8cec457a8961
replaced Pure/Syntax/symbol_font.ML by Pure/Syntax/symbol.ML;
wenzelm
parents:
diff
changeset
|
201 |
|
8cec457a8961
replaced Pure/Syntax/symbol_font.ML by Pure/Syntax/symbol.ML;
wenzelm
parents:
diff
changeset
|
202 |
fun is_printable s = |
8cec457a8961
replaced Pure/Syntax/symbol_font.ML by Pure/Syntax/symbol.ML;
wenzelm
parents:
diff
changeset
|
203 |
size s = 1 andalso ord " " <= ord s andalso ord s <= ord "~" orelse |
8cec457a8961
replaced Pure/Syntax/symbol_font.ML by Pure/Syntax/symbol.ML;
wenzelm
parents:
diff
changeset
|
204 |
size s > 2 andalso nth_elem (2, explode s) <> "^"; |
8cec457a8961
replaced Pure/Syntax/symbol_font.ML by Pure/Syntax/symbol.ML;
wenzelm
parents:
diff
changeset
|
205 |
|
8cec457a8961
replaced Pure/Syntax/symbol_font.ML by Pure/Syntax/symbol.ML;
wenzelm
parents:
diff
changeset
|
206 |
|
5112 | 207 |
(* beginning *) |
208 |
||
209 |
val smash_blanks = map (fn s => if is_blank s then space else s); |
|
210 |
||
211 |
fun beginning raw_ss = |
|
212 |
let |
|
213 |
val (all_ss, _) = take_suffix is_blank raw_ss; |
|
214 |
val dots = if length all_ss > 10 then " ..." else ""; |
|
215 |
val (ss, _) = take_suffix is_blank (take (10, all_ss)); |
|
216 |
in implode (smash_blanks ss) ^ dots end; |
|
217 |
||
218 |
||
4687
8cec457a8961
replaced Pure/Syntax/symbol_font.ML by Pure/Syntax/symbol.ML;
wenzelm
parents:
diff
changeset
|
219 |
(* scan *) |
8cec457a8961
replaced Pure/Syntax/symbol_font.ML by Pure/Syntax/symbol.ML;
wenzelm
parents:
diff
changeset
|
220 |
|
8cec457a8961
replaced Pure/Syntax/symbol_font.ML by Pure/Syntax/symbol.ML;
wenzelm
parents:
diff
changeset
|
221 |
val scan_id = Scan.one is_letter ^^ (Scan.any is_letdig >> implode); |
8cec457a8961
replaced Pure/Syntax/symbol_font.ML by Pure/Syntax/symbol.ML;
wenzelm
parents:
diff
changeset
|
222 |
|
8cec457a8961
replaced Pure/Syntax/symbol_font.ML by Pure/Syntax/symbol.ML;
wenzelm
parents:
diff
changeset
|
223 |
val scan = |
8cec457a8961
replaced Pure/Syntax/symbol_font.ML by Pure/Syntax/symbol.ML;
wenzelm
parents:
diff
changeset
|
224 |
($$ "\\" --| Scan.optional ($$ "\\") "") ^^ $$ "<" ^^ |
4921 | 225 |
!! (fn (cs, _) => "Malformed symbolic character specification: \\" ^ "<" ^ beginning cs) |
4687
8cec457a8961
replaced Pure/Syntax/symbol_font.ML by Pure/Syntax/symbol.ML;
wenzelm
parents:
diff
changeset
|
226 |
(Scan.optional ($$ "^") "" ^^ scan_id ^^ $$ ">") || |
8cec457a8961
replaced Pure/Syntax/symbol_font.ML by Pure/Syntax/symbol.ML;
wenzelm
parents:
diff
changeset
|
227 |
Scan.one not_eof; |
8cec457a8961
replaced Pure/Syntax/symbol_font.ML by Pure/Syntax/symbol.ML;
wenzelm
parents:
diff
changeset
|
228 |
|
8cec457a8961
replaced Pure/Syntax/symbol_font.ML by Pure/Syntax/symbol.ML;
wenzelm
parents:
diff
changeset
|
229 |
|
4959 | 230 |
(* source *) |
231 |
||
232 |
val recover = Scan.any1 ((not o is_blank) andf not_eof); |
|
233 |
||
234 |
fun source do_recover src = |
|
235 |
Source.source stopper (Scan.bulk scan) (if do_recover then Some recover else None) src; |
|
236 |
||
237 |
||
4687
8cec457a8961
replaced Pure/Syntax/symbol_font.ML by Pure/Syntax/symbol.ML;
wenzelm
parents:
diff
changeset
|
238 |
(* explode *) |
8cec457a8961
replaced Pure/Syntax/symbol_font.ML by Pure/Syntax/symbol.ML;
wenzelm
parents:
diff
changeset
|
239 |
|
8cec457a8961
replaced Pure/Syntax/symbol_font.ML by Pure/Syntax/symbol.ML;
wenzelm
parents:
diff
changeset
|
240 |
fun no_syms [] = true |
8cec457a8961
replaced Pure/Syntax/symbol_font.ML by Pure/Syntax/symbol.ML;
wenzelm
parents:
diff
changeset
|
241 |
| no_syms ("\\" :: "<" :: _) = false |
8cec457a8961
replaced Pure/Syntax/symbol_font.ML by Pure/Syntax/symbol.ML;
wenzelm
parents:
diff
changeset
|
242 |
| no_syms (c :: cs) = ord c < enc_start andalso no_syms cs; |
8cec457a8961
replaced Pure/Syntax/symbol_font.ML by Pure/Syntax/symbol.ML;
wenzelm
parents:
diff
changeset
|
243 |
|
8cec457a8961
replaced Pure/Syntax/symbol_font.ML by Pure/Syntax/symbol.ML;
wenzelm
parents:
diff
changeset
|
244 |
fun sym_explode str = |
8cec457a8961
replaced Pure/Syntax/symbol_font.ML by Pure/Syntax/symbol.ML;
wenzelm
parents:
diff
changeset
|
245 |
let val chs = explode str in |
4901 | 246 |
if no_syms chs then chs (*tune trivial case*) |
4938 | 247 |
else map symbol (#1 (Scan.error (Scan.finite stopper (Scan.repeat scan)) chs)) |
4687
8cec457a8961
replaced Pure/Syntax/symbol_font.ML by Pure/Syntax/symbol.ML;
wenzelm
parents:
diff
changeset
|
248 |
end; |
8cec457a8961
replaced Pure/Syntax/symbol_font.ML by Pure/Syntax/symbol.ML;
wenzelm
parents:
diff
changeset
|
249 |
|
8cec457a8961
replaced Pure/Syntax/symbol_font.ML by Pure/Syntax/symbol.ML;
wenzelm
parents:
diff
changeset
|
250 |
|
5229 | 251 |
(* printable length *) |
252 |
||
253 |
fun sym_length ss = foldl (fn (n, c) => if is_printable c then n + 1 else n) (0, ss); |
|
254 |
val sym_size = sym_length o sym_explode; |
|
255 |
||
256 |
||
4687
8cec457a8961
replaced Pure/Syntax/symbol_font.ML by Pure/Syntax/symbol.ML;
wenzelm
parents:
diff
changeset
|
257 |
(* input / output *) |
8cec457a8961
replaced Pure/Syntax/symbol_font.ML by Pure/Syntax/symbol.ML;
wenzelm
parents:
diff
changeset
|
258 |
|
8cec457a8961
replaced Pure/Syntax/symbol_font.ML by Pure/Syntax/symbol.ML;
wenzelm
parents:
diff
changeset
|
259 |
fun input str = |
8cec457a8961
replaced Pure/Syntax/symbol_font.ML by Pure/Syntax/symbol.ML;
wenzelm
parents:
diff
changeset
|
260 |
let val chs = explode str in |
8cec457a8961
replaced Pure/Syntax/symbol_font.ML by Pure/Syntax/symbol.ML;
wenzelm
parents:
diff
changeset
|
261 |
if forall (fn c => ord c < enc_start) chs then str |
8cec457a8961
replaced Pure/Syntax/symbol_font.ML by Pure/Syntax/symbol.ML;
wenzelm
parents:
diff
changeset
|
262 |
else implode (map symbol' chs) |
8cec457a8961
replaced Pure/Syntax/symbol_font.ML by Pure/Syntax/symbol.ML;
wenzelm
parents:
diff
changeset
|
263 |
end; |
8cec457a8961
replaced Pure/Syntax/symbol_font.ML by Pure/Syntax/symbol.ML;
wenzelm
parents:
diff
changeset
|
264 |
|
8cec457a8961
replaced Pure/Syntax/symbol_font.ML by Pure/Syntax/symbol.ML;
wenzelm
parents:
diff
changeset
|
265 |
val output = implode o map char o sym_explode; |
8cec457a8961
replaced Pure/Syntax/symbol_font.ML by Pure/Syntax/symbol.ML;
wenzelm
parents:
diff
changeset
|
266 |
|
8cec457a8961
replaced Pure/Syntax/symbol_font.ML by Pure/Syntax/symbol.ML;
wenzelm
parents:
diff
changeset
|
267 |
|
5229 | 268 |
(*final declarations of this structure!*) |
4687
8cec457a8961
replaced Pure/Syntax/symbol_font.ML by Pure/Syntax/symbol.ML;
wenzelm
parents:
diff
changeset
|
269 |
val explode = sym_explode; |
5229 | 270 |
val length = sym_length; |
271 |
val size = sym_size; |
|
4687
8cec457a8961
replaced Pure/Syntax/symbol_font.ML by Pure/Syntax/symbol.ML;
wenzelm
parents:
diff
changeset
|
272 |
|
8cec457a8961
replaced Pure/Syntax/symbol_font.ML by Pure/Syntax/symbol.ML;
wenzelm
parents:
diff
changeset
|
273 |
|
8cec457a8961
replaced Pure/Syntax/symbol_font.ML by Pure/Syntax/symbol.ML;
wenzelm
parents:
diff
changeset
|
274 |
end; |