author | wenzelm |
Wed, 31 Jan 2001 22:14:53 +0100 | |
changeset 11010 | 2c6559297be3 |
parent 10953 | ea024d025463 |
child 12116 | 4027b15377a5 |
permissions | -rw-r--r-- |
6118 | 1 |
(* Title: Pure/General/symbol.ML |
6116
8ba2f25610f7
files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff
changeset
|
2 |
ID: $Id$ |
8ba2f25610f7
files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff
changeset
|
3 |
Author: Markus Wenzel, TU Muenchen |
8806 | 4 |
License: GPL (GNU GENERAL PUBLIC LICENSE) |
6116
8ba2f25610f7
files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff
changeset
|
5 |
|
8806 | 6 |
Generalized characters, independent of encoding. |
6116
8ba2f25610f7
files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff
changeset
|
7 |
*) |
8ba2f25610f7
files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff
changeset
|
8 |
|
8ba2f25610f7
files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff
changeset
|
9 |
signature SYMBOL = |
8ba2f25610f7
files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff
changeset
|
10 |
sig |
8ba2f25610f7
files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff
changeset
|
11 |
type symbol |
8ba2f25610f7
files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff
changeset
|
12 |
val space: symbol |
10953 | 13 |
val spaces: int -> symbol |
6857 | 14 |
val sync: symbol |
15 |
val is_sync: symbol -> bool |
|
16 |
val not_sync: symbol -> bool |
|
10747 | 17 |
val malformed: symbol |
6116
8ba2f25610f7
files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff
changeset
|
18 |
val eof: symbol |
8ba2f25610f7
files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff
changeset
|
19 |
val is_eof: symbol -> bool |
8ba2f25610f7
files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff
changeset
|
20 |
val not_eof: symbol -> bool |
8ba2f25610f7
files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff
changeset
|
21 |
val stopper: symbol * (symbol -> bool) |
8ba2f25610f7
files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff
changeset
|
22 |
val is_ascii: symbol -> bool |
8ba2f25610f7
files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff
changeset
|
23 |
val is_letter: symbol -> bool |
8ba2f25610f7
files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff
changeset
|
24 |
val is_digit: symbol -> bool |
8ba2f25610f7
files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff
changeset
|
25 |
val is_quasi_letter: symbol -> bool |
8ba2f25610f7
files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff
changeset
|
26 |
val is_letdig: symbol -> bool |
8ba2f25610f7
files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff
changeset
|
27 |
val is_blank: symbol -> bool |
8230 | 28 |
val is_symbolic: symbol -> bool |
6116
8ba2f25610f7
files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff
changeset
|
29 |
val is_printable: symbol -> bool |
6272 | 30 |
val length: symbol list -> int |
11010 | 31 |
val strip_blanks: string -> string |
6116
8ba2f25610f7
files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff
changeset
|
32 |
val beginning: symbol list -> string |
8ba2f25610f7
files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff
changeset
|
33 |
val scan: string list -> symbol * string list |
6640 | 34 |
val scanner: string -> (symbol list -> 'a * symbol list) -> symbol list -> 'a |
6116
8ba2f25610f7
files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff
changeset
|
35 |
val source: bool -> (string, 'a) Source.source -> |
8ba2f25610f7
files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff
changeset
|
36 |
(symbol, (string, 'a) Source.source) Source.source |
6272 | 37 |
val explode: string -> symbol list |
38 |
val input: string -> string |
|
10953 | 39 |
val default_indent: string * int -> string |
40 |
val add_mode: string -> (string -> string * real) * (string * int -> string) -> unit |
|
6692 | 41 |
val isabelle_fontN: string |
42 |
val symbolsN: string |
|
43 |
val xsymbolsN: string |
|
10923 | 44 |
val plain_output: string -> string |
6272 | 45 |
val output: string -> string |
46 |
val output_width: string -> string * real |
|
10953 | 47 |
val indent: string * int -> string |
6116
8ba2f25610f7
files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff
changeset
|
48 |
end; |
8ba2f25610f7
files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff
changeset
|
49 |
|
8ba2f25610f7
files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff
changeset
|
50 |
structure Symbol: SYMBOL = |
8ba2f25610f7
files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff
changeset
|
51 |
struct |
8ba2f25610f7
files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff
changeset
|
52 |
|
8ba2f25610f7
files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff
changeset
|
53 |
|
6272 | 54 |
(** generalized characters **) |
55 |
||
56 |
(*symbols, which are considered the smallest entities of any Isabelle |
|
57 |
string, may be of the following form: |
|
58 |
(a) ASCII symbols: a |
|
59 |
(b) printable symbols: \<ident> |
|
60 |
(c) control symbols: \<^ident> |
|
61 |
||
62 |
input may include non-ASCII characters according to isabelle-0 encoding; |
|
63 |
output is subject to the print_mode variable (default: verbatim); |
|
64 |
*) |
|
65 |
||
66 |
type symbol = string; |
|
67 |
||
68 |
val space = " "; |
|
10953 | 69 |
fun spaces k = Library.replicate_string k space; |
6857 | 70 |
val sync = "\\<^sync>"; |
10747 | 71 |
val malformed = "\\<^malformed>"; |
6272 | 72 |
val eof = ""; |
73 |
||
74 |
||
75 |
(* kinds *) |
|
76 |
||
6857 | 77 |
fun is_sync s = s = sync; |
78 |
fun not_sync s = s <> sync; |
|
79 |
||
6272 | 80 |
fun is_eof s = s = eof; |
81 |
fun not_eof s = s <> eof; |
|
82 |
val stopper = (eof, is_eof); |
|
83 |
||
84 |
fun is_ascii s = size s = 1 andalso ord s < 128; |
|
85 |
||
86 |
fun is_letter s = |
|
87 |
size s = 1 andalso |
|
88 |
(ord "A" <= ord s andalso ord s <= ord "Z" orelse |
|
89 |
ord "a" <= ord s andalso ord s <= ord "z"); |
|
90 |
||
91 |
fun is_digit s = |
|
92 |
size s = 1 andalso ord "0" <= ord s andalso ord s <= ord "9"; |
|
93 |
||
94 |
fun is_quasi_letter "_" = true |
|
95 |
| is_quasi_letter "'" = true |
|
96 |
| is_quasi_letter s = is_letter s; |
|
97 |
||
98 |
val is_blank = |
|
99 |
fn " " => true | "\t" => true | "\n" => true | "\^L" => true |
|
100 |
| "\160" => true | "\\<spacespace>" => true |
|
101 |
| _ => false; |
|
102 |
||
103 |
val is_letdig = is_quasi_letter orf is_digit; |
|
104 |
||
8230 | 105 |
fun is_symbolic s = |
106 |
size s > 2 andalso nth_elem_string (2, s) <> "^"; |
|
107 |
||
6272 | 108 |
fun is_printable s = |
109 |
size s = 1 andalso ord space <= ord s andalso ord s <= ord "~" orelse |
|
8230 | 110 |
is_symbolic s; |
111 |
||
6272 | 112 |
|
10738 | 113 |
fun sym_length ss = foldl (fn (n, s) => |
114 |
(if not (is_printable s) then 0 else |
|
115 |
(case Library.try String.substring (s, 2, 4) of |
|
116 |
Some s' => if s' = "long" orelse s' = "Long" then 2 else 1 |
|
117 |
| None => 1)) + n) (0, ss); |
|
6272 | 118 |
|
11010 | 119 |
fun strip_blanks s = |
120 |
implode (#1 (Library.take_suffix is_blank (#2 (Library.take_prefix is_blank (explode s))))); |
|
121 |
||
6272 | 122 |
|
123 |
(* beginning *) |
|
124 |
||
125 |
val smash_blanks = map (fn s => if is_blank s then space else s); |
|
126 |
||
127 |
fun beginning raw_ss = |
|
128 |
let |
|
129 |
val (all_ss, _) = take_suffix is_blank raw_ss; |
|
130 |
val dots = if length all_ss > 10 then " ..." else ""; |
|
131 |
val (ss, _) = take_suffix is_blank (take (10, all_ss)); |
|
132 |
in implode (smash_blanks ss) ^ dots end; |
|
133 |
||
134 |
||
135 |
||
136 |
(** isabelle-0 encoding table **) |
|
6116
8ba2f25610f7
files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff
changeset
|
137 |
|
8ba2f25610f7
files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff
changeset
|
138 |
val enc_start = 160; |
8ba2f25610f7
files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff
changeset
|
139 |
val enc_end = 255; |
8ba2f25610f7
files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff
changeset
|
140 |
|
8ba2f25610f7
files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff
changeset
|
141 |
val enc_vector = |
8ba2f25610f7
files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff
changeset
|
142 |
[ |
8ba2f25610f7
files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff
changeset
|
143 |
(* GENERATED TEXT FOLLOWS - Do not edit! *) |
6166 | 144 |
"\\<spacespace>", |
6116
8ba2f25610f7
files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff
changeset
|
145 |
"\\<Gamma>", |
8ba2f25610f7
files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff
changeset
|
146 |
"\\<Delta>", |
8ba2f25610f7
files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff
changeset
|
147 |
"\\<Theta>", |
8ba2f25610f7
files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff
changeset
|
148 |
"\\<Lambda>", |
8ba2f25610f7
files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff
changeset
|
149 |
"\\<Pi>", |
8ba2f25610f7
files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff
changeset
|
150 |
"\\<Sigma>", |
8ba2f25610f7
files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff
changeset
|
151 |
"\\<Phi>", |
8ba2f25610f7
files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff
changeset
|
152 |
"\\<Psi>", |
8ba2f25610f7
files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff
changeset
|
153 |
"\\<Omega>", |
8ba2f25610f7
files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff
changeset
|
154 |
"\\<alpha>", |
8ba2f25610f7
files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff
changeset
|
155 |
"\\<beta>", |
8ba2f25610f7
files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff
changeset
|
156 |
"\\<gamma>", |
8ba2f25610f7
files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff
changeset
|
157 |
"\\<delta>", |
8ba2f25610f7
files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff
changeset
|
158 |
"\\<epsilon>", |
8ba2f25610f7
files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff
changeset
|
159 |
"\\<zeta>", |
8ba2f25610f7
files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff
changeset
|
160 |
"\\<eta>", |
8ba2f25610f7
files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff
changeset
|
161 |
"\\<theta>", |
8ba2f25610f7
files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff
changeset
|
162 |
"\\<kappa>", |
8ba2f25610f7
files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff
changeset
|
163 |
"\\<lambda>", |
8ba2f25610f7
files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff
changeset
|
164 |
"\\<mu>", |
8ba2f25610f7
files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff
changeset
|
165 |
"\\<nu>", |
8ba2f25610f7
files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff
changeset
|
166 |
"\\<xi>", |
8ba2f25610f7
files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff
changeset
|
167 |
"\\<pi>", |
8ba2f25610f7
files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff
changeset
|
168 |
"\\<rho>", |
8ba2f25610f7
files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff
changeset
|
169 |
"\\<sigma>", |
8ba2f25610f7
files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff
changeset
|
170 |
"\\<tau>", |
8ba2f25610f7
files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff
changeset
|
171 |
"\\<phi>", |
8ba2f25610f7
files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff
changeset
|
172 |
"\\<chi>", |
8ba2f25610f7
files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff
changeset
|
173 |
"\\<psi>", |
8ba2f25610f7
files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff
changeset
|
174 |
"\\<omega>", |
8ba2f25610f7
files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff
changeset
|
175 |
"\\<not>", |
8ba2f25610f7
files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff
changeset
|
176 |
"\\<and>", |
8ba2f25610f7
files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff
changeset
|
177 |
"\\<or>", |
8ba2f25610f7
files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff
changeset
|
178 |
"\\<forall>", |
8ba2f25610f7
files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff
changeset
|
179 |
"\\<exists>", |
8ba2f25610f7
files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff
changeset
|
180 |
"\\<And>", |
8ba2f25610f7
files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff
changeset
|
181 |
"\\<lceil>", |
8ba2f25610f7
files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff
changeset
|
182 |
"\\<rceil>", |
8ba2f25610f7
files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff
changeset
|
183 |
"\\<lfloor>", |
8ba2f25610f7
files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff
changeset
|
184 |
"\\<rfloor>", |
8ba2f25610f7
files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff
changeset
|
185 |
"\\<turnstile>", |
8ba2f25610f7
files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff
changeset
|
186 |
"\\<Turnstile>", |
8ba2f25610f7
files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff
changeset
|
187 |
"\\<lbrakk>", |
8ba2f25610f7
files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff
changeset
|
188 |
"\\<rbrakk>", |
8ba2f25610f7
files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff
changeset
|
189 |
"\\<cdot>", |
8ba2f25610f7
files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff
changeset
|
190 |
"\\<in>", |
8ba2f25610f7
files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff
changeset
|
191 |
"\\<subseteq>", |
8ba2f25610f7
files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff
changeset
|
192 |
"\\<inter>", |
8ba2f25610f7
files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff
changeset
|
193 |
"\\<union>", |
8ba2f25610f7
files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff
changeset
|
194 |
"\\<Inter>", |
8ba2f25610f7
files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff
changeset
|
195 |
"\\<Union>", |
8ba2f25610f7
files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff
changeset
|
196 |
"\\<sqinter>", |
8ba2f25610f7
files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff
changeset
|
197 |
"\\<squnion>", |
8ba2f25610f7
files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff
changeset
|
198 |
"\\<Sqinter>", |
8ba2f25610f7
files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff
changeset
|
199 |
"\\<Squnion>", |
8ba2f25610f7
files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff
changeset
|
200 |
"\\<bottom>", |
8ba2f25610f7
files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff
changeset
|
201 |
"\\<doteq>", |
8ba2f25610f7
files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff
changeset
|
202 |
"\\<equiv>", |
8ba2f25610f7
files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff
changeset
|
203 |
"\\<noteq>", |
8ba2f25610f7
files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff
changeset
|
204 |
"\\<sqsubset>", |
8ba2f25610f7
files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff
changeset
|
205 |
"\\<sqsubseteq>", |
8ba2f25610f7
files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff
changeset
|
206 |
"\\<prec>", |
8ba2f25610f7
files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff
changeset
|
207 |
"\\<preceq>", |
8ba2f25610f7
files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff
changeset
|
208 |
"\\<succ>", |
8ba2f25610f7
files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff
changeset
|
209 |
"\\<approx>", |
8ba2f25610f7
files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff
changeset
|
210 |
"\\<sim>", |
8ba2f25610f7
files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff
changeset
|
211 |
"\\<simeq>", |
8ba2f25610f7
files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff
changeset
|
212 |
"\\<le>", |
8ba2f25610f7
files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff
changeset
|
213 |
"\\<Colon>", |
8ba2f25610f7
files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff
changeset
|
214 |
"\\<leftarrow>", |
8ba2f25610f7
files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff
changeset
|
215 |
"\\<midarrow>", |
8ba2f25610f7
files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff
changeset
|
216 |
"\\<rightarrow>", |
8ba2f25610f7
files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff
changeset
|
217 |
"\\<Leftarrow>", |
8ba2f25610f7
files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff
changeset
|
218 |
"\\<Midarrow>", |
8ba2f25610f7
files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff
changeset
|
219 |
"\\<Rightarrow>", |
9961 | 220 |
"\\<frown>", |
6116
8ba2f25610f7
files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff
changeset
|
221 |
"\\<mapsto>", |
8ba2f25610f7
files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff
changeset
|
222 |
"\\<leadsto>", |
8ba2f25610f7
files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff
changeset
|
223 |
"\\<up>", |
8ba2f25610f7
files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff
changeset
|
224 |
"\\<down>", |
8ba2f25610f7
files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff
changeset
|
225 |
"\\<notin>", |
8ba2f25610f7
files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff
changeset
|
226 |
"\\<times>", |
8ba2f25610f7
files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff
changeset
|
227 |
"\\<oplus>", |
8ba2f25610f7
files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff
changeset
|
228 |
"\\<ominus>", |
8ba2f25610f7
files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff
changeset
|
229 |
"\\<otimes>", |
8ba2f25610f7
files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff
changeset
|
230 |
"\\<oslash>", |
8ba2f25610f7
files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff
changeset
|
231 |
"\\<subset>", |
8ba2f25610f7
files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff
changeset
|
232 |
"\\<infinity>", |
8ba2f25610f7
files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff
changeset
|
233 |
"\\<box>", |
8ba2f25610f7
files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff
changeset
|
234 |
"\\<diamond>", |
8ba2f25610f7
files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff
changeset
|
235 |
"\\<circ>", |
8ba2f25610f7
files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff
changeset
|
236 |
"\\<bullet>", |
8ba2f25610f7
files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff
changeset
|
237 |
"\\<parallel>", |
8ba2f25610f7
files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff
changeset
|
238 |
"\\<surd>", |
8ba2f25610f7
files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff
changeset
|
239 |
"\\<copyright>" |
8ba2f25610f7
files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff
changeset
|
240 |
(* END OF GENERATED TEXT *) |
8ba2f25610f7
files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff
changeset
|
241 |
]; |
8ba2f25610f7
files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff
changeset
|
242 |
|
8ba2f25610f7
files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff
changeset
|
243 |
val enc_rel = enc_vector ~~ map chr (enc_start upto enc_end); |
8ba2f25610f7
files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff
changeset
|
244 |
|
8ba2f25610f7
files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff
changeset
|
245 |
val char_tab = Symtab.make enc_rel; |
8ba2f25610f7
files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff
changeset
|
246 |
val symbol_tab = Symtab.make (map swap enc_rel); |
8ba2f25610f7
files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff
changeset
|
247 |
|
8ba2f25610f7
files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff
changeset
|
248 |
fun lookup_symbol c = |
8ba2f25610f7
files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff
changeset
|
249 |
if ord c < enc_start then None |
8ba2f25610f7
files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff
changeset
|
250 |
else Symtab.lookup (symbol_tab, c); |
8ba2f25610f7
files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff
changeset
|
251 |
|
8ba2f25610f7
files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff
changeset
|
252 |
|
8ba2f25610f7
files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff
changeset
|
253 |
(* encode / decode *) |
8ba2f25610f7
files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff
changeset
|
254 |
|
8ba2f25610f7
files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff
changeset
|
255 |
fun char s = if_none (Symtab.lookup (char_tab, s)) s; |
8ba2f25610f7
files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff
changeset
|
256 |
fun symbol c = if_none (lookup_symbol c) c; |
8ba2f25610f7
files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff
changeset
|
257 |
|
8ba2f25610f7
files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff
changeset
|
258 |
fun symbol' c = |
8ba2f25610f7
files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff
changeset
|
259 |
(case lookup_symbol c of |
8ba2f25610f7
files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff
changeset
|
260 |
None => c |
8ba2f25610f7
files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff
changeset
|
261 |
| Some s => "\\" ^ s); |
8ba2f25610f7
files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff
changeset
|
262 |
|
8ba2f25610f7
files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff
changeset
|
263 |
|
8ba2f25610f7
files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff
changeset
|
264 |
|
8998 | 265 |
(** scanning through symbols **) |
6640 | 266 |
|
267 |
fun scanner msg scan chs = |
|
268 |
let |
|
269 |
fun err_msg cs = msg ^ ": " ^ beginning cs; |
|
270 |
val fin_scan = Scan.error (Scan.finite stopper (!! (fn (cs, _) => err_msg cs) scan)); |
|
271 |
in |
|
272 |
(case fin_scan chs of |
|
273 |
(result, []) => result |
|
274 |
| (_, rest) => error (err_msg rest)) |
|
275 |
end; |
|
276 |
||
277 |
||
278 |
||
6272 | 279 |
(** symbol input **) |
6116
8ba2f25610f7
files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff
changeset
|
280 |
|
8ba2f25610f7
files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff
changeset
|
281 |
(* scan *) |
8ba2f25610f7
files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff
changeset
|
282 |
|
8ba2f25610f7
files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff
changeset
|
283 |
val scan_id = Scan.one is_letter ^^ (Scan.any is_letdig >> implode); |
8ba2f25610f7
files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff
changeset
|
284 |
|
8ba2f25610f7
files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff
changeset
|
285 |
val scan = |
8ba2f25610f7
files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff
changeset
|
286 |
($$ "\\" --| Scan.optional ($$ "\\") "") ^^ $$ "<" ^^ |
8ba2f25610f7
files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff
changeset
|
287 |
!! (fn (cs, _) => "Malformed symbolic character specification: \\" ^ "<" ^ beginning cs) |
8ba2f25610f7
files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff
changeset
|
288 |
(Scan.optional ($$ "^") "" ^^ scan_id ^^ $$ ">") || |
8ba2f25610f7
files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff
changeset
|
289 |
Scan.one not_eof; |
8ba2f25610f7
files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff
changeset
|
290 |
|
8ba2f25610f7
files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff
changeset
|
291 |
|
8ba2f25610f7
files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff
changeset
|
292 |
(* source *) |
8ba2f25610f7
files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff
changeset
|
293 |
|
10747 | 294 |
val recover = Scan.any ((not o is_blank) andf not_eof) >> K [malformed]; |
6116
8ba2f25610f7
files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff
changeset
|
295 |
|
8ba2f25610f7
files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff
changeset
|
296 |
fun source do_recover src = |
8ba2f25610f7
files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff
changeset
|
297 |
Source.source stopper (Scan.bulk scan) (if do_recover then Some recover else None) src; |
8ba2f25610f7
files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff
changeset
|
298 |
|
8ba2f25610f7
files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff
changeset
|
299 |
|
8ba2f25610f7
files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff
changeset
|
300 |
(* explode *) |
8ba2f25610f7
files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff
changeset
|
301 |
|
8ba2f25610f7
files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff
changeset
|
302 |
fun no_syms [] = true |
8ba2f25610f7
files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff
changeset
|
303 |
| no_syms ("\\" :: "<" :: _) = false |
8ba2f25610f7
files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff
changeset
|
304 |
| no_syms (c :: cs) = ord c < enc_start andalso no_syms cs; |
8ba2f25610f7
files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff
changeset
|
305 |
|
8ba2f25610f7
files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff
changeset
|
306 |
fun sym_explode str = |
8ba2f25610f7
files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff
changeset
|
307 |
let val chs = explode str in |
8ba2f25610f7
files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff
changeset
|
308 |
if no_syms chs then chs (*tune trivial case*) |
8ba2f25610f7
files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff
changeset
|
309 |
else map symbol (the (Scan.read stopper (Scan.repeat scan) chs)) |
8ba2f25610f7
files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff
changeset
|
310 |
end; |
8ba2f25610f7
files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff
changeset
|
311 |
|
8ba2f25610f7
files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff
changeset
|
312 |
|
6272 | 313 |
(* input *) |
6116
8ba2f25610f7
files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff
changeset
|
314 |
|
8ba2f25610f7
files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff
changeset
|
315 |
fun input str = |
8ba2f25610f7
files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff
changeset
|
316 |
let val chs = explode str in |
8ba2f25610f7
files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff
changeset
|
317 |
if forall (fn c => ord c < enc_start) chs then str |
8ba2f25610f7
files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff
changeset
|
318 |
else implode (map symbol' chs) |
8ba2f25610f7
files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff
changeset
|
319 |
end; |
8ba2f25610f7
files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff
changeset
|
320 |
|
8ba2f25610f7
files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff
changeset
|
321 |
|
6272 | 322 |
|
323 |
(** symbol output **) |
|
324 |
||
10953 | 325 |
(* default *) |
6272 | 326 |
|
327 |
fun string_size s = (s, real (size s)); |
|
328 |
||
329 |
fun default_output s = |
|
6320 | 330 |
if not (exists_string (equal "\\") s) then string_size s |
10738 | 331 |
else string_size (implode (map (fn "\\" => "\\\\" | c => c) (explode s))); (*sic!*) |
6272 | 332 |
|
10953 | 333 |
fun default_indent (_: string, k) = spaces k; |
6272 | 334 |
|
10953 | 335 |
|
336 |
(* isabelle_font *) |
|
6272 | 337 |
|
338 |
fun isabelle_font_output s = |
|
339 |
let val cs = sym_explode s |
|
340 |
in (implode (map char cs), real (sym_length cs)) end; |
|
341 |
||
10953 | 342 |
val isabelle_font_indent = default_indent; |
343 |
||
6272 | 344 |
|
345 |
(* maintain modes *) |
|
346 |
||
6692 | 347 |
val isabelle_fontN = "isabelle_font"; |
348 |
val symbolsN = "symbols"; |
|
349 |
val xsymbolsN = "xsymbols"; |
|
350 |
||
10953 | 351 |
val modes = ref (Symtab.make [(isabelle_fontN, (isabelle_font_output, isabelle_font_indent))]); |
6272 | 352 |
|
353 |
fun lookup_mode name = Symtab.lookup (! modes, name); |
|
354 |
||
10953 | 355 |
fun add_mode name m = |
6272 | 356 |
(if is_none (lookup_mode name) then () |
6320 | 357 |
else warning ("Redeclaration of symbol print mode " ^ quote name); |
10953 | 358 |
modes := Symtab.update ((name, m), ! modes)); |
359 |
||
360 |
fun get_mode () = |
|
361 |
if_none (get_first lookup_mode (! print_mode)) (default_output, default_indent); |
|
6272 | 362 |
|
363 |
||
364 |
(* mode output *) |
|
365 |
||
10953 | 366 |
fun output_width x = #1 (get_mode ()) x; |
6272 | 367 |
val output = #1 o output_width; |
10923 | 368 |
val plain_output = #1 o default_output; |
6272 | 369 |
|
10953 | 370 |
fun indent x = #2 (get_mode ()) x; |
371 |
||
6272 | 372 |
|
6116
8ba2f25610f7
files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff
changeset
|
373 |
(*final declarations of this structure!*) |
6272 | 374 |
val length = sym_length; |
6116
8ba2f25610f7
files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff
changeset
|
375 |
val explode = sym_explode; |
6272 | 376 |
|
6116
8ba2f25610f7
files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff
changeset
|
377 |
|
8ba2f25610f7
files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff
changeset
|
378 |
end; |