--- a/NEWS Fri Nov 19 23:48:07 2010 +0100
+++ b/NEWS Sat Nov 20 00:53:26 2010 +0100
@@ -490,6 +490,10 @@
*** ML ***
+* Renamed raw "explode" function to "raw_explode" to emphasize its
+meaning. Note that internally to Isabelle, Symbol.explode is used in
+almost all situations.
+
* Discontinued obsolete function sys_error and exception SYS_ERROR.
See implementation manual for further details on exceptions in
Isabelle/ML.
--- a/src/HOL/Boogie/Tools/boogie_commands.ML Fri Nov 19 23:48:07 2010 +0100
+++ b/src/HOL/Boogie/Tools/boogie_commands.ML Sat Nov 20 00:53:26 2010 +0100
@@ -116,7 +116,7 @@
end
fun write_list head =
- map Pretty.str o sort (dict_ord string_ord o pairself explode) #>
+ map Pretty.str o sort (dict_ord string_ord o pairself raw_explode) #>
Pretty.writeln o Pretty.big_list head
fun parens s = "(" ^ s ^ ")"
--- a/src/HOL/Boogie/Tools/boogie_loader.ML Fri Nov 19 23:48:07 2010 +0100
+++ b/src/HOL/Boogie/Tools/boogie_loader.ML Sat Nov 20 00:53:26 2010 +0100
@@ -344,7 +344,7 @@
| (_, ts') => error (scan_err "unparsed input" ts'))
end
-fun read_int' s = (case read_int (explode s) of (i, []) => SOME i | _ => NONE)
+fun read_int' s = (case read_int (raw_explode s) of (i, []) => SOME i | _ => NONE)
fun $$$ s = Scan.one (fn (_, Token s') => s = s' | _ => false)
fun str st = Scan.some (fn (_, Token s) => SOME s | _ => NONE) st
--- a/src/HOL/Import/lazy_seq.ML Fri Nov 19 23:48:07 2010 +0100
+++ b/src/HOL/Import/lazy_seq.ML Sat Nov 20 00:53:26 2010 +0100
@@ -543,7 +543,7 @@
F e (getItem s)
end
-fun fromString s = of_list (explode s)
+fun fromString s = of_list (raw_explode s)
end
--- a/src/HOL/Import/mono_scan.ML Fri Nov 19 23:48:07 2010 +0100
+++ b/src/HOL/Import/mono_scan.ML Sat Nov 20 00:53:26 2010 +0100
@@ -233,6 +233,6 @@
fun this [] = (fn toks => ([], toks))
| this (xs' as (x::xs)) = one (fn y => x=y) -- this xs >> K xs'
-fun this_string s = this (explode s) >> K s
+fun this_string s = this (raw_explode s) >> K s
end
\ No newline at end of file
--- a/src/HOL/Import/proof_kernel.ML Fri Nov 19 23:48:07 2010 +0100
+++ b/src/HOL/Import/proof_kernel.ML Sat Nov 20 00:53:26 2010 +0100
@@ -501,8 +501,8 @@
fun replacestr x y s =
let
- val xl = explode x
- val yl = explode y
+ val xl = raw_explode x
+ val yl = raw_explode y
fun isprefix [] ys = true
| isprefix (x::xs) (y::ys) = if x = y then isprefix xs ys else false
| isprefix _ _ = false
@@ -511,7 +511,7 @@
fun r [] = []
| r (S as (s::ss)) = if isp S then r (chg S) else s::(r ss)
in
- implode(r (explode s))
+ implode(r (raw_explode s))
end
fun protect_factname s = replacestr "." "_dot_" s
--- a/src/HOL/Import/scan.ML Fri Nov 19 23:48:07 2010 +0100
+++ b/src/HOL/Import/scan.ML Sat Nov 20 00:53:26 2010 +0100
@@ -213,7 +213,7 @@
fun this [] = (fn toks => ([], toks))
| this (xs' as (x::xs)) = one (fn y => x=y) -- this xs >> K xs'
-fun this_string s = this (explode s) >> K s
+fun this_string s = this (raw_explode s) >> K s
end
--- a/src/HOL/Import/seq.ML Fri Nov 19 23:48:07 2010 +0100
+++ b/src/HOL/Import/seq.ML Sat Nov 20 00:53:26 2010 +0100
@@ -94,6 +94,6 @@
open Extended
val fromList = I
-val fromString = explode
+val fromString = raw_explode
end
--- a/src/HOL/Library/Sum_Of_Squares/sum_of_squares.ML Fri Nov 19 23:48:07 2010 +0100
+++ b/src/HOL/Library/Sum_Of_Squares/sum_of_squares.ML Sat Nov 20 00:53:26 2010 +0100
@@ -79,7 +79,7 @@
val z = pow10(~ e) */ y +/ rat_1
val k = int_of_rat (round_rat(pow10 d */ z))
in (if x </ rat_0 then "-0." else "0.") ^
- implode(tl(explode(string_of_int k))) ^
+ implode(tl(raw_explode(string_of_int k))) ^
(if e = 0 then "" else "e"^string_of_int e)
end
end;
@@ -558,7 +558,7 @@
>> (fn (h, x) => h */ pow10 (int_of_rat x));
fun mkparser p s =
- let val (x,rst) = p (explode s)
+ let val (x,rst) = p (raw_explode s)
in if null rst then x
else error "mkparser: unparsed input"
end;;
--- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Fri Nov 19 23:48:07 2010 +0100
+++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Sat Nov 20 00:53:26 2010 +0100
@@ -444,7 +444,7 @@
val (prover_name, _) = get_prover ctxt args
val timeout =
AList.lookup (op =) args minimize_timeoutK
- |> Option.map (fst o read_int o explode)
+ |> Option.map (fst o read_int o raw_explode) (* FIXME Symbol.explode (?) *)
|> the_default 5
val params = Sledgehammer_Isar.default_params ctxt
[("verbose", "true"),
--- a/src/HOL/Nominal/nominal_datatype.ML Fri Nov 19 23:48:07 2010 +0100
+++ b/src/HOL/Nominal/nominal_datatype.ML Sat Nov 20 00:53:26 2010 +0100
@@ -723,7 +723,7 @@
| reindex (DtRec i) = DtRec (the (AList.lookup op = ty_idxs i))
| reindex dt = dt;
- fun strip_suffix i s = implode (List.take (explode s, size s - i));
+ fun strip_suffix i s = implode (List.take (raw_explode s, size s - i)); (* FIXME Symbol.explode (?) *)
(** strips the "_Rep" in type names *)
fun strip_nth_name i s =
--- a/src/HOL/Proofs/Lambda/WeakNorm.thy Fri Nov 19 23:48:07 2010 +0100
+++ b/src/HOL/Proofs/Lambda/WeakNorm.thy Sat Nov 20 00:53:26 2010 +0100
@@ -389,7 +389,7 @@
ML {*
fun dBtype_of_typ (Type ("fun", [T, U])) =
@{code Fun} (dBtype_of_typ T, dBtype_of_typ U)
- | dBtype_of_typ (TFree (s, _)) = (case explode s of
+ | dBtype_of_typ (TFree (s, _)) = (case raw_explode s of
["'", a] => @{code Atom} (@{code nat} (ord a - 97))
| _ => error "dBtype_of_typ: variable name")
| dBtype_of_typ _ = error "dBtype_of_typ: bad type";
@@ -458,7 +458,7 @@
fun dBtype_of_typ (Type ("fun", [T, U])) =
Norm.Fun (dBtype_of_typ T, dBtype_of_typ U)
- | dBtype_of_typ (TFree (s, _)) = (case explode s of
+ | dBtype_of_typ (TFree (s, _)) = (case raw_explode s of
["'", a] => Norm.Atom (nat_of_int (ord a - 97))
| _ => error "dBtype_of_typ: variable name")
| dBtype_of_typ _ = error "dBtype_of_typ: bad type";
--- a/src/HOL/Tools/ATP/atp_proof.ML Fri Nov 19 23:48:07 2010 +0100
+++ b/src/HOL/Tools/ATP/atp_proof.ML Sat Nov 20 00:53:26 2010 +0100
@@ -321,7 +321,7 @@
fst o Scan.finite Symbol.stopper
(Scan.error (!! (fn _ => raise Fail "unrecognized ATP output")
(Scan.repeat1 parse_line)))
- o explode o strip_spaces_except_between_ident_chars
+ o raw_explode o strip_spaces_except_between_ident_chars
fun clean_up_dependency seen dep = find_first (curry is_same_step dep) seen
fun clean_up_dependencies _ [] = []
--- a/src/HOL/Tools/Datatype/datatype_prop.ML Fri Nov 19 23:48:07 2010 +0100
+++ b/src/HOL/Tools/Datatype/datatype_prop.ML Sat Nov 20 00:53:26 2010 +0100
@@ -48,7 +48,7 @@
fun make_tnames Ts =
let
- fun type_name (TFree (name, _)) = implode (tl (explode name))
+ fun type_name (TFree (name, _)) = implode (tl (raw_explode name)) (* FIXME Symbol.explode (?) *)
| type_name (Type (name, _)) =
let val name' = Long_Name.base_name name
in if Syntax.is_identifier name' then name' else "x" end;
--- a/src/HOL/Tools/Function/size.ML Fri Nov 19 23:48:07 2010 +0100
+++ b/src/HOL/Tools/Function/size.ML Sat Nov 20 00:53:26 2010 +0100
@@ -71,7 +71,7 @@
val ((param_size_fs, param_size_fTs), f_names) = paramTs |>
map (fn T as TFree (s, _) =>
let
- val name = "f" ^ implode (tl (explode s));
+ val name = "f" ^ implode (tl (raw_explode s)); (* FIXME Symbol.explode (?) *)
val U = T --> HOLogic.natT
in
(((s, Free (name, U)), U), name)
--- a/src/HOL/Tools/Nitpick/kodkod.ML Fri Nov 19 23:48:07 2010 +0100
+++ b/src/HOL/Tools/Nitpick/kodkod.ML Sat Nov 20 00:53:26 2010 +0100
@@ -908,7 +908,7 @@
raise SYNTAX ("Kodkod.extract_instance",
"ill-formed Kodkodi output"))
(parse_instance new_kodkodi)))
- o strip_blanks o explode
+ o strip_blanks o raw_explode
val problem_marker = "*** PROBLEM "
val outcome_marker = "---OUTCOME---\n"
--- a/src/HOL/Tools/Nitpick/nitpick_model.ML Fri Nov 19 23:48:07 2010 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_model.ML Sat Nov 20 00:53:26 2010 +0100
@@ -120,7 +120,7 @@
| NONE => (Unsynchronized.change pool (cons (T, [j])); 1)
fun atom_suffix s =
nat_subscript
- #> (s <> "" andalso Symbol.is_ascii_digit (List.last (explode s)))
+ #> (s <> "" andalso Symbol.is_ascii_digit (List.last (raw_explode s))) (* FIXME Symbol.explode (?) *)
? prefix "\<^isub>,"
fun nth_atom_name thy atomss pool prefix T j =
let
--- a/src/HOL/Tools/Nitpick/nitpick_util.ML Fri Nov 19 23:48:07 2010 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_util.ML Sat Nov 20 00:53:26 2010 +0100
@@ -240,7 +240,7 @@
val parse_time_option = Sledgehammer_Util.parse_time_option
val string_from_time = Sledgehammer_Util.string_from_time
-val i_subscript = implode o map (prefix "\<^isub>") o explode
+val i_subscript = implode o map (prefix "\<^isub>") o raw_explode (* FIXME Symbol.explode (?) *)
fun be_subscript s = "\<^bsub>" ^ s ^ "\<^esub>"
fun nat_subscript n =
let val s = signed_string_of_int n in
--- a/src/HOL/Tools/SMT/z3_model.ML Fri Nov 19 23:48:07 2010 +0100
+++ b/src/HOL/Tools/SMT/z3_model.ML Sat Nov 20 00:53:26 2010 +0100
@@ -38,7 +38,7 @@
(fn sign => nat_num >> sign))
val is_char = Symbol.is_ascii_letter orf Symbol.is_ascii_digit orf
- member (op =) (explode "_+*-/%~=<>$&|?!.@^#")
+ member (op =) (raw_explode "_+*-/%~=<>$&|?!.@^#")
val name = spaced (Scan.many1 is_char >> implode)
fun $$$ s = spaced (Scan.this_string s)
@@ -68,7 +68,7 @@
Scan.repeat (name --| $$$ "->" -- (func || expr >> (single o pair [])))
fun read_cex ls =
- maps (cons "\n" o explode) ls
+ maps (cons "\n" o raw_explode) ls
|> try (fst o Scan.finite Symbol.stopper cex)
|> the_default []
--- a/src/HOL/Tools/SMT/z3_proof_parser.ML Fri Nov 19 23:48:07 2010 +0100
+++ b/src/HOL/Tools/SMT/z3_proof_parser.ML Sat Nov 20 00:53:26 2010 +0100
@@ -256,7 +256,7 @@
fun parse_line _ _ (st as ((SOME _, _), _)) = st
| parse_line scan line ((_, line_no), cx) =
- let val st = ((line_no, cx), explode line)
+ let val st = ((line_no, cx), raw_explode line)
in
(case Scan.catch (Scan.finite' Symbol.stopper (Scan.option scan)) st of
(SOME r, ((_, cx'), _)) => ((r, line_no+1), cx')
@@ -299,7 +299,7 @@
(fn sign => nat_num >> sign)) st
val is_char = Symbol.is_ascii_letter orf Symbol.is_ascii_digit orf
- member (op =) (explode "_+*-/%~=<>$&|?!.@^#")
+ member (op =) (raw_explode "_+*-/%~=<>$&|?!.@^#")
fun name st = (Scan.lift (Scan.many1 is_char) >> implode) st
fun sym st =
--- a/src/HOL/Tools/Sledgehammer/sledgehammer.ML Fri Nov 19 23:48:07 2010 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer.ML Sat Nov 20 00:53:26 2010 +0100
@@ -313,7 +313,7 @@
val digit = Scan.one Symbol.is_ascii_digit;
val num3 = as_num (digit ::: digit ::: (digit >> single));
val time = num --| Scan.$$ "." -- num3 >> (fn (a, b) => a * 1000 + b);
- val as_time = Scan.read Symbol.stopper time o explode
+ val as_time = Scan.read Symbol.stopper time o raw_explode
in (output, as_time t) end;
fun run_on probfile =
case filter (curry (op =) "" o getenv o fst) (exec :: required_execs) of
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_atp_reconstruct.ML Fri Nov 19 23:48:07 2010 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_atp_reconstruct.ML Sat Nov 20 00:53:26 2010 +0100
@@ -81,7 +81,7 @@
val extract_clause_formula_relation =
Substring.full #> Substring.position set_ClauseFormulaRelationN
#> snd #> Substring.position "." #> fst #> Substring.string
- #> explode #> filter_out Symbol.is_blank #> parse_clause_formula_relation
+ #> raw_explode #> filter_out Symbol.is_blank #> parse_clause_formula_relation
#> fst
fun repair_conjecture_shape_and_fact_names output conjecture_shape fact_names =
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML Fri Nov 19 23:48:07 2010 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML Sat Nov 20 00:53:26 2010 +0100
@@ -51,7 +51,7 @@
end
val has_junk =
- exists (fn s => not (Symbol.is_digit s) andalso s <> ".") o explode
+ exists (fn s => not (Symbol.is_digit s) andalso s <> ".") o raw_explode (* FIXME Symbol.explode (?) *)
fun parse_time_option _ "none" = NONE
| parse_time_option name s =
@@ -66,7 +66,7 @@
fun string_from_time t =
string_of_real (0.01 * Real.fromInt (Time.toMilliseconds t div 10)) ^ " s"
-val subscript = implode o map (prefix "\<^isub>") o explode
+val subscript = implode o map (prefix "\<^isub>") o raw_explode (* FIXME Symbol.explode (?) *)
fun nat_subscript n =
n |> string_of_int |> print_mode_active Symbol.xsymbolsN ? subscript
--- a/src/HOL/Tools/hologic.ML Fri Nov 19 23:48:07 2010 +0100
+++ b/src/HOL/Tools/hologic.ML Sat Nov 20 00:53:26 2010 +0100
@@ -598,7 +598,7 @@
val stringT = listT charT;
-val mk_string = mk_list charT o map (mk_char o ord) o explode;
+val mk_string = mk_list charT o map (mk_char o ord) o raw_explode;
val dest_string = implode o map (chr o dest_char) o dest_list;
--- a/src/HOL/Tools/refute.ML Fri Nov 19 23:48:07 2010 +0100
+++ b/src/HOL/Tools/refute.ML Sat Nov 20 00:53:26 2010 +0100
@@ -2955,7 +2955,7 @@
(* string -> string *)
fun strip_leading_quote s =
(implode o (fn [] => [] | x::xs => if x="'" then xs else x::xs)
- o explode) s
+ o raw_explode) s (* FIXME Symbol.explode (?) *)
(* Term.typ -> string *)
fun string_of_typ (Type (s, _)) = s
| string_of_typ (TFree (x, _)) = strip_leading_quote x
--- a/src/HOL/Tools/string_syntax.ML Fri Nov 19 23:48:07 2010 +0100
+++ b/src/HOL/Tools/string_syntax.ML Sat Nov 20 00:53:26 2010 +0100
@@ -32,7 +32,7 @@
Syntax.Appl [Syntax.Constant @{const_syntax Char}, mk_nib (ord s div 16), mk_nib (ord s mod 16)]
else error ("Non-ASCII symbol: " ^ quote s);
-val specials = explode "\\\"`'";
+val specials = raw_explode "\\\"`'";
fun dest_chr c1 c2 =
let val c = chr (dest_nib c1 * 16 + dest_nib c2) in
--- a/src/Pure/General/path.ML Fri Nov 19 23:48:07 2010 +0100
+++ b/src/Pure/General/path.ML Sat Nov 20 00:53:26 2010 +0100
@@ -73,9 +73,9 @@
val current = Path [];
val root = Path [Root ""];
-fun named_root s = Path [root_elem (explode s)];
-fun basic s = Path [basic_elem (explode s)];
-fun variable s = Path [variable_elem (explode s)];
+fun named_root s = Path [root_elem (raw_explode s)];
+fun basic s = Path [basic_elem (raw_explode s)];
+fun variable s = Path [variable_elem (raw_explode s)];
val parent = Path [Parent];
fun is_absolute (Path xs) =
@@ -128,7 +128,7 @@
| explode_elem "~" = Variable "HOME"
| explode_elem "~~" = Variable "ISABELLE_HOME"
| explode_elem s =
- (case explode s of
+ (case raw_explode s of
"$" :: cs => variable_elem cs
| cs => basic_elem cs);
@@ -143,7 +143,7 @@
(0, es) => ([], es)
| (1, es) => ([Root ""], es)
| (_, []) => ([Root ""], [])
- | (_, e :: es) => ([root_elem (explode e)], es))
+ | (_, e :: es) => ([root_elem (raw_explode e)], es))
in Path (norm (explode_elems raw_elems @ roots)) end;
end;
@@ -161,7 +161,7 @@
| ext e = split_path (fn (prfx, s) => append prfx (basic (s ^ "." ^ e)));
val split_ext = split_path (fn (prfx, s) => apfst (append prfx)
- (case take_suffix (fn c => c <> ".") (explode s) of
+ (case take_suffix (fn c => c <> ".") (raw_explode s) of
([], _) => (Path [Basic s], "")
| (cs, e) => (Path [Basic (implode (take (length cs - 1) cs))], implode e)));
--- a/src/Pure/General/scan.ML Fri Nov 19 23:48:07 2010 +0100
+++ b/src/Pure/General/scan.ML Sat Nov 20 00:53:26 2010 +0100
@@ -154,7 +154,7 @@
if (y: string) = x then drop_prefix ys xs else raise FAIL NONE;
in (ys, drop_prefix ys xs) end;
-fun this_string s = this (explode s) >> K s; (*primitive string -- no symbols here!*)
+fun this_string s = this (raw_explode s) >> K s; (*primitive string -- no symbols here!*)
fun many _ [] = raise MORE NONE
| many pred (lst as x :: xs) =
--- a/src/Pure/General/source.ML Fri Nov 19 23:48:07 2010 +0100
+++ b/src/Pure/General/source.ML Sat Nov 20 00:53:26 2010 +0100
@@ -107,7 +107,7 @@
(* string source *)
-val of_string = of_list o explode;
+val of_string = of_list o raw_explode;
fun of_string_limited limit str =
make_source [] (Substring.full str) default_prompt
@@ -127,14 +127,14 @@
NONE => []
| SOME 0 => []
| SOME _ => TextIO.input instream :: slurp ());
- in maps explode (slurp ()) end;
+ in maps raw_explode (slurp ()) end;
fun tty in_stream = make_source [] () default_prompt (fn prompt => fn () =>
let val input = slurp_input in_stream in
if exists (fn c => c = "\n") input then (input, ())
else
(case (Output.prompt prompt; TextIO.inputLine in_stream) of
- SOME line => (input @ explode line, ())
+ SOME line => (input @ raw_explode line, ())
| NONE => (input, ()))
end);
--- a/src/Pure/General/symbol.ML Fri Nov 19 23:48:07 2010 +0100
+++ b/src/Pure/General/symbol.ML Sat Nov 20 00:53:26 2010 +0100
@@ -188,7 +188,7 @@
| enc ([], d :: ds) = raw2 d :: encode ds
| enc (cs, d :: ds) = raw1 cs :: raw2 d :: encode ds;
in
- if exists_string (not o raw_chr) str then implode (encode (explode str))
+ if exists_string (not o raw_chr) str then implode (encode (raw_explode str))
else raw0 str
end;
@@ -215,7 +215,7 @@
fun decode_raw s =
if not (is_raw s) then error (malformed_msg s)
else if String.isPrefix "\\<^raw:" s then String.substring (s, 7, size s - 8)
- else chr (#1 (Library.read_int (explode (String.substring (s, 6, size s - 7)))));
+ else chr (#1 (Library.read_int (raw_explode (String.substring (s, 6, size s - 7)))));
(* symbol variants *)
@@ -470,7 +470,7 @@
in
fun sym_explode str =
- let val chs = explode str in
+ let val chs = raw_explode str in
if no_explode chs then chs
else Source.exhaust (source (Source.of_list chs))
end;
--- a/src/Pure/General/xml.ML Fri Nov 19 23:48:07 2010 +0100
+++ b/src/Pure/General/xml.ML Sat Nov 20 00:53:26 2010 +0100
@@ -158,7 +158,7 @@
val parse_comments =
blanks -- Scan.repeat (parse_comment -- blanks >> K ()) >> K ();
-val parse_string = Scan.read Symbol.stopper parse_chars o explode;
+val parse_string = Scan.read Symbol.stopper parse_chars o raw_explode;
fun parse_content xs =
(parse_optional_text @@@
@@ -184,7 +184,7 @@
fun parse s =
(case Scan.finite Symbol.stopper (Scan.error (!! (err "Malformed element")
- (blanks |-- parse_document --| blanks))) (explode s) of
+ (blanks |-- parse_document --| blanks))) (raw_explode s) of
(x, []) => x
| (_, ys) => error ("XML parsing error: Unprocessed input\n" ^ Symbol.beginning 100 ys));
--- a/src/Pure/Isar/class.ML Fri Nov 19 23:48:07 2010 +0100
+++ b/src/Pure/Isar/class.ML Sat Nov 20 00:53:26 2010 +0100
@@ -477,7 +477,7 @@
--| junk))
::: Scan.repeat ((Scan.many1 is_valid >> implode) --| junk));
in
- explode #> scan_valids #> implode
+ raw_explode #> scan_valids #> implode
end;
val type_name = sanitize_name o Long_Name.base_name;
--- a/src/Pure/Isar/token.ML Fri Nov 19 23:48:07 2010 +0100
+++ b/src/Pure/Isar/token.ML Sat Nov 20 00:53:26 2010 +0100
@@ -265,7 +265,7 @@
(* scan symbolic idents *)
-val is_sym_char = member (op =) (explode "!#$%&*+-/<=>?@^_|~");
+val is_sym_char = member (op =) (raw_explode "!#$%&*+-/<=>?@^_|~");
val scan_symid =
Scan.many1 (is_sym_char o Symbol_Pos.symbol) ||
--- a/src/Pure/ML-Systems/polyml_common.ML Fri Nov 19 23:48:07 2010 +0100
+++ b/src/Pure/ML-Systems/polyml_common.ML Sat Nov 20 00:53:26 2010 +0100
@@ -29,6 +29,7 @@
val _ = PolyML.Compiler.forgetValue "foldl";
val _ = PolyML.Compiler.forgetValue "foldr";
val _ = PolyML.Compiler.forgetValue "print";
+val _ = PolyML.Compiler.forgetValue "explode";
(* Compiler options *)
@@ -48,7 +49,7 @@
val ord = SML90.ord;
val chr = SML90.chr;
-val explode = SML90.explode;
+val raw_explode = SML90.explode;
val implode = SML90.implode;
--- a/src/Pure/ML-Systems/smlnj.ML Fri Nov 19 23:48:07 2010 +0100
+++ b/src/Pure/ML-Systems/smlnj.ML Sat Nov 20 00:53:26 2010 +0100
@@ -30,9 +30,9 @@
(* restore old-style character / string functions *)
-val ord = mk_int o SML90.ord;
-val chr = SML90.chr o dest_int;
-val explode = SML90.explode;
+val ord = mk_int o SML90.ord;
+val chr = SML90.chr o dest_int;
+val raw_explode = SML90.explode;
val implode = SML90.implode;
--- a/src/Pure/ML/ml_lex.ML Fri Nov 19 23:48:07 2010 +0100
+++ b/src/Pure/ML/ml_lex.ML Sat Nov 20 00:53:26 2010 +0100
@@ -149,7 +149,7 @@
"sharing", "sig", "signature", "struct", "structure", "then", "type",
"val", "where", "while", "with", "withtype"];
-val lex = Scan.make_lexicon (map explode keywords);
+val lex = Scan.make_lexicon (map raw_explode keywords);
fun scan_keyword x = Scan.literal lex x;
@@ -166,7 +166,7 @@
Scan.one (Symbol.is_ascii_letter o Symbol_Pos.symbol) -- scan_letdigs >> op ::;
val scan_symbolic =
- Scan.many1 (member (op =) (explode "!#$%&*+-/:<=>?@\\^`|~") o Symbol_Pos.symbol);
+ Scan.many1 (member (op =) (raw_explode "!#$%&*+-/:<=>?@\\^`|~") o Symbol_Pos.symbol);
in
@@ -211,7 +211,7 @@
local
val scan_escape =
- Scan.one (member (op =) (explode "\"\\abtnvfr") o Symbol_Pos.symbol) >> single ||
+ Scan.one (member (op =) (raw_explode "\"\\abtnvfr") o Symbol_Pos.symbol) >> single ||
$$$ "^" @@@ (Scan.one (fn (s, _) => ord "@" <= ord s andalso ord s <= ord "_") >> single) ||
Scan.one (Symbol.is_ascii_digit o Symbol_Pos.symbol) --
Scan.one (Symbol.is_ascii_digit o Symbol_Pos.symbol) --
--- a/src/Pure/Proof/extraction.ML Fri Nov 19 23:48:07 2010 +0100
+++ b/src/Pure/Proof/extraction.ML Sat Nov 20 00:53:26 2010 +0100
@@ -68,7 +68,7 @@
| rlz_proc _ = NONE;
val unpack_ixn = apfst implode o apsnd (fst o read_int o tl) o
- take_prefix (fn s => s <> ":") o explode;
+ take_prefix (fn s => s <> ":") o raw_explode;
type rules =
{next: int, rs: ((term * term) list * (term * term)) list,
--- a/src/Pure/codegen.ML Fri Nov 19 23:48:07 2010 +0100
+++ b/src/Pure/codegen.ML Sat Nov 20 00:53:26 2010 +0100
@@ -355,7 +355,7 @@
Symbol.is_ascii_digit x orelse Symbol.is_ascii_quasi x;
fun dest_sym s =
- (case split_last (snd (take_prefix (fn c => c = "\\") (explode s))) of
+ (case split_last (snd (take_prefix (fn c => c = "\\") (raw_explode s))) of
("<" :: "^" :: xs, ">") => (true, implode xs)
| ("<" :: xs, ">") => (false, implode xs)
| _ => raise Fail "dest_sym");
@@ -374,7 +374,7 @@
| (ys, zs) => implode ys :: check_str zs);
val s' = space_implode "_" (maps (check_str o Symbol.explode) (Long_Name.explode s))
in
- if Symbol.is_ascii_letter (hd (explode s')) then s' else "id_" ^ s'
+ if Symbol.is_ascii_letter (hd (raw_explode s')) then s' else "id_" ^ s'
end;
fun mk_long_id (p as (tab, used)) module s =
@@ -826,7 +826,7 @@
(**** Reflection ****)
-val strip_tname = implode o tl o explode;
+val strip_tname = implode o tl o raw_explode;
fun pretty_list xs = Pretty.block (str "[" ::
flat (separate [str ",", Pretty.brk 1] (map single xs)) @
@@ -962,7 +962,7 @@
val _ = List.app Keyword.keyword ["attach", "file", "contains"];
fun strip_whitespace s = implode (fst (take_suffix (fn c => c = "\n" orelse c = " ")
- (snd (take_prefix (fn c => c = "\n" orelse c = " ") (explode s))))) ^ "\n";
+ (snd (take_prefix (fn c => c = "\n" orelse c = " ") (raw_explode s))))) ^ "\n";
val parse_attach = Scan.repeat (Parse.$$$ "attach" |--
Scan.optional (Parse.$$$ "(" |-- Parse.xname --| Parse.$$$ ")") "" --
--- a/src/Pure/library.ML Fri Nov 19 23:48:07 2010 +0100
+++ b/src/Pure/library.ML Sat Nov 20 00:53:26 2010 +0100
@@ -669,7 +669,7 @@
val read_int = read_radix_int 10;
-fun oct_char s = chr (#1 (read_radix_int 8 (explode s)));
+fun oct_char s = chr (#1 (read_radix_int 8 (raw_explode s)));
--- a/src/Pure/name.ML Fri Nov 19 23:48:07 2010 +0100
+++ b/src/Pure/name.ML Sat Nov 20 00:53:26 2010 +0100
@@ -166,7 +166,7 @@
if is_valid x then x :: xs
else
(case Symbol.decode x of
- Symbol.Sym name => "_" :: explode name @ sep xs
+ Symbol.Sym name => "_" :: raw_explode name @ sep xs
| _ => sep xs);
fun upper_lower cs =
if upper then nth_map 0 Symbol.to_ascii_upper cs
--- a/src/Tools/Code/code_ml.ML Fri Nov 19 23:48:07 2010 +0100
+++ b/src/Tools/Code/code_ml.ML Sat Nov 20 00:53:26 2010 +0100
@@ -679,7 +679,7 @@
fun chr i =
let
val xs = string_of_int i;
- val ys = replicate_string (3 - length (explode xs)) "0";
+ val ys = replicate_string (3 - length (raw_explode xs)) "0";
in "\\" ^ ys ^ xs end;
fun char_ocaml c =
let
--- a/src/Tools/Code/code_printer.ML Fri Nov 19 23:48:07 2010 +0100
+++ b/src/Tools/Code/code_printer.ML Sat Nov 20 00:53:26 2010 +0100
@@ -173,8 +173,8 @@
of SOME name' => name'
| NONE => error ("Invalid name in context: " ^ quote name);
-val first_upper = implode o nth_map 0 Symbol.to_ascii_upper o explode;
-val first_lower = implode o nth_map 0 Symbol.to_ascii_lower o explode;
+val first_upper = implode o nth_map 0 Symbol.to_ascii_upper o raw_explode;
+val first_lower = implode o nth_map 0 Symbol.to_ascii_lower o raw_explode;
fun aux_params vars lhss =
let
--- a/src/Tools/IsaPlanner/rw_tools.ML Fri Nov 19 23:48:07 2010 +0100
+++ b/src/Tools/IsaPlanner/rw_tools.ML Sat Nov 20 00:53:26 2010 +0100
@@ -20,10 +20,10 @@
construction/definition. *)
(*
fun dest_fake_bound_name n =
- case (explode n) of
+ case (raw_explode n) of (* FIXME Symbol.explode (?) *)
(":" :: realchars) => implode realchars
| _ => n; *)
-fun is_fake_bound_name n = (hd (explode n) = ":");
+fun is_fake_bound_name n = (hd (raw_explode n) = ":"); (* FIXME Symbol.explode (?) *)
fun mk_fake_bound_name n = ":b_" ^ n;
@@ -31,20 +31,20 @@
(* fake free variable names for local meta variables - these work
as placeholders. *)
fun dest_fake_fix_name n =
- case (explode n) of
+ case (raw_explode n) of (* FIXME Symbol.explode (?) *)
("@" :: realchars) => implode realchars
| _ => n;
-fun is_fake_fix_name n = (hd (explode n) = "@");
+fun is_fake_fix_name n = (hd (raw_explode n) = "@"); (* FIXME Symbol.explode (?) *)
fun mk_fake_fix_name n = "@" ^ n;
(* fake free variable names for meta level bound variables *)
fun dest_fake_all_name n =
- case (explode n) of
+ case (raw_explode n) of (* FIXME Symbol.explode (?) *)
("+" :: realchars) => implode realchars
| _ => n;
-fun is_fake_all_name n = (hd (explode n) = "+");
+fun is_fake_all_name n = (hd (raw_explode n) = "+"); (* FIXME Symbol.explode (?) *)
fun mk_fake_all_name n = "+" ^ n;
--- a/src/Tools/WWW_Find/unicode_symbols.ML Fri Nov 19 23:48:07 2010 +0100
+++ b/src/Tools/WWW_Find/unicode_symbols.ML Sat Nov 20 00:53:26 2010 +0100
@@ -82,7 +82,7 @@
-- Scan.many (not o Symbol.is_ascii_blank o Symbol_Pos.symbol)
>> (token AsciiSymbol o op ::);
-fun not_contains xs c = not (member (op =) (explode xs) (Symbol_Pos.symbol c));
+fun not_contains xs c = not (member (op =) (raw_explode xs) (Symbol_Pos.symbol c));
val scan_comment =
$$$ "#" |-- (Scan.many (not_contains "\n") @@@ ($$$ "\n"))
>> token Comment;
--- a/src/Tools/cache_io.ML Fri Nov 19 23:48:07 2010 +0100
+++ b/src/Tools/cache_io.ML Sat Nov 20 00:53:26 2010 +0100
@@ -81,7 +81,7 @@
File.shell_path cache_path)
fun int_of_string s =
- (case read_int (explode s) of
+ (case read_int (raw_explode s) of
(i, []) => i
| _ => err ())