author | berghofe |
Wed, 27 Nov 2002 17:20:49 +0100 | |
changeset 13730 | 09aeb7346d3f |
parent 13559 | 51c3ac47d127 |
child 14171 | 0cab06e3bbd0 |
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 |
|
12116 | 6 |
Generalized characters with infinitely many named symbols. |
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 |
12904 | 25 |
val is_quasi: symbol -> bool |
6116
8ba2f25610f7
files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff
changeset
|
26 |
val is_quasi_letter: symbol -> bool |
8ba2f25610f7
files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff
changeset
|
27 |
val is_letdig: symbol -> bool |
8ba2f25610f7
files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff
changeset
|
28 |
val is_blank: symbol -> bool |
13559
51c3ac47d127
added checking so that (rename_tac "x y") is rejected, since
paulson
parents:
12904
diff
changeset
|
29 |
val is_identifier: symbol -> bool |
8230 | 30 |
val is_symbolic: symbol -> bool |
6116
8ba2f25610f7
files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff
changeset
|
31 |
val is_printable: symbol -> bool |
6272 | 32 |
val length: symbol list -> int |
11010 | 33 |
val strip_blanks: string -> string |
6116
8ba2f25610f7
files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff
changeset
|
34 |
val beginning: symbol list -> string |
13730 | 35 |
val scan_id: string list -> string * string list |
6116
8ba2f25610f7
files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff
changeset
|
36 |
val scan: string list -> symbol * string list |
6640 | 37 |
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
|
38 |
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
|
39 |
(symbol, (string, 'a) Source.source) Source.source |
6272 | 40 |
val explode: string -> symbol list |
12904 | 41 |
val bump_string: string -> string |
10953 | 42 |
val default_indent: string * int -> string |
43 |
val add_mode: string -> (string -> string * real) * (string * int -> string) -> unit |
|
6692 | 44 |
val symbolsN: string |
45 |
val xsymbolsN: string |
|
10923 | 46 |
val plain_output: string -> string |
6272 | 47 |
val output: string -> string |
48 |
val output_width: string -> string * real |
|
10953 | 49 |
val indent: string * int -> string |
6116
8ba2f25610f7
files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff
changeset
|
50 |
end; |
8ba2f25610f7
files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff
changeset
|
51 |
|
8ba2f25610f7
files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff
changeset
|
52 |
structure Symbol: SYMBOL = |
8ba2f25610f7
files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff
changeset
|
53 |
struct |
8ba2f25610f7
files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff
changeset
|
54 |
|
8ba2f25610f7
files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff
changeset
|
55 |
|
6272 | 56 |
(** generalized characters **) |
57 |
||
58 |
(*symbols, which are considered the smallest entities of any Isabelle |
|
59 |
string, may be of the following form: |
|
60 |
(a) ASCII symbols: a |
|
61 |
(b) printable symbols: \<ident> |
|
62 |
(c) control symbols: \<^ident> |
|
63 |
||
12116 | 64 |
output is subject to the print_mode variable (default: verbatim), |
65 |
actual interpretation in display is up to front-end tools; |
|
6272 | 66 |
*) |
67 |
||
68 |
type symbol = string; |
|
69 |
||
70 |
val space = " "; |
|
10953 | 71 |
fun spaces k = Library.replicate_string k space; |
6857 | 72 |
val sync = "\\<^sync>"; |
10747 | 73 |
val malformed = "\\<^malformed>"; |
6272 | 74 |
val eof = ""; |
75 |
||
76 |
||
77 |
(* kinds *) |
|
78 |
||
6857 | 79 |
fun is_sync s = s = sync; |
80 |
fun not_sync s = s <> sync; |
|
81 |
||
6272 | 82 |
fun is_eof s = s = eof; |
83 |
fun not_eof s = s <> eof; |
|
84 |
val stopper = (eof, is_eof); |
|
85 |
||
86 |
fun is_ascii s = size s = 1 andalso ord s < 128; |
|
87 |
||
88 |
fun is_letter s = |
|
89 |
size s = 1 andalso |
|
90 |
(ord "A" <= ord s andalso ord s <= ord "Z" orelse |
|
91 |
ord "a" <= ord s andalso ord s <= ord "z"); |
|
92 |
||
93 |
fun is_digit s = |
|
94 |
size s = 1 andalso ord "0" <= ord s andalso ord s <= ord "9"; |
|
95 |
||
12904 | 96 |
fun is_quasi "_" = true |
97 |
| is_quasi "'" = true |
|
98 |
| is_quasi _ = false; |
|
99 |
||
100 |
fun is_quasi_letter s = is_quasi s orelse is_letter s; |
|
6272 | 101 |
|
102 |
val is_blank = |
|
103 |
fn " " => true | "\t" => true | "\n" => true | "\^L" => true |
|
104 |
| "\160" => true | "\\<spacespace>" => true |
|
105 |
| _ => false; |
|
106 |
||
12904 | 107 |
fun is_letdig s = is_quasi_letter s orelse is_digit s; |
6272 | 108 |
|
8230 | 109 |
fun is_symbolic s = |
110 |
size s > 2 andalso nth_elem_string (2, s) <> "^"; |
|
111 |
||
6272 | 112 |
fun is_printable s = |
113 |
size s = 1 andalso ord space <= ord s andalso ord s <= ord "~" orelse |
|
8230 | 114 |
is_symbolic s; |
115 |
||
13559
51c3ac47d127
added checking so that (rename_tac "x y") is rejected, since
paulson
parents:
12904
diff
changeset
|
116 |
fun is_identifier s = |
51c3ac47d127
added checking so that (rename_tac "x y") is rejected, since
paulson
parents:
12904
diff
changeset
|
117 |
case (explode s) of |
51c3ac47d127
added checking so that (rename_tac "x y") is rejected, since
paulson
parents:
12904
diff
changeset
|
118 |
[] => false |
51c3ac47d127
added checking so that (rename_tac "x y") is rejected, since
paulson
parents:
12904
diff
changeset
|
119 |
| c::cs => is_letter c andalso forall is_letdig cs; |
6272 | 120 |
|
10738 | 121 |
fun sym_length ss = foldl (fn (n, s) => |
122 |
(if not (is_printable s) then 0 else |
|
123 |
(case Library.try String.substring (s, 2, 4) of |
|
124 |
Some s' => if s' = "long" orelse s' = "Long" then 2 else 1 |
|
125 |
| None => 1)) + n) (0, ss); |
|
6272 | 126 |
|
11010 | 127 |
fun strip_blanks s = |
128 |
implode (#1 (Library.take_suffix is_blank (#2 (Library.take_prefix is_blank (explode s))))); |
|
129 |
||
6272 | 130 |
|
131 |
(* beginning *) |
|
132 |
||
133 |
val smash_blanks = map (fn s => if is_blank s then space else s); |
|
134 |
||
135 |
fun beginning raw_ss = |
|
136 |
let |
|
137 |
val (all_ss, _) = take_suffix is_blank raw_ss; |
|
138 |
val dots = if length all_ss > 10 then " ..." else ""; |
|
139 |
val (ss, _) = take_suffix is_blank (take (10, all_ss)); |
|
140 |
in implode (smash_blanks ss) ^ dots end; |
|
141 |
||
142 |
||
143 |
||
8998 | 144 |
(** scanning through symbols **) |
6640 | 145 |
|
146 |
fun scanner msg scan chs = |
|
147 |
let |
|
148 |
fun err_msg cs = msg ^ ": " ^ beginning cs; |
|
149 |
val fin_scan = Scan.error (Scan.finite stopper (!! (fn (cs, _) => err_msg cs) scan)); |
|
150 |
in |
|
151 |
(case fin_scan chs of |
|
152 |
(result, []) => result |
|
153 |
| (_, rest) => error (err_msg rest)) |
|
154 |
end; |
|
155 |
||
156 |
||
157 |
||
6272 | 158 |
(** symbol input **) |
6116
8ba2f25610f7
files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff
changeset
|
159 |
|
8ba2f25610f7
files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff
changeset
|
160 |
(* scan *) |
8ba2f25610f7
files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff
changeset
|
161 |
|
8ba2f25610f7
files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff
changeset
|
162 |
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
|
163 |
|
8ba2f25610f7
files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff
changeset
|
164 |
val scan = |
8ba2f25610f7
files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff
changeset
|
165 |
($$ "\\" --| Scan.optional ($$ "\\") "") ^^ $$ "<" ^^ |
8ba2f25610f7
files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff
changeset
|
166 |
!! (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
|
167 |
(Scan.optional ($$ "^") "" ^^ scan_id ^^ $$ ">") || |
8ba2f25610f7
files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff
changeset
|
168 |
Scan.one not_eof; |
8ba2f25610f7
files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff
changeset
|
169 |
|
8ba2f25610f7
files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff
changeset
|
170 |
|
8ba2f25610f7
files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff
changeset
|
171 |
(* source *) |
8ba2f25610f7
files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff
changeset
|
172 |
|
10747 | 173 |
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
|
174 |
|
8ba2f25610f7
files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff
changeset
|
175 |
fun source do_recover src = |
8ba2f25610f7
files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff
changeset
|
176 |
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
|
177 |
|
8ba2f25610f7
files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff
changeset
|
178 |
|
8ba2f25610f7
files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff
changeset
|
179 |
(* explode *) |
8ba2f25610f7
files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff
changeset
|
180 |
|
8ba2f25610f7
files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff
changeset
|
181 |
fun no_syms [] = true |
8ba2f25610f7
files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff
changeset
|
182 |
| no_syms ("\\" :: "<" :: _) = false |
12116 | 183 |
| no_syms (_ :: cs) = no_syms cs; |
6116
8ba2f25610f7
files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff
changeset
|
184 |
|
8ba2f25610f7
files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff
changeset
|
185 |
fun sym_explode str = |
8ba2f25610f7
files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff
changeset
|
186 |
let val chs = explode str in |
8ba2f25610f7
files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff
changeset
|
187 |
if no_syms chs then chs (*tune trivial case*) |
12116 | 188 |
else the (Scan.read stopper (Scan.repeat scan) chs) |
6116
8ba2f25610f7
files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff
changeset
|
189 |
end; |
8ba2f25610f7
files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff
changeset
|
190 |
|
8ba2f25610f7
files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff
changeset
|
191 |
|
12904 | 192 |
(* bump_string -- increment suffix of lowercase letters like a base 26 number *) |
193 |
||
194 |
fun bump_string str = |
|
195 |
let |
|
196 |
fun bump [] = ["a"] |
|
197 |
| bump ("z" :: ss) = "a" :: bump ss |
|
198 |
| bump (s :: ss) = |
|
199 |
if size s = 1 andalso ord "a" <= ord s andalso ord s < ord "z" |
|
200 |
then chr (ord s + 1) :: ss |
|
201 |
else "a" :: s :: ss; |
|
202 |
val (cs, qs) = Library.take_suffix is_quasi (sym_explode str); |
|
203 |
in implode (rev (bump (rev cs)) @ qs) end; |
|
204 |
||
6272 | 205 |
|
206 |
(** symbol output **) |
|
207 |
||
10953 | 208 |
(* default *) |
6272 | 209 |
|
210 |
fun string_size s = (s, real (size s)); |
|
211 |
||
13730 | 212 |
val escape = Scan.repeat |
213 |
((($$ "\\" >> K "\\\\") ^^ Scan.optional ($$ "\\" >> K "\\\\") "" ^^ $$ "<" ^^ |
|
214 |
Scan.optional ($$ "^") "" ^^ scan_id ^^ $$ ">") || |
|
215 |
Scan.one not_eof) >> implode; |
|
216 |
||
6272 | 217 |
fun default_output s = |
6320 | 218 |
if not (exists_string (equal "\\") s) then string_size s |
13730 | 219 |
else string_size (fst (Scan.finite stopper escape (explode s))); |
6272 | 220 |
|
10953 | 221 |
fun default_indent (_: string, k) = spaces k; |
6272 | 222 |
|
10953 | 223 |
|
6272 | 224 |
(* maintain modes *) |
225 |
||
6692 | 226 |
val symbolsN = "symbols"; |
227 |
val xsymbolsN = "xsymbols"; |
|
228 |
||
12116 | 229 |
val modes = |
230 |
ref (Symtab.empty: ((string -> string * real) * (string * int -> string)) Symtab.table); |
|
6272 | 231 |
|
232 |
fun lookup_mode name = Symtab.lookup (! modes, name); |
|
233 |
||
10953 | 234 |
fun add_mode name m = |
6272 | 235 |
(if is_none (lookup_mode name) then () |
6320 | 236 |
else warning ("Redeclaration of symbol print mode " ^ quote name); |
10953 | 237 |
modes := Symtab.update ((name, m), ! modes)); |
238 |
||
239 |
fun get_mode () = |
|
240 |
if_none (get_first lookup_mode (! print_mode)) (default_output, default_indent); |
|
6272 | 241 |
|
242 |
||
243 |
(* mode output *) |
|
244 |
||
10953 | 245 |
fun output_width x = #1 (get_mode ()) x; |
6272 | 246 |
val output = #1 o output_width; |
10923 | 247 |
val plain_output = #1 o default_output; |
6272 | 248 |
|
10953 | 249 |
fun indent x = #2 (get_mode ()) x; |
250 |
||
6272 | 251 |
|
6116
8ba2f25610f7
files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff
changeset
|
252 |
(*final declarations of this structure!*) |
6272 | 253 |
val length = sym_length; |
6116
8ba2f25610f7
files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff
changeset
|
254 |
val explode = sym_explode; |
6272 | 255 |
|
6116
8ba2f25610f7
files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff
changeset
|
256 |
|
8ba2f25610f7
files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff
changeset
|
257 |
end; |