author | schirmer |
Tue, 13 Apr 2004 23:08:12 +0200 | |
changeset 14557 | 31ae4a47267c |
parent 14361 | ad2f5da643b4 |
child 14559 | 7612d19d5638 |
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> |
|
14557
31ae4a47267c
* cleaner distinction between control symbols "\<^...>" and "\<^raw...>" in
schirmer
parents:
14361
diff
changeset
|
62 |
(c) control symbols: \<^ident> |
31ae4a47267c
* cleaner distinction between control symbols "\<^...>" and "\<^raw...>" in
schirmer
parents:
14361
diff
changeset
|
63 |
(d) raw control symbols: \<^raw...>, where "..." may be any printable |
31ae4a47267c
* cleaner distinction between control symbols "\<^...>" and "\<^raw...>" in
schirmer
parents:
14361
diff
changeset
|
64 |
character excluding ">" |
6272 | 65 |
|
12116 | 66 |
output is subject to the print_mode variable (default: verbatim), |
67 |
actual interpretation in display is up to front-end tools; |
|
6272 | 68 |
*) |
69 |
||
70 |
type symbol = string; |
|
71 |
||
72 |
val space = " "; |
|
10953 | 73 |
fun spaces k = Library.replicate_string k space; |
6857 | 74 |
val sync = "\\<^sync>"; |
10747 | 75 |
val malformed = "\\<^malformed>"; |
6272 | 76 |
val eof = ""; |
77 |
||
78 |
||
79 |
(* kinds *) |
|
80 |
||
6857 | 81 |
fun is_sync s = s = sync; |
82 |
fun not_sync s = s <> sync; |
|
83 |
||
6272 | 84 |
fun is_eof s = s = eof; |
85 |
fun not_eof s = s <> eof; |
|
86 |
val stopper = (eof, is_eof); |
|
87 |
||
88 |
fun is_ascii s = size s = 1 andalso ord s < 128; |
|
89 |
||
14171
0cab06e3bbd0
Extended the notion of letter and digit, such that now one may use greek,
skalberg
parents:
13730
diff
changeset
|
90 |
local |
0cab06e3bbd0
Extended the notion of letter and digit, such that now one may use greek,
skalberg
parents:
13730
diff
changeset
|
91 |
fun wrap s = "\\<" ^ s ^ ">" |
0cab06e3bbd0
Extended the notion of letter and digit, such that now one may use greek,
skalberg
parents:
13730
diff
changeset
|
92 |
|
0cab06e3bbd0
Extended the notion of letter and digit, such that now one may use greek,
skalberg
parents:
13730
diff
changeset
|
93 |
val cal_letters = |
0cab06e3bbd0
Extended the notion of letter and digit, such that now one may use greek,
skalberg
parents:
13730
diff
changeset
|
94 |
["A","B","C","D","E","F","G","H","I","J","K","L","M", |
0cab06e3bbd0
Extended the notion of letter and digit, such that now one may use greek,
skalberg
parents:
13730
diff
changeset
|
95 |
"N","O","P","Q","R","S","T","U","V","W","X","Y","Z"] |
0cab06e3bbd0
Extended the notion of letter and digit, such that now one may use greek,
skalberg
parents:
13730
diff
changeset
|
96 |
|
0cab06e3bbd0
Extended the notion of letter and digit, such that now one may use greek,
skalberg
parents:
13730
diff
changeset
|
97 |
val small_letters = |
0cab06e3bbd0
Extended the notion of letter and digit, such that now one may use greek,
skalberg
parents:
13730
diff
changeset
|
98 |
["a","b","c","d","e","f","g","h","i","j","k","l","m", |
0cab06e3bbd0
Extended the notion of letter and digit, such that now one may use greek,
skalberg
parents:
13730
diff
changeset
|
99 |
"n","o","p","q","r","s","t","u","v","w","x","y","z"] |
0cab06e3bbd0
Extended the notion of letter and digit, such that now one may use greek,
skalberg
parents:
13730
diff
changeset
|
100 |
|
0cab06e3bbd0
Extended the notion of letter and digit, such that now one may use greek,
skalberg
parents:
13730
diff
changeset
|
101 |
val goth_letters = |
0cab06e3bbd0
Extended the notion of letter and digit, such that now one may use greek,
skalberg
parents:
13730
diff
changeset
|
102 |
["AA","BB","CC","DD","EE","FF","GG","HH","II","JJ","KK","LL","MM", |
0cab06e3bbd0
Extended the notion of letter and digit, such that now one may use greek,
skalberg
parents:
13730
diff
changeset
|
103 |
"NN","OO","PP","QQ","RR","SS","TT","UU","VV","WW","XX","YY","ZZ", |
0cab06e3bbd0
Extended the notion of letter and digit, such that now one may use greek,
skalberg
parents:
13730
diff
changeset
|
104 |
"aa","bb","cc","dd","ee","ff","gg","hh","ii","jj","kk","ll","mm", |
0cab06e3bbd0
Extended the notion of letter and digit, such that now one may use greek,
skalberg
parents:
13730
diff
changeset
|
105 |
"nn","oo","pp","qq","rr","ss","tt","uu","vv","ww","xx","yy","zz"] |
0cab06e3bbd0
Extended the notion of letter and digit, such that now one may use greek,
skalberg
parents:
13730
diff
changeset
|
106 |
|
0cab06e3bbd0
Extended the notion of letter and digit, such that now one may use greek,
skalberg
parents:
13730
diff
changeset
|
107 |
val greek_letters = |
0cab06e3bbd0
Extended the notion of letter and digit, such that now one may use greek,
skalberg
parents:
13730
diff
changeset
|
108 |
["alpha","beta","gamma","delta","epsilon","zeta","eta","theta", |
0cab06e3bbd0
Extended the notion of letter and digit, such that now one may use greek,
skalberg
parents:
13730
diff
changeset
|
109 |
"iota","kappa",(*"lambda",*)"mu","nu","xi","pi","rho","sigma","tau", |
0cab06e3bbd0
Extended the notion of letter and digit, such that now one may use greek,
skalberg
parents:
13730
diff
changeset
|
110 |
"upsilon","phi","psi","omega","Gamma","Delta","Theta","Lambda", |
0cab06e3bbd0
Extended the notion of letter and digit, such that now one may use greek,
skalberg
parents:
13730
diff
changeset
|
111 |
"Xi","Pi","Sigma","Upsilon","Phi","Psi","Omega"] |
0cab06e3bbd0
Extended the notion of letter and digit, such that now one may use greek,
skalberg
parents:
13730
diff
changeset
|
112 |
|
0cab06e3bbd0
Extended the notion of letter and digit, such that now one may use greek,
skalberg
parents:
13730
diff
changeset
|
113 |
val bbb_letters = ["bool","complex","nat","rat","real","int"] |
0cab06e3bbd0
Extended the notion of letter and digit, such that now one may use greek,
skalberg
parents:
13730
diff
changeset
|
114 |
|
14234
9590df3c5f2a
use \<^isub> and \<^isup> in identifiers instead of just \<^sub> (avoid
kleing
parents:
14232
diff
changeset
|
115 |
val control_letters = ["^isub", "^isup"] |
14232 | 116 |
|
14171
0cab06e3bbd0
Extended the notion of letter and digit, such that now one may use greek,
skalberg
parents:
13730
diff
changeset
|
117 |
val pre_letters = |
0cab06e3bbd0
Extended the notion of letter and digit, such that now one may use greek,
skalberg
parents:
13730
diff
changeset
|
118 |
cal_letters @ |
0cab06e3bbd0
Extended the notion of letter and digit, such that now one may use greek,
skalberg
parents:
13730
diff
changeset
|
119 |
small_letters @ |
0cab06e3bbd0
Extended the notion of letter and digit, such that now one may use greek,
skalberg
parents:
13730
diff
changeset
|
120 |
goth_letters @ |
14232 | 121 |
greek_letters @ |
122 |
control_letters |
|
123 |
||
14171
0cab06e3bbd0
Extended the notion of letter and digit, such that now one may use greek,
skalberg
parents:
13730
diff
changeset
|
124 |
in |
14232 | 125 |
val ext_letters = map wrap pre_letters |
14173 | 126 |
|
14171
0cab06e3bbd0
Extended the notion of letter and digit, such that now one may use greek,
skalberg
parents:
13730
diff
changeset
|
127 |
fun is_ext_letter s = String.isPrefix "\\<" s andalso s mem ext_letters |
0cab06e3bbd0
Extended the notion of letter and digit, such that now one may use greek,
skalberg
parents:
13730
diff
changeset
|
128 |
end |
0cab06e3bbd0
Extended the notion of letter and digit, such that now one may use greek,
skalberg
parents:
13730
diff
changeset
|
129 |
|
6272 | 130 |
fun is_letter s = |
14171
0cab06e3bbd0
Extended the notion of letter and digit, such that now one may use greek,
skalberg
parents:
13730
diff
changeset
|
131 |
(size s = 1 andalso |
0cab06e3bbd0
Extended the notion of letter and digit, such that now one may use greek,
skalberg
parents:
13730
diff
changeset
|
132 |
(ord "A" <= ord s andalso ord s <= ord "Z" orelse |
0cab06e3bbd0
Extended the notion of letter and digit, such that now one may use greek,
skalberg
parents:
13730
diff
changeset
|
133 |
ord "a" <= ord s andalso ord s <= ord "z")) |
0cab06e3bbd0
Extended the notion of letter and digit, such that now one may use greek,
skalberg
parents:
13730
diff
changeset
|
134 |
orelse is_ext_letter s |
6272 | 135 |
|
136 |
fun is_digit s = |
|
14173 | 137 |
size s = 1 andalso ord "0" <= ord s andalso ord s <= ord "9" |
6272 | 138 |
|
12904 | 139 |
fun is_quasi "_" = true |
140 |
| is_quasi "'" = true |
|
141 |
| is_quasi _ = false; |
|
142 |
||
143 |
fun is_quasi_letter s = is_quasi s orelse is_letter s; |
|
6272 | 144 |
|
145 |
val is_blank = |
|
14221 | 146 |
fn " " => true | "\t" => true | "\r" => true | "\n" => true | "\^L" => true |
6272 | 147 |
| "\160" => true | "\\<spacespace>" => true |
148 |
| _ => false; |
|
149 |
||
12904 | 150 |
fun is_letdig s = is_quasi_letter s orelse is_digit s; |
6272 | 151 |
|
8230 | 152 |
fun is_symbolic s = |
14171
0cab06e3bbd0
Extended the notion of letter and digit, such that now one may use greek,
skalberg
parents:
13730
diff
changeset
|
153 |
size s > 2 andalso nth_elem_string (2, s) <> "^" |
14173 | 154 |
andalso not (is_ext_letter s); |
8230 | 155 |
|
6272 | 156 |
fun is_printable s = |
157 |
size s = 1 andalso ord space <= ord s andalso ord s <= ord "~" orelse |
|
14173 | 158 |
is_ext_letter s orelse |
8230 | 159 |
is_symbolic s; |
160 |
||
14361
ad2f5da643b4
* Support for raw latex output in control symbols: \<^raw...>
schirmer
parents:
14234
diff
changeset
|
161 |
fun is_ctrl_letter s = |
ad2f5da643b4
* Support for raw latex output in control symbols: \<^raw...>
schirmer
parents:
14234
diff
changeset
|
162 |
size s = 1 andalso ord space <= ord s andalso ord s <= ord "~" andalso s <> ">"; |
ad2f5da643b4
* Support for raw latex output in control symbols: \<^raw...>
schirmer
parents:
14234
diff
changeset
|
163 |
|
13559
51c3ac47d127
added checking so that (rename_tac "x y") is rejected, since
paulson
parents:
12904
diff
changeset
|
164 |
fun is_identifier s = |
51c3ac47d127
added checking so that (rename_tac "x y") is rejected, since
paulson
parents:
12904
diff
changeset
|
165 |
case (explode s) of |
51c3ac47d127
added checking so that (rename_tac "x y") is rejected, since
paulson
parents:
12904
diff
changeset
|
166 |
[] => false |
51c3ac47d127
added checking so that (rename_tac "x y") is rejected, since
paulson
parents:
12904
diff
changeset
|
167 |
| c::cs => is_letter c andalso forall is_letdig cs; |
6272 | 168 |
|
10738 | 169 |
fun sym_length ss = foldl (fn (n, s) => |
170 |
(if not (is_printable s) then 0 else |
|
171 |
(case Library.try String.substring (s, 2, 4) of |
|
172 |
Some s' => if s' = "long" orelse s' = "Long" then 2 else 1 |
|
173 |
| None => 1)) + n) (0, ss); |
|
6272 | 174 |
|
11010 | 175 |
fun strip_blanks s = |
176 |
implode (#1 (Library.take_suffix is_blank (#2 (Library.take_prefix is_blank (explode s))))); |
|
177 |
||
6272 | 178 |
|
179 |
(* beginning *) |
|
180 |
||
181 |
val smash_blanks = map (fn s => if is_blank s then space else s); |
|
182 |
||
183 |
fun beginning raw_ss = |
|
184 |
let |
|
185 |
val (all_ss, _) = take_suffix is_blank raw_ss; |
|
186 |
val dots = if length all_ss > 10 then " ..." else ""; |
|
187 |
val (ss, _) = take_suffix is_blank (take (10, all_ss)); |
|
188 |
in implode (smash_blanks ss) ^ dots end; |
|
189 |
||
190 |
||
191 |
||
8998 | 192 |
(** scanning through symbols **) |
6640 | 193 |
|
194 |
fun scanner msg scan chs = |
|
195 |
let |
|
196 |
fun err_msg cs = msg ^ ": " ^ beginning cs; |
|
197 |
val fin_scan = Scan.error (Scan.finite stopper (!! (fn (cs, _) => err_msg cs) scan)); |
|
198 |
in |
|
199 |
(case fin_scan chs of |
|
200 |
(result, []) => result |
|
201 |
| (_, rest) => error (err_msg rest)) |
|
202 |
end; |
|
203 |
||
204 |
||
205 |
||
6272 | 206 |
(** symbol input **) |
6116
8ba2f25610f7
files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff
changeset
|
207 |
|
8ba2f25610f7
files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff
changeset
|
208 |
(* scan *) |
8ba2f25610f7
files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff
changeset
|
209 |
|
8ba2f25610f7
files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff
changeset
|
210 |
val scan_id = Scan.one is_letter ^^ (Scan.any is_letdig >> implode); |
14361
ad2f5da643b4
* Support for raw latex output in control symbols: \<^raw...>
schirmer
parents:
14234
diff
changeset
|
211 |
val scan_ctrlid = Scan.one is_letter ^^ (Scan.any is_ctrl_letter >> implode); |
14557
31ae4a47267c
* cleaner distinction between control symbols "\<^...>" and "\<^raw...>" in
schirmer
parents:
14361
diff
changeset
|
212 |
val scan_rawctrlid = $$ "r" ^^ $$ "a" ^^ $$ "w" ^^ scan_ctrlid; |
6116
8ba2f25610f7
files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff
changeset
|
213 |
|
8ba2f25610f7
files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff
changeset
|
214 |
val scan = |
14361
ad2f5da643b4
* Support for raw latex output in control symbols: \<^raw...>
schirmer
parents:
14234
diff
changeset
|
215 |
$$ "\\" ^^ $$ "<" ^^ |
6116
8ba2f25610f7
files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff
changeset
|
216 |
!! (fn (cs, _) => "Malformed symbolic character specification: \\" ^ "<" ^ beginning cs) |
14557
31ae4a47267c
* cleaner distinction between control symbols "\<^...>" and "\<^raw...>" in
schirmer
parents:
14361
diff
changeset
|
217 |
((($$ "^" ^^ (scan_rawctrlid || scan_id)) || scan_id) ^^ $$ ">") || |
6116
8ba2f25610f7
files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff
changeset
|
218 |
Scan.one not_eof; |
8ba2f25610f7
files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff
changeset
|
219 |
|
8ba2f25610f7
files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff
changeset
|
220 |
(* source *) |
8ba2f25610f7
files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff
changeset
|
221 |
|
10747 | 222 |
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
|
223 |
|
8ba2f25610f7
files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff
changeset
|
224 |
fun source do_recover src = |
8ba2f25610f7
files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff
changeset
|
225 |
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
|
226 |
|
8ba2f25610f7
files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff
changeset
|
227 |
|
8ba2f25610f7
files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff
changeset
|
228 |
(* explode *) |
8ba2f25610f7
files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff
changeset
|
229 |
|
8ba2f25610f7
files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff
changeset
|
230 |
fun no_syms [] = true |
8ba2f25610f7
files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff
changeset
|
231 |
| no_syms ("\\" :: "<" :: _) = false |
12116 | 232 |
| 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
|
233 |
|
8ba2f25610f7
files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff
changeset
|
234 |
fun sym_explode str = |
8ba2f25610f7
files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff
changeset
|
235 |
let val chs = explode str in |
8ba2f25610f7
files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff
changeset
|
236 |
if no_syms chs then chs (*tune trivial case*) |
12116 | 237 |
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
|
238 |
end; |
8ba2f25610f7
files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff
changeset
|
239 |
|
8ba2f25610f7
files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff
changeset
|
240 |
|
12904 | 241 |
(* bump_string -- increment suffix of lowercase letters like a base 26 number *) |
242 |
||
243 |
fun bump_string str = |
|
244 |
let |
|
245 |
fun bump [] = ["a"] |
|
246 |
| bump ("z" :: ss) = "a" :: bump ss |
|
247 |
| bump (s :: ss) = |
|
248 |
if size s = 1 andalso ord "a" <= ord s andalso ord s < ord "z" |
|
249 |
then chr (ord s + 1) :: ss |
|
250 |
else "a" :: s :: ss; |
|
251 |
val (cs, qs) = Library.take_suffix is_quasi (sym_explode str); |
|
252 |
in implode (rev (bump (rev cs)) @ qs) end; |
|
253 |
||
6272 | 254 |
|
255 |
(** symbol output **) |
|
256 |
||
10953 | 257 |
(* default *) |
6272 | 258 |
|
259 |
fun string_size s = (s, real (size s)); |
|
260 |
||
13730 | 261 |
val escape = Scan.repeat |
262 |
((($$ "\\" >> K "\\\\") ^^ Scan.optional ($$ "\\" >> K "\\\\") "" ^^ $$ "<" ^^ |
|
263 |
Scan.optional ($$ "^") "" ^^ scan_id ^^ $$ ">") || |
|
264 |
Scan.one not_eof) >> implode; |
|
265 |
||
14557
31ae4a47267c
* cleaner distinction between control symbols "\<^...>" and "\<^raw...>" in
schirmer
parents:
14361
diff
changeset
|
266 |
|
31ae4a47267c
* cleaner distinction between control symbols "\<^...>" and "\<^raw...>" in
schirmer
parents:
14361
diff
changeset
|
267 |
val default_output = string_size |
6272 | 268 |
|
10953 | 269 |
fun default_indent (_: string, k) = spaces k; |
6272 | 270 |
|
10953 | 271 |
|
6272 | 272 |
(* maintain modes *) |
273 |
||
6692 | 274 |
val symbolsN = "symbols"; |
275 |
val xsymbolsN = "xsymbols"; |
|
276 |
||
12116 | 277 |
val modes = |
278 |
ref (Symtab.empty: ((string -> string * real) * (string * int -> string)) Symtab.table); |
|
6272 | 279 |
|
280 |
fun lookup_mode name = Symtab.lookup (! modes, name); |
|
281 |
||
10953 | 282 |
fun add_mode name m = |
6272 | 283 |
(if is_none (lookup_mode name) then () |
6320 | 284 |
else warning ("Redeclaration of symbol print mode " ^ quote name); |
10953 | 285 |
modes := Symtab.update ((name, m), ! modes)); |
286 |
||
287 |
fun get_mode () = |
|
288 |
if_none (get_first lookup_mode (! print_mode)) (default_output, default_indent); |
|
6272 | 289 |
|
290 |
||
291 |
(* mode output *) |
|
292 |
||
10953 | 293 |
fun output_width x = #1 (get_mode ()) x; |
6272 | 294 |
val output = #1 o output_width; |
14557
31ae4a47267c
* cleaner distinction between control symbols "\<^...>" and "\<^raw...>" in
schirmer
parents:
14361
diff
changeset
|
295 |
fun plain_output s = |
31ae4a47267c
* cleaner distinction between control symbols "\<^...>" and "\<^raw...>" in
schirmer
parents:
14361
diff
changeset
|
296 |
if not (exists_string (equal "\\") s) then s |
31ae4a47267c
* cleaner distinction between control symbols "\<^...>" and "\<^raw...>" in
schirmer
parents:
14361
diff
changeset
|
297 |
else fst (Scan.finite stopper escape (explode s)); |
6272 | 298 |
|
10953 | 299 |
fun indent x = #2 (get_mode ()) x; |
300 |
||
6272 | 301 |
|
6116
8ba2f25610f7
files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff
changeset
|
302 |
(*final declarations of this structure!*) |
6272 | 303 |
val length = sym_length; |
6116
8ba2f25610f7
files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff
changeset
|
304 |
val explode = sym_explode; |
6272 | 305 |
|
6116
8ba2f25610f7
files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff
changeset
|
306 |
|
8ba2f25610f7
files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff
changeset
|
307 |
end; |