author  paulson 
Wed, 08 Oct 2003 15:58:15 +0200  
changeset 14221  9276f30eaed6 
parent 14173  a3690aeb79d4 
child 14232  ef550525c591 
permissions  rwrr 
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 frontend 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 

14171
0cab06e3bbd0
Extended the notion of letter and digit, such that now one may use greek,
skalberg
parents:
13730
diff
changeset

88 
local 
0cab06e3bbd0
Extended the notion of letter and digit, such that now one may use greek,
skalberg
parents:
13730
diff
changeset

89 
fun wrap s = "\\<" ^ s ^ ">" 
0cab06e3bbd0
Extended the notion of letter and digit, such that now one may use greek,
skalberg
parents:
13730
diff
changeset

90 

0cab06e3bbd0
Extended the notion of letter and digit, such that now one may use greek,
skalberg
parents:
13730
diff
changeset

91 
val cal_letters = 
0cab06e3bbd0
Extended the notion of letter and digit, such that now one may use greek,
skalberg
parents:
13730
diff
changeset

92 
["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

93 
"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

94 

0cab06e3bbd0
Extended the notion of letter and digit, such that now one may use greek,
skalberg
parents:
13730
diff
changeset

95 
val small_letters = 
0cab06e3bbd0
Extended the notion of letter and digit, such that now one may use greek,
skalberg
parents:
13730
diff
changeset

96 
["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

97 
"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

98 

0cab06e3bbd0
Extended the notion of letter and digit, such that now one may use greek,
skalberg
parents:
13730
diff
changeset

99 
val goth_letters = 
0cab06e3bbd0
Extended the notion of letter and digit, such that now one may use greek,
skalberg
parents:
13730
diff
changeset

100 
["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

101 
"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

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 

0cab06e3bbd0
Extended the notion of letter and digit, such that now one may use greek,
skalberg
parents:
13730
diff
changeset

105 
val greek_letters = 
0cab06e3bbd0
Extended the notion of letter and digit, such that now one may use greek,
skalberg
parents:
13730
diff
changeset

106 
["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

107 
"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

108 
"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

109 
"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

110 

0cab06e3bbd0
Extended the notion of letter and digit, such that now one may use greek,
skalberg
parents:
13730
diff
changeset

111 
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

112 

0cab06e3bbd0
Extended the notion of letter and digit, such that now one may use greek,
skalberg
parents:
13730
diff
changeset

113 
val pre_letters = 
0cab06e3bbd0
Extended the notion of letter and digit, such that now one may use greek,
skalberg
parents:
13730
diff
changeset

114 
cal_letters @ 
0cab06e3bbd0
Extended the notion of letter and digit, such that now one may use greek,
skalberg
parents:
13730
diff
changeset

115 
small_letters @ 
0cab06e3bbd0
Extended the notion of letter and digit, such that now one may use greek,
skalberg
parents:
13730
diff
changeset

116 
goth_letters @ 
0cab06e3bbd0
Extended the notion of letter and digit, such that now one may use greek,
skalberg
parents:
13730
diff
changeset

117 
greek_letters 
0cab06e3bbd0
Extended the notion of letter and digit, such that now one may use greek,
skalberg
parents:
13730
diff
changeset

118 
in 
0cab06e3bbd0
Extended the notion of letter and digit, such that now one may use greek,
skalberg
parents:
13730
diff
changeset

119 
val ext_letters = map wrap pre_letters 
14173  120 

14171
0cab06e3bbd0
Extended the notion of letter and digit, such that now one may use greek,
skalberg
parents:
13730
diff
changeset

121 
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

122 
end 
0cab06e3bbd0
Extended the notion of letter and digit, such that now one may use greek,
skalberg
parents:
13730
diff
changeset

123 

6272  124 
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

125 
(size s = 1 andalso 
0cab06e3bbd0
Extended the notion of letter and digit, such that now one may use greek,
skalberg
parents:
13730
diff
changeset

126 
(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

127 
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

128 
orelse is_ext_letter s 
6272  129 

130 
fun is_digit s = 

14173  131 
size s = 1 andalso ord "0" <= ord s andalso ord s <= ord "9" 
6272  132 

12904  133 
fun is_quasi "_" = true 
134 
 is_quasi "'" = true 

135 
 is_quasi _ = false; 

136 

137 
fun is_quasi_letter s = is_quasi s orelse is_letter s; 

6272  138 

139 
val is_blank = 

14221  140 
fn " " => true  "\t" => true  "\r" => true  "\n" => true  "\^L" => true 
6272  141 
 "\160" => true  "\\<spacespace>" => true 
142 
 _ => false; 

143 

12904  144 
fun is_letdig s = is_quasi_letter s orelse is_digit s; 
6272  145 

8230  146 
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

147 
size s > 2 andalso nth_elem_string (2, s) <> "^" 
14173  148 
andalso not (is_ext_letter s); 
8230  149 

6272  150 
fun is_printable s = 
151 
size s = 1 andalso ord space <= ord s andalso ord s <= ord "~" orelse 

14173  152 
is_ext_letter s orelse 
8230  153 
is_symbolic s; 
154 

13559
51c3ac47d127
added checking so that (rename_tac "x y") is rejected, since
paulson
parents:
12904
diff
changeset

155 
fun is_identifier s = 
51c3ac47d127
added checking so that (rename_tac "x y") is rejected, since
paulson
parents:
12904
diff
changeset

156 
case (explode s) of 
51c3ac47d127
added checking so that (rename_tac "x y") is rejected, since
paulson
parents:
12904
diff
changeset

157 
[] => false 
51c3ac47d127
added checking so that (rename_tac "x y") is rejected, since
paulson
parents:
12904
diff
changeset

158 
 c::cs => is_letter c andalso forall is_letdig cs; 
6272  159 

10738  160 
fun sym_length ss = foldl (fn (n, s) => 
161 
(if not (is_printable s) then 0 else 

162 
(case Library.try String.substring (s, 2, 4) of 

163 
Some s' => if s' = "long" orelse s' = "Long" then 2 else 1 

164 
 None => 1)) + n) (0, ss); 

6272  165 

11010  166 
fun strip_blanks s = 
167 
implode (#1 (Library.take_suffix is_blank (#2 (Library.take_prefix is_blank (explode s))))); 

168 

6272  169 

170 
(* beginning *) 

171 

172 
val smash_blanks = map (fn s => if is_blank s then space else s); 

173 

174 
fun beginning raw_ss = 

175 
let 

176 
val (all_ss, _) = take_suffix is_blank raw_ss; 

177 
val dots = if length all_ss > 10 then " ..." else ""; 

178 
val (ss, _) = take_suffix is_blank (take (10, all_ss)); 

179 
in implode (smash_blanks ss) ^ dots end; 

180 

181 

182 

8998  183 
(** scanning through symbols **) 
6640  184 

185 
fun scanner msg scan chs = 

186 
let 

187 
fun err_msg cs = msg ^ ": " ^ beginning cs; 

188 
val fin_scan = Scan.error (Scan.finite stopper (!! (fn (cs, _) => err_msg cs) scan)); 

189 
in 

190 
(case fin_scan chs of 

191 
(result, []) => result 

192 
 (_, rest) => error (err_msg rest)) 

193 
end; 

194 

195 

196 

6272  197 
(** symbol input **) 
6116
8ba2f25610f7
files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff
changeset

198 

8ba2f25610f7
files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff
changeset

199 
(* scan *) 
8ba2f25610f7
files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff
changeset

200 

8ba2f25610f7
files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff
changeset

201 
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

202 

8ba2f25610f7
files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff
changeset

203 
val scan = 
8ba2f25610f7
files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff
changeset

204 
($$ "\\"  Scan.optional ($$ "\\") "") ^^ $$ "<" ^^ 
8ba2f25610f7
files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff
changeset

205 
!! (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

206 
(Scan.optional ($$ "^") "" ^^ scan_id ^^ $$ ">")  
8ba2f25610f7
files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff
changeset

207 
Scan.one not_eof; 
8ba2f25610f7
files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff
changeset

208 

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 
(* source *) 
8ba2f25610f7
files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff
changeset

211 

10747  212 
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

213 

8ba2f25610f7
files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff
changeset

214 
fun source do_recover src = 
8ba2f25610f7
files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff
changeset

215 
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

216 

8ba2f25610f7
files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff
changeset

217 

8ba2f25610f7
files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff
changeset

218 
(* explode *) 
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 
fun no_syms [] = true 
8ba2f25610f7
files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff
changeset

221 
 no_syms ("\\" :: "<" :: _) = false 
12116  222 
 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

223 

8ba2f25610f7
files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff
changeset

224 
fun sym_explode str = 
8ba2f25610f7
files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff
changeset

225 
let val chs = explode str in 
8ba2f25610f7
files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff
changeset

226 
if no_syms chs then chs (*tune trivial case*) 
12116  227 
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

228 
end; 
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 

12904  231 
(* bump_string  increment suffix of lowercase letters like a base 26 number *) 
232 

233 
fun bump_string str = 

234 
let 

235 
fun bump [] = ["a"] 

236 
 bump ("z" :: ss) = "a" :: bump ss 

237 
 bump (s :: ss) = 

238 
if size s = 1 andalso ord "a" <= ord s andalso ord s < ord "z" 

239 
then chr (ord s + 1) :: ss 

240 
else "a" :: s :: ss; 

241 
val (cs, qs) = Library.take_suffix is_quasi (sym_explode str); 

242 
in implode (rev (bump (rev cs)) @ qs) end; 

243 

6272  244 

245 
(** symbol output **) 

246 

10953  247 
(* default *) 
6272  248 

249 
fun string_size s = (s, real (size s)); 

250 

13730  251 
val escape = Scan.repeat 
252 
((($$ "\\" >> K "\\\\") ^^ Scan.optional ($$ "\\" >> K "\\\\") "" ^^ $$ "<" ^^ 

253 
Scan.optional ($$ "^") "" ^^ scan_id ^^ $$ ">")  

254 
Scan.one not_eof) >> implode; 

255 

6272  256 
fun default_output s = 
6320  257 
if not (exists_string (equal "\\") s) then string_size s 
13730  258 
else string_size (fst (Scan.finite stopper escape (explode s))); 
6272  259 

10953  260 
fun default_indent (_: string, k) = spaces k; 
6272  261 

10953  262 

6272  263 
(* maintain modes *) 
264 

6692  265 
val symbolsN = "symbols"; 
266 
val xsymbolsN = "xsymbols"; 

267 

12116  268 
val modes = 
269 
ref (Symtab.empty: ((string > string * real) * (string * int > string)) Symtab.table); 

6272  270 

271 
fun lookup_mode name = Symtab.lookup (! modes, name); 

272 

10953  273 
fun add_mode name m = 
6272  274 
(if is_none (lookup_mode name) then () 
6320  275 
else warning ("Redeclaration of symbol print mode " ^ quote name); 
10953  276 
modes := Symtab.update ((name, m), ! modes)); 
277 

278 
fun get_mode () = 

279 
if_none (get_first lookup_mode (! print_mode)) (default_output, default_indent); 

6272  280 

281 

282 
(* mode output *) 

283 

10953  284 
fun output_width x = #1 (get_mode ()) x; 
6272  285 
val output = #1 o output_width; 
10923  286 
val plain_output = #1 o default_output; 
6272  287 

10953  288 
fun indent x = #2 (get_mode ()) x; 
289 

6272  290 

6116
8ba2f25610f7
files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff
changeset

291 
(*final declarations of this structure!*) 
6272  292 
val length = sym_length; 
6116
8ba2f25610f7
files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff
changeset

293 
val explode = sym_explode; 
6272  294 

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 
end; 