renamed raw "explode" function to "raw_explode" to emphasize its meaning;
authorwenzelm
Sat Nov 20 00:53:26 2010 +0100 (2010-11-20)
changeset 40627becf5d5187cc
parent 40626 d86540f6ea0d
child 40628 1b1484c3b163
renamed raw "explode" function to "raw_explode" to emphasize its meaning;
NEWS
src/HOL/Boogie/Tools/boogie_commands.ML
src/HOL/Boogie/Tools/boogie_loader.ML
src/HOL/Import/lazy_seq.ML
src/HOL/Import/mono_scan.ML
src/HOL/Import/proof_kernel.ML
src/HOL/Import/scan.ML
src/HOL/Import/seq.ML
src/HOL/Library/Sum_Of_Squares/sum_of_squares.ML
src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML
src/HOL/Nominal/nominal_datatype.ML
src/HOL/Proofs/Lambda/WeakNorm.thy
src/HOL/Tools/ATP/atp_proof.ML
src/HOL/Tools/Datatype/datatype_prop.ML
src/HOL/Tools/Function/size.ML
src/HOL/Tools/Nitpick/kodkod.ML
src/HOL/Tools/Nitpick/nitpick_model.ML
src/HOL/Tools/Nitpick/nitpick_util.ML
src/HOL/Tools/SMT/z3_model.ML
src/HOL/Tools/SMT/z3_proof_parser.ML
src/HOL/Tools/Sledgehammer/sledgehammer.ML
src/HOL/Tools/Sledgehammer/sledgehammer_atp_reconstruct.ML
src/HOL/Tools/Sledgehammer/sledgehammer_util.ML
src/HOL/Tools/hologic.ML
src/HOL/Tools/refute.ML
src/HOL/Tools/string_syntax.ML
src/Pure/General/path.ML
src/Pure/General/scan.ML
src/Pure/General/source.ML
src/Pure/General/symbol.ML
src/Pure/General/xml.ML
src/Pure/Isar/class.ML
src/Pure/Isar/token.ML
src/Pure/ML-Systems/polyml_common.ML
src/Pure/ML-Systems/smlnj.ML
src/Pure/ML/ml_lex.ML
src/Pure/Proof/extraction.ML
src/Pure/codegen.ML
src/Pure/library.ML
src/Pure/name.ML
src/Tools/Code/code_ml.ML
src/Tools/Code/code_printer.ML
src/Tools/IsaPlanner/rw_tools.ML
src/Tools/WWW_Find/unicode_symbols.ML
src/Tools/cache_io.ML
     1.1 --- a/NEWS	Fri Nov 19 23:48:07 2010 +0100
     1.2 +++ b/NEWS	Sat Nov 20 00:53:26 2010 +0100
     1.3 @@ -490,6 +490,10 @@
     1.4  
     1.5  *** ML ***
     1.6  
     1.7 +* Renamed raw "explode" function to "raw_explode" to emphasize its
     1.8 +meaning.  Note that internally to Isabelle, Symbol.explode is used in
     1.9 +almost all situations.
    1.10 +
    1.11  * Discontinued obsolete function sys_error and exception SYS_ERROR.
    1.12  See implementation manual for further details on exceptions in
    1.13  Isabelle/ML.
     2.1 --- a/src/HOL/Boogie/Tools/boogie_commands.ML	Fri Nov 19 23:48:07 2010 +0100
     2.2 +++ b/src/HOL/Boogie/Tools/boogie_commands.ML	Sat Nov 20 00:53:26 2010 +0100
     2.3 @@ -116,7 +116,7 @@
     2.4  end
     2.5  
     2.6  fun write_list head =
     2.7 -  map Pretty.str o sort (dict_ord string_ord o pairself explode) #>
     2.8 +  map Pretty.str o sort (dict_ord string_ord o pairself raw_explode) #>
     2.9    Pretty.writeln o Pretty.big_list head
    2.10  
    2.11  fun parens s = "(" ^ s ^ ")"
     3.1 --- a/src/HOL/Boogie/Tools/boogie_loader.ML	Fri Nov 19 23:48:07 2010 +0100
     3.2 +++ b/src/HOL/Boogie/Tools/boogie_loader.ML	Sat Nov 20 00:53:26 2010 +0100
     3.3 @@ -344,7 +344,7 @@
     3.4      | (_, ts') => error (scan_err "unparsed input" ts'))
     3.5    end
     3.6  
     3.7 -fun read_int' s = (case read_int (explode s) of (i, []) => SOME i | _ => NONE)
     3.8 +fun read_int' s = (case read_int (raw_explode s) of (i, []) => SOME i | _ => NONE)
     3.9  
    3.10  fun $$$ s = Scan.one (fn (_, Token s') => s = s' | _ => false)
    3.11  fun str st = Scan.some (fn (_, Token s) => SOME s | _ => NONE) st
     4.1 --- a/src/HOL/Import/lazy_seq.ML	Fri Nov 19 23:48:07 2010 +0100
     4.2 +++ b/src/HOL/Import/lazy_seq.ML	Sat Nov 20 00:53:26 2010 +0100
     4.3 @@ -543,7 +543,7 @@
     4.4          F e (getItem s)
     4.5      end
     4.6  
     4.7 -fun fromString s = of_list (explode s)
     4.8 +fun fromString s = of_list (raw_explode s)
     4.9  
    4.10  end
    4.11  
     5.1 --- a/src/HOL/Import/mono_scan.ML	Fri Nov 19 23:48:07 2010 +0100
     5.2 +++ b/src/HOL/Import/mono_scan.ML	Sat Nov 20 00:53:26 2010 +0100
     5.3 @@ -233,6 +233,6 @@
     5.4  fun this [] = (fn toks => ([], toks))
     5.5    | this (xs' as (x::xs)) = one (fn y => x=y) -- this xs >> K xs'
     5.6  
     5.7 -fun this_string s = this (explode s) >> K s
     5.8 +fun this_string s = this (raw_explode s) >> K s
     5.9  
    5.10  end
    5.11 \ No newline at end of file
     6.1 --- a/src/HOL/Import/proof_kernel.ML	Fri Nov 19 23:48:07 2010 +0100
     6.2 +++ b/src/HOL/Import/proof_kernel.ML	Sat Nov 20 00:53:26 2010 +0100
     6.3 @@ -501,8 +501,8 @@
     6.4  
     6.5  fun replacestr x y s =
     6.6  let
     6.7 -  val xl = explode x
     6.8 -  val yl = explode y
     6.9 +  val xl = raw_explode x
    6.10 +  val yl = raw_explode y
    6.11    fun isprefix [] ys = true
    6.12      | isprefix (x::xs) (y::ys) = if x = y then isprefix xs ys else false
    6.13      | isprefix _ _ = false
    6.14 @@ -511,7 +511,7 @@
    6.15    fun r [] = []
    6.16      | r (S as (s::ss)) = if isp S then r (chg S) else s::(r ss)
    6.17  in
    6.18 -  implode(r (explode s))
    6.19 +  implode(r (raw_explode s))
    6.20  end
    6.21  
    6.22  fun protect_factname s = replacestr "." "_dot_" s
     7.1 --- a/src/HOL/Import/scan.ML	Fri Nov 19 23:48:07 2010 +0100
     7.2 +++ b/src/HOL/Import/scan.ML	Sat Nov 20 00:53:26 2010 +0100
     7.3 @@ -213,7 +213,7 @@
     7.4  fun this [] = (fn toks => ([], toks))
     7.5    | this (xs' as (x::xs)) = one (fn y => x=y) -- this xs >> K xs'
     7.6  
     7.7 -fun this_string s = this (explode s) >> K s
     7.8 +fun this_string s = this (raw_explode s) >> K s
     7.9  
    7.10  end
    7.11  
     8.1 --- a/src/HOL/Import/seq.ML	Fri Nov 19 23:48:07 2010 +0100
     8.2 +++ b/src/HOL/Import/seq.ML	Sat Nov 20 00:53:26 2010 +0100
     8.3 @@ -94,6 +94,6 @@
     8.4  open Extended
     8.5  
     8.6  val fromList = I
     8.7 -val fromString = explode
     8.8 +val fromString = raw_explode
     8.9  
    8.10  end
     9.1 --- a/src/HOL/Library/Sum_Of_Squares/sum_of_squares.ML	Fri Nov 19 23:48:07 2010 +0100
     9.2 +++ b/src/HOL/Library/Sum_Of_Squares/sum_of_squares.ML	Sat Nov 20 00:53:26 2010 +0100
     9.3 @@ -79,7 +79,7 @@
     9.4     val z = pow10(~ e) */ y +/ rat_1
     9.5     val k = int_of_rat (round_rat(pow10 d */ z))
     9.6    in (if x </ rat_0 then "-0." else "0.") ^
     9.7 -     implode(tl(explode(string_of_int k))) ^
     9.8 +     implode(tl(raw_explode(string_of_int k))) ^
     9.9       (if e = 0 then "" else "e"^string_of_int e)
    9.10    end
    9.11  end;
    9.12 @@ -558,7 +558,7 @@
    9.13      >> (fn (h, x) => h */ pow10 (int_of_rat x));
    9.14  
    9.15   fun mkparser p s =
    9.16 -  let val (x,rst) = p (explode s)
    9.17 +  let val (x,rst) = p (raw_explode s)
    9.18    in if null rst then x
    9.19       else error "mkparser: unparsed input"
    9.20    end;;
    10.1 --- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Fri Nov 19 23:48:07 2010 +0100
    10.2 +++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Sat Nov 20 00:53:26 2010 +0100
    10.3 @@ -444,7 +444,7 @@
    10.4      val (prover_name, _) = get_prover ctxt args
    10.5      val timeout =
    10.6        AList.lookup (op =) args minimize_timeoutK
    10.7 -      |> Option.map (fst o read_int o explode)
    10.8 +      |> Option.map (fst o read_int o raw_explode)  (* FIXME Symbol.explode (?) *)
    10.9        |> the_default 5
   10.10      val params = Sledgehammer_Isar.default_params ctxt
   10.11        [("verbose", "true"),
    11.1 --- a/src/HOL/Nominal/nominal_datatype.ML	Fri Nov 19 23:48:07 2010 +0100
    11.2 +++ b/src/HOL/Nominal/nominal_datatype.ML	Sat Nov 20 00:53:26 2010 +0100
    11.3 @@ -723,7 +723,7 @@
    11.4        | reindex (DtRec i) = DtRec (the (AList.lookup op = ty_idxs i))
    11.5        | reindex dt = dt;
    11.6  
    11.7 -    fun strip_suffix i s = implode (List.take (explode s, size s - i));
    11.8 +    fun strip_suffix i s = implode (List.take (raw_explode s, size s - i));  (* FIXME Symbol.explode (?) *)
    11.9  
   11.10      (** strips the "_Rep" in type names *)
   11.11      fun strip_nth_name i s =
    12.1 --- a/src/HOL/Proofs/Lambda/WeakNorm.thy	Fri Nov 19 23:48:07 2010 +0100
    12.2 +++ b/src/HOL/Proofs/Lambda/WeakNorm.thy	Sat Nov 20 00:53:26 2010 +0100
    12.3 @@ -389,7 +389,7 @@
    12.4  ML {*
    12.5  fun dBtype_of_typ (Type ("fun", [T, U])) =
    12.6        @{code Fun} (dBtype_of_typ T, dBtype_of_typ U)
    12.7 -  | dBtype_of_typ (TFree (s, _)) = (case explode s of
    12.8 +  | dBtype_of_typ (TFree (s, _)) = (case raw_explode s of
    12.9          ["'", a] => @{code Atom} (@{code nat} (ord a - 97))
   12.10        | _ => error "dBtype_of_typ: variable name")
   12.11    | dBtype_of_typ _ = error "dBtype_of_typ: bad type";
   12.12 @@ -458,7 +458,7 @@
   12.13  
   12.14  fun dBtype_of_typ (Type ("fun", [T, U])) =
   12.15        Norm.Fun (dBtype_of_typ T, dBtype_of_typ U)
   12.16 -  | dBtype_of_typ (TFree (s, _)) = (case explode s of
   12.17 +  | dBtype_of_typ (TFree (s, _)) = (case raw_explode s of
   12.18          ["'", a] => Norm.Atom (nat_of_int (ord a - 97))
   12.19        | _ => error "dBtype_of_typ: variable name")
   12.20    | dBtype_of_typ _ = error "dBtype_of_typ: bad type";
    13.1 --- a/src/HOL/Tools/ATP/atp_proof.ML	Fri Nov 19 23:48:07 2010 +0100
    13.2 +++ b/src/HOL/Tools/ATP/atp_proof.ML	Sat Nov 20 00:53:26 2010 +0100
    13.3 @@ -321,7 +321,7 @@
    13.4    fst o Scan.finite Symbol.stopper
    13.5              (Scan.error (!! (fn _ => raise Fail "unrecognized ATP output")
    13.6                              (Scan.repeat1 parse_line)))
    13.7 -  o explode o strip_spaces_except_between_ident_chars
    13.8 +  o raw_explode o strip_spaces_except_between_ident_chars
    13.9  
   13.10  fun clean_up_dependency seen dep = find_first (curry is_same_step dep) seen
   13.11  fun clean_up_dependencies _ [] = []
    14.1 --- a/src/HOL/Tools/Datatype/datatype_prop.ML	Fri Nov 19 23:48:07 2010 +0100
    14.2 +++ b/src/HOL/Tools/Datatype/datatype_prop.ML	Sat Nov 20 00:53:26 2010 +0100
    14.3 @@ -48,7 +48,7 @@
    14.4  
    14.5  fun make_tnames Ts =
    14.6    let
    14.7 -    fun type_name (TFree (name, _)) = implode (tl (explode name))
    14.8 +    fun type_name (TFree (name, _)) = implode (tl (raw_explode name))  (* FIXME Symbol.explode (?) *)
    14.9        | type_name (Type (name, _)) = 
   14.10            let val name' = Long_Name.base_name name
   14.11            in if Syntax.is_identifier name' then name' else "x" end;
    15.1 --- a/src/HOL/Tools/Function/size.ML	Fri Nov 19 23:48:07 2010 +0100
    15.2 +++ b/src/HOL/Tools/Function/size.ML	Sat Nov 20 00:53:26 2010 +0100
    15.3 @@ -71,7 +71,7 @@
    15.4      val ((param_size_fs, param_size_fTs), f_names) = paramTs |>
    15.5        map (fn T as TFree (s, _) =>
    15.6          let
    15.7 -          val name = "f" ^ implode (tl (explode s));
    15.8 +          val name = "f" ^ implode (tl (raw_explode s));  (* FIXME Symbol.explode (?) *)
    15.9            val U = T --> HOLogic.natT
   15.10          in
   15.11            (((s, Free (name, U)), U), name)
    16.1 --- a/src/HOL/Tools/Nitpick/kodkod.ML	Fri Nov 19 23:48:07 2010 +0100
    16.2 +++ b/src/HOL/Tools/Nitpick/kodkod.ML	Sat Nov 20 00:53:26 2010 +0100
    16.3 @@ -908,7 +908,7 @@
    16.4                                  raise SYNTAX ("Kodkod.extract_instance",
    16.5                                                "ill-formed Kodkodi output"))
    16.6                              (parse_instance new_kodkodi)))
    16.7 -  o strip_blanks o explode
    16.8 +  o strip_blanks o raw_explode
    16.9  
   16.10  val problem_marker = "*** PROBLEM "
   16.11  val outcome_marker = "---OUTCOME---\n"
    17.1 --- a/src/HOL/Tools/Nitpick/nitpick_model.ML	Fri Nov 19 23:48:07 2010 +0100
    17.2 +++ b/src/HOL/Tools/Nitpick/nitpick_model.ML	Sat Nov 20 00:53:26 2010 +0100
    17.3 @@ -120,7 +120,7 @@
    17.4    | NONE => (Unsynchronized.change pool (cons (T, [j])); 1)
    17.5  fun atom_suffix s =
    17.6    nat_subscript
    17.7 -  #> (s <> "" andalso Symbol.is_ascii_digit (List.last (explode s)))
    17.8 +  #> (s <> "" andalso Symbol.is_ascii_digit (List.last (raw_explode s)))  (* FIXME Symbol.explode (?) *)
    17.9       ? prefix "\<^isub>,"
   17.10  fun nth_atom_name thy atomss pool prefix T j =
   17.11    let
    18.1 --- a/src/HOL/Tools/Nitpick/nitpick_util.ML	Fri Nov 19 23:48:07 2010 +0100
    18.2 +++ b/src/HOL/Tools/Nitpick/nitpick_util.ML	Sat Nov 20 00:53:26 2010 +0100
    18.3 @@ -240,7 +240,7 @@
    18.4  val parse_time_option = Sledgehammer_Util.parse_time_option
    18.5  val string_from_time = Sledgehammer_Util.string_from_time
    18.6  
    18.7 -val i_subscript = implode o map (prefix "\<^isub>") o explode
    18.8 +val i_subscript = implode o map (prefix "\<^isub>") o raw_explode  (* FIXME Symbol.explode (?) *)
    18.9  fun be_subscript s = "\<^bsub>" ^ s ^ "\<^esub>"
   18.10  fun nat_subscript n =
   18.11    let val s = signed_string_of_int n in
    19.1 --- a/src/HOL/Tools/SMT/z3_model.ML	Fri Nov 19 23:48:07 2010 +0100
    19.2 +++ b/src/HOL/Tools/SMT/z3_model.ML	Sat Nov 20 00:53:26 2010 +0100
    19.3 @@ -38,7 +38,7 @@
    19.4    (fn sign => nat_num >> sign))
    19.5  
    19.6  val is_char = Symbol.is_ascii_letter orf Symbol.is_ascii_digit orf
    19.7 -  member (op =) (explode "_+*-/%~=<>$&|?!.@^#")
    19.8 +  member (op =) (raw_explode "_+*-/%~=<>$&|?!.@^#")
    19.9  val name = spaced (Scan.many1 is_char >> implode)
   19.10  
   19.11  fun $$$ s = spaced (Scan.this_string s)
   19.12 @@ -68,7 +68,7 @@
   19.13    Scan.repeat (name --| $$$ "->" -- (func || expr >> (single o pair [])))
   19.14  
   19.15  fun read_cex ls =
   19.16 -  maps (cons "\n" o explode) ls
   19.17 +  maps (cons "\n" o raw_explode) ls
   19.18    |> try (fst o Scan.finite Symbol.stopper cex)
   19.19    |> the_default []
   19.20  
    20.1 --- a/src/HOL/Tools/SMT/z3_proof_parser.ML	Fri Nov 19 23:48:07 2010 +0100
    20.2 +++ b/src/HOL/Tools/SMT/z3_proof_parser.ML	Sat Nov 20 00:53:26 2010 +0100
    20.3 @@ -256,7 +256,7 @@
    20.4  
    20.5  fun parse_line _ _ (st as ((SOME _, _), _)) = st
    20.6    | parse_line scan line ((_, line_no), cx) =
    20.7 -      let val st = ((line_no, cx), explode line)
    20.8 +      let val st = ((line_no, cx), raw_explode line)
    20.9        in
   20.10          (case Scan.catch (Scan.finite' Symbol.stopper (Scan.option scan)) st of
   20.11            (SOME r, ((_, cx'), _)) => ((r, line_no+1), cx')
   20.12 @@ -299,7 +299,7 @@
   20.13    (fn sign => nat_num >> sign)) st
   20.14  
   20.15  val is_char = Symbol.is_ascii_letter orf Symbol.is_ascii_digit orf
   20.16 -  member (op =) (explode "_+*-/%~=<>$&|?!.@^#")
   20.17 +  member (op =) (raw_explode "_+*-/%~=<>$&|?!.@^#")
   20.18  fun name st = (Scan.lift (Scan.many1 is_char) >> implode) st
   20.19  
   20.20  fun sym st =
    21.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer.ML	Fri Nov 19 23:48:07 2010 +0100
    21.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer.ML	Sat Nov 20 00:53:26 2010 +0100
    21.3 @@ -313,7 +313,7 @@
    21.4          val digit = Scan.one Symbol.is_ascii_digit;
    21.5          val num3 = as_num (digit ::: digit ::: (digit >> single));
    21.6          val time = num --| Scan.$$ "." -- num3 >> (fn (a, b) => a * 1000 + b);
    21.7 -        val as_time = Scan.read Symbol.stopper time o explode
    21.8 +        val as_time = Scan.read Symbol.stopper time o raw_explode
    21.9        in (output, as_time t) end;
   21.10      fun run_on probfile =
   21.11        case filter (curry (op =) "" o getenv o fst) (exec :: required_execs) of
    22.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_atp_reconstruct.ML	Fri Nov 19 23:48:07 2010 +0100
    22.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_atp_reconstruct.ML	Sat Nov 20 00:53:26 2010 +0100
    22.3 @@ -81,7 +81,7 @@
    22.4  val extract_clause_formula_relation =
    22.5    Substring.full #> Substring.position set_ClauseFormulaRelationN
    22.6    #> snd #> Substring.position "." #> fst #> Substring.string
    22.7 -  #> explode #> filter_out Symbol.is_blank #> parse_clause_formula_relation
    22.8 +  #> raw_explode #> filter_out Symbol.is_blank #> parse_clause_formula_relation
    22.9    #> fst
   22.10  
   22.11  fun repair_conjecture_shape_and_fact_names output conjecture_shape fact_names =
    23.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML	Fri Nov 19 23:48:07 2010 +0100
    23.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML	Sat Nov 20 00:53:26 2010 +0100
    23.3 @@ -51,7 +51,7 @@
    23.4           end
    23.5  
    23.6  val has_junk =
    23.7 -  exists (fn s => not (Symbol.is_digit s) andalso s <> ".") o explode
    23.8 +  exists (fn s => not (Symbol.is_digit s) andalso s <> ".") o raw_explode (* FIXME Symbol.explode (?) *)
    23.9  
   23.10  fun parse_time_option _ "none" = NONE
   23.11    | parse_time_option name s =
   23.12 @@ -66,7 +66,7 @@
   23.13  fun string_from_time t =
   23.14    string_of_real (0.01 * Real.fromInt (Time.toMilliseconds t div 10)) ^ " s"
   23.15  
   23.16 -val subscript = implode o map (prefix "\<^isub>") o explode
   23.17 +val subscript = implode o map (prefix "\<^isub>") o raw_explode  (* FIXME Symbol.explode (?) *)
   23.18  fun nat_subscript n =
   23.19    n |> string_of_int |> print_mode_active Symbol.xsymbolsN ? subscript
   23.20  
    24.1 --- a/src/HOL/Tools/hologic.ML	Fri Nov 19 23:48:07 2010 +0100
    24.2 +++ b/src/HOL/Tools/hologic.ML	Sat Nov 20 00:53:26 2010 +0100
    24.3 @@ -598,7 +598,7 @@
    24.4  
    24.5  val stringT = listT charT;
    24.6  
    24.7 -val mk_string = mk_list charT o map (mk_char o ord) o explode;
    24.8 +val mk_string = mk_list charT o map (mk_char o ord) o raw_explode;
    24.9  val dest_string = implode o map (chr o dest_char) o dest_list;
   24.10  
   24.11  
    25.1 --- a/src/HOL/Tools/refute.ML	Fri Nov 19 23:48:07 2010 +0100
    25.2 +++ b/src/HOL/Tools/refute.ML	Sat Nov 20 00:53:26 2010 +0100
    25.3 @@ -2955,7 +2955,7 @@
    25.4      (* string -> string *)
    25.5      fun strip_leading_quote s =
    25.6        (implode o (fn [] => [] | x::xs => if x="'" then xs else x::xs)
    25.7 -        o explode) s
    25.8 +        o raw_explode) s  (* FIXME Symbol.explode (?) *)
    25.9      (* Term.typ -> string *)
   25.10      fun string_of_typ (Type (s, _)) = s
   25.11        | string_of_typ (TFree (x, _)) = strip_leading_quote x
    26.1 --- a/src/HOL/Tools/string_syntax.ML	Fri Nov 19 23:48:07 2010 +0100
    26.2 +++ b/src/HOL/Tools/string_syntax.ML	Sat Nov 20 00:53:26 2010 +0100
    26.3 @@ -32,7 +32,7 @@
    26.4      Syntax.Appl [Syntax.Constant @{const_syntax Char}, mk_nib (ord s div 16), mk_nib (ord s mod 16)]
    26.5    else error ("Non-ASCII symbol: " ^ quote s);
    26.6  
    26.7 -val specials = explode "\\\"`'";
    26.8 +val specials = raw_explode "\\\"`'";
    26.9  
   26.10  fun dest_chr c1 c2 =
   26.11    let val c = chr (dest_nib c1 * 16 + dest_nib c2) in
    27.1 --- a/src/Pure/General/path.ML	Fri Nov 19 23:48:07 2010 +0100
    27.2 +++ b/src/Pure/General/path.ML	Sat Nov 20 00:53:26 2010 +0100
    27.3 @@ -73,9 +73,9 @@
    27.4  
    27.5  val current = Path [];
    27.6  val root = Path [Root ""];
    27.7 -fun named_root s = Path [root_elem (explode s)];
    27.8 -fun basic s = Path [basic_elem (explode s)];
    27.9 -fun variable s = Path [variable_elem (explode s)];
   27.10 +fun named_root s = Path [root_elem (raw_explode s)];
   27.11 +fun basic s = Path [basic_elem (raw_explode s)];
   27.12 +fun variable s = Path [variable_elem (raw_explode s)];
   27.13  val parent = Path [Parent];
   27.14  
   27.15  fun is_absolute (Path xs) =
   27.16 @@ -128,7 +128,7 @@
   27.17    | explode_elem "~" = Variable "HOME"
   27.18    | explode_elem "~~" = Variable "ISABELLE_HOME"
   27.19    | explode_elem s =
   27.20 -      (case explode s of
   27.21 +      (case raw_explode s of
   27.22          "$" :: cs => variable_elem cs
   27.23        | cs => basic_elem cs);
   27.24  
   27.25 @@ -143,7 +143,7 @@
   27.26        (0, es) => ([], es)
   27.27      | (1, es) => ([Root ""], es)
   27.28      | (_, []) => ([Root ""], [])
   27.29 -    | (_, e :: es) => ([root_elem (explode e)], es))
   27.30 +    | (_, e :: es) => ([root_elem (raw_explode e)], es))
   27.31    in Path (norm (explode_elems raw_elems @ roots)) end;
   27.32  
   27.33  end;
   27.34 @@ -161,7 +161,7 @@
   27.35    | ext e = split_path (fn (prfx, s) => append prfx (basic (s ^ "." ^ e)));
   27.36  
   27.37  val split_ext = split_path (fn (prfx, s) => apfst (append prfx)
   27.38 -  (case take_suffix (fn c => c <> ".") (explode s) of
   27.39 +  (case take_suffix (fn c => c <> ".") (raw_explode s) of
   27.40      ([], _) => (Path [Basic s], "")
   27.41    | (cs, e) => (Path [Basic (implode (take (length cs - 1) cs))], implode e)));
   27.42  
    28.1 --- a/src/Pure/General/scan.ML	Fri Nov 19 23:48:07 2010 +0100
    28.2 +++ b/src/Pure/General/scan.ML	Sat Nov 20 00:53:26 2010 +0100
    28.3 @@ -154,7 +154,7 @@
    28.4            if (y: string) = x then drop_prefix ys xs else raise FAIL NONE;
    28.5    in (ys, drop_prefix ys xs) end;
    28.6  
    28.7 -fun this_string s = this (explode s) >> K s;  (*primitive string -- no symbols here!*)
    28.8 +fun this_string s = this (raw_explode s) >> K s;  (*primitive string -- no symbols here!*)
    28.9  
   28.10  fun many _ [] = raise MORE NONE
   28.11    | many pred (lst as x :: xs) =
    29.1 --- a/src/Pure/General/source.ML	Fri Nov 19 23:48:07 2010 +0100
    29.2 +++ b/src/Pure/General/source.ML	Sat Nov 20 00:53:26 2010 +0100
    29.3 @@ -107,7 +107,7 @@
    29.4  
    29.5  (* string source *)
    29.6  
    29.7 -val of_string = of_list o explode;
    29.8 +val of_string = of_list o raw_explode;
    29.9  
   29.10  fun of_string_limited limit str =
   29.11    make_source [] (Substring.full str) default_prompt
   29.12 @@ -127,14 +127,14 @@
   29.13          NONE => []
   29.14        | SOME 0 => []
   29.15        | SOME _ => TextIO.input instream :: slurp ());
   29.16 -  in maps explode (slurp ()) end;
   29.17 +  in maps raw_explode (slurp ()) end;
   29.18  
   29.19  fun tty in_stream = make_source [] () default_prompt (fn prompt => fn () =>
   29.20    let val input = slurp_input in_stream in
   29.21      if exists (fn c => c = "\n") input then (input, ())
   29.22      else
   29.23        (case (Output.prompt prompt; TextIO.inputLine in_stream) of
   29.24 -        SOME line => (input @ explode line, ())
   29.25 +        SOME line => (input @ raw_explode line, ())
   29.26        | NONE => (input, ()))
   29.27    end);
   29.28  
    30.1 --- a/src/Pure/General/symbol.ML	Fri Nov 19 23:48:07 2010 +0100
    30.2 +++ b/src/Pure/General/symbol.ML	Sat Nov 20 00:53:26 2010 +0100
    30.3 @@ -188,7 +188,7 @@
    30.4            | enc ([], d :: ds) = raw2 d :: encode ds
    30.5            | enc (cs, d :: ds) = raw1 cs :: raw2 d :: encode ds;
    30.6        in
    30.7 -        if exists_string (not o raw_chr) str then implode (encode (explode str))
    30.8 +        if exists_string (not o raw_chr) str then implode (encode (raw_explode str))
    30.9          else raw0 str
   30.10        end;
   30.11  
   30.12 @@ -215,7 +215,7 @@
   30.13  fun decode_raw s =
   30.14    if not (is_raw s) then error (malformed_msg s)
   30.15    else if String.isPrefix "\\<^raw:" s then String.substring (s, 7, size s - 8)
   30.16 -  else chr (#1 (Library.read_int (explode (String.substring (s, 6, size s - 7)))));
   30.17 +  else chr (#1 (Library.read_int (raw_explode (String.substring (s, 6, size s - 7)))));
   30.18  
   30.19  
   30.20  (* symbol variants *)
   30.21 @@ -470,7 +470,7 @@
   30.22  in
   30.23  
   30.24  fun sym_explode str =
   30.25 -  let val chs = explode str in
   30.26 +  let val chs = raw_explode str in
   30.27      if no_explode chs then chs
   30.28      else Source.exhaust (source (Source.of_list chs))
   30.29    end;
    31.1 --- a/src/Pure/General/xml.ML	Fri Nov 19 23:48:07 2010 +0100
    31.2 +++ b/src/Pure/General/xml.ML	Sat Nov 20 00:53:26 2010 +0100
    31.3 @@ -158,7 +158,7 @@
    31.4  val parse_comments =
    31.5    blanks -- Scan.repeat (parse_comment -- blanks >> K ()) >> K ();
    31.6  
    31.7 -val parse_string = Scan.read Symbol.stopper parse_chars o explode;
    31.8 +val parse_string = Scan.read Symbol.stopper parse_chars o raw_explode;
    31.9  
   31.10  fun parse_content xs =
   31.11    (parse_optional_text @@@
   31.12 @@ -184,7 +184,7 @@
   31.13  
   31.14  fun parse s =
   31.15    (case Scan.finite Symbol.stopper (Scan.error (!! (err "Malformed element")
   31.16 -      (blanks |-- parse_document --| blanks))) (explode s) of
   31.17 +      (blanks |-- parse_document --| blanks))) (raw_explode s) of
   31.18      (x, []) => x
   31.19    | (_, ys) => error ("XML parsing error: Unprocessed input\n" ^ Symbol.beginning 100 ys));
   31.20  
    32.1 --- a/src/Pure/Isar/class.ML	Fri Nov 19 23:48:07 2010 +0100
    32.2 +++ b/src/Pure/Isar/class.ML	Sat Nov 20 00:53:26 2010 +0100
    32.3 @@ -477,7 +477,7 @@
    32.4          --| junk))
    32.5        ::: Scan.repeat ((Scan.many1 is_valid >> implode) --| junk));
    32.6    in
    32.7 -    explode #> scan_valids #> implode
    32.8 +    raw_explode #> scan_valids #> implode
    32.9    end;
   32.10  
   32.11  val type_name = sanitize_name o Long_Name.base_name;
    33.1 --- a/src/Pure/Isar/token.ML	Fri Nov 19 23:48:07 2010 +0100
    33.2 +++ b/src/Pure/Isar/token.ML	Sat Nov 20 00:53:26 2010 +0100
    33.3 @@ -265,7 +265,7 @@
    33.4  
    33.5  (* scan symbolic idents *)
    33.6  
    33.7 -val is_sym_char = member (op =) (explode "!#$%&*+-/<=>?@^_|~");
    33.8 +val is_sym_char = member (op =) (raw_explode "!#$%&*+-/<=>?@^_|~");
    33.9  
   33.10  val scan_symid =
   33.11    Scan.many1 (is_sym_char o Symbol_Pos.symbol) ||
    34.1 --- a/src/Pure/ML-Systems/polyml_common.ML	Fri Nov 19 23:48:07 2010 +0100
    34.2 +++ b/src/Pure/ML-Systems/polyml_common.ML	Sat Nov 20 00:53:26 2010 +0100
    34.3 @@ -29,6 +29,7 @@
    34.4  val _ = PolyML.Compiler.forgetValue "foldl";
    34.5  val _ = PolyML.Compiler.forgetValue "foldr";
    34.6  val _ = PolyML.Compiler.forgetValue "print";
    34.7 +val _ = PolyML.Compiler.forgetValue "explode";
    34.8  
    34.9  
   34.10  (* Compiler options *)
   34.11 @@ -48,7 +49,7 @@
   34.12  
   34.13  val ord = SML90.ord;
   34.14  val chr = SML90.chr;
   34.15 -val explode = SML90.explode;
   34.16 +val raw_explode = SML90.explode;
   34.17  val implode = SML90.implode;
   34.18  
   34.19  
    35.1 --- a/src/Pure/ML-Systems/smlnj.ML	Fri Nov 19 23:48:07 2010 +0100
    35.2 +++ b/src/Pure/ML-Systems/smlnj.ML	Sat Nov 20 00:53:26 2010 +0100
    35.3 @@ -30,9 +30,9 @@
    35.4  
    35.5  (* restore old-style character / string functions *)
    35.6  
    35.7 -val ord     = mk_int o SML90.ord;
    35.8 -val chr     = SML90.chr o dest_int;
    35.9 -val explode = SML90.explode;
   35.10 +val ord = mk_int o SML90.ord;
   35.11 +val chr = SML90.chr o dest_int;
   35.12 +val raw_explode = SML90.explode;
   35.13  val implode = SML90.implode;
   35.14  
   35.15  
    36.1 --- a/src/Pure/ML/ml_lex.ML	Fri Nov 19 23:48:07 2010 +0100
    36.2 +++ b/src/Pure/ML/ml_lex.ML	Sat Nov 20 00:53:26 2010 +0100
    36.3 @@ -149,7 +149,7 @@
    36.4    "sharing", "sig", "signature", "struct", "structure", "then", "type",
    36.5    "val", "where", "while", "with", "withtype"];
    36.6  
    36.7 -val lex = Scan.make_lexicon (map explode keywords);
    36.8 +val lex = Scan.make_lexicon (map raw_explode keywords);
    36.9  fun scan_keyword x = Scan.literal lex x;
   36.10  
   36.11  
   36.12 @@ -166,7 +166,7 @@
   36.13    Scan.one (Symbol.is_ascii_letter o Symbol_Pos.symbol) -- scan_letdigs >> op ::;
   36.14  
   36.15  val scan_symbolic =
   36.16 -  Scan.many1 (member (op =) (explode "!#$%&*+-/:<=>?@\\^`|~") o Symbol_Pos.symbol);
   36.17 +  Scan.many1 (member (op =) (raw_explode "!#$%&*+-/:<=>?@\\^`|~") o Symbol_Pos.symbol);
   36.18  
   36.19  in
   36.20  
   36.21 @@ -211,7 +211,7 @@
   36.22  local
   36.23  
   36.24  val scan_escape =
   36.25 -  Scan.one (member (op =) (explode "\"\\abtnvfr") o Symbol_Pos.symbol) >> single ||
   36.26 +  Scan.one (member (op =) (raw_explode "\"\\abtnvfr") o Symbol_Pos.symbol) >> single ||
   36.27    $$$ "^" @@@ (Scan.one (fn (s, _) => ord "@" <= ord s andalso ord s <= ord "_") >> single) ||
   36.28    Scan.one (Symbol.is_ascii_digit o Symbol_Pos.symbol) --
   36.29      Scan.one (Symbol.is_ascii_digit o Symbol_Pos.symbol) --
    37.1 --- a/src/Pure/Proof/extraction.ML	Fri Nov 19 23:48:07 2010 +0100
    37.2 +++ b/src/Pure/Proof/extraction.ML	Sat Nov 20 00:53:26 2010 +0100
    37.3 @@ -68,7 +68,7 @@
    37.4    | rlz_proc _ = NONE;
    37.5  
    37.6  val unpack_ixn = apfst implode o apsnd (fst o read_int o tl) o
    37.7 -  take_prefix (fn s => s <> ":") o explode;
    37.8 +  take_prefix (fn s => s <> ":") o raw_explode;
    37.9  
   37.10  type rules =
   37.11    {next: int, rs: ((term * term) list * (term * term)) list,
    38.1 --- a/src/Pure/codegen.ML	Fri Nov 19 23:48:07 2010 +0100
    38.2 +++ b/src/Pure/codegen.ML	Sat Nov 20 00:53:26 2010 +0100
    38.3 @@ -355,7 +355,7 @@
    38.4    Symbol.is_ascii_digit x orelse Symbol.is_ascii_quasi x;
    38.5  
    38.6  fun dest_sym s =
    38.7 -  (case split_last (snd (take_prefix (fn c => c = "\\") (explode s))) of
    38.8 +  (case split_last (snd (take_prefix (fn c => c = "\\") (raw_explode s))) of
    38.9      ("<" :: "^" :: xs, ">") => (true, implode xs)
   38.10    | ("<" :: xs, ">") => (false, implode xs)
   38.11    | _ => raise Fail "dest_sym");
   38.12 @@ -374,7 +374,7 @@
   38.13          | (ys, zs) => implode ys :: check_str zs);
   38.14      val s' = space_implode "_" (maps (check_str o Symbol.explode) (Long_Name.explode s))
   38.15    in
   38.16 -    if Symbol.is_ascii_letter (hd (explode s')) then s' else "id_" ^ s'
   38.17 +    if Symbol.is_ascii_letter (hd (raw_explode s')) then s' else "id_" ^ s'
   38.18    end;
   38.19  
   38.20  fun mk_long_id (p as (tab, used)) module s =
   38.21 @@ -826,7 +826,7 @@
   38.22  
   38.23  (**** Reflection ****)
   38.24  
   38.25 -val strip_tname = implode o tl o explode;
   38.26 +val strip_tname = implode o tl o raw_explode;
   38.27  
   38.28  fun pretty_list xs = Pretty.block (str "[" ::
   38.29    flat (separate [str ",", Pretty.brk 1] (map single xs)) @
   38.30 @@ -962,7 +962,7 @@
   38.31  val _ = List.app Keyword.keyword ["attach", "file", "contains"];
   38.32  
   38.33  fun strip_whitespace s = implode (fst (take_suffix (fn c => c = "\n" orelse c = " ")
   38.34 -  (snd (take_prefix (fn c => c = "\n" orelse c = " ") (explode s))))) ^ "\n";
   38.35 +  (snd (take_prefix (fn c => c = "\n" orelse c = " ") (raw_explode s))))) ^ "\n";
   38.36  
   38.37  val parse_attach = Scan.repeat (Parse.$$$ "attach" |--
   38.38    Scan.optional (Parse.$$$ "(" |-- Parse.xname --| Parse.$$$ ")") "" --
    39.1 --- a/src/Pure/library.ML	Fri Nov 19 23:48:07 2010 +0100
    39.2 +++ b/src/Pure/library.ML	Sat Nov 20 00:53:26 2010 +0100
    39.3 @@ -669,7 +669,7 @@
    39.4  
    39.5  val read_int = read_radix_int 10;
    39.6  
    39.7 -fun oct_char s = chr (#1 (read_radix_int 8 (explode s)));
    39.8 +fun oct_char s = chr (#1 (read_radix_int 8 (raw_explode s)));
    39.9  
   39.10  
   39.11  
    40.1 --- a/src/Pure/name.ML	Fri Nov 19 23:48:07 2010 +0100
    40.2 +++ b/src/Pure/name.ML	Sat Nov 20 00:53:26 2010 +0100
    40.3 @@ -166,7 +166,7 @@
    40.4            if is_valid x then x :: xs
    40.5            else
    40.6              (case Symbol.decode x of
    40.7 -              Symbol.Sym name => "_" :: explode name @ sep xs
    40.8 +              Symbol.Sym name => "_" :: raw_explode name @ sep xs
    40.9              | _ => sep xs);
   40.10          fun upper_lower cs =
   40.11            if upper then nth_map 0 Symbol.to_ascii_upper cs
    41.1 --- a/src/Tools/Code/code_ml.ML	Fri Nov 19 23:48:07 2010 +0100
    41.2 +++ b/src/Tools/Code/code_ml.ML	Sat Nov 20 00:53:26 2010 +0100
    41.3 @@ -679,7 +679,7 @@
    41.4    fun chr i =
    41.5      let
    41.6        val xs = string_of_int i;
    41.7 -      val ys = replicate_string (3 - length (explode xs)) "0";
    41.8 +      val ys = replicate_string (3 - length (raw_explode xs)) "0";
    41.9      in "\\" ^ ys ^ xs end;
   41.10    fun char_ocaml c =
   41.11      let
    42.1 --- a/src/Tools/Code/code_printer.ML	Fri Nov 19 23:48:07 2010 +0100
    42.2 +++ b/src/Tools/Code/code_printer.ML	Sat Nov 20 00:53:26 2010 +0100
    42.3 @@ -173,8 +173,8 @@
    42.4   of SOME name' => name'
    42.5    | NONE => error ("Invalid name in context: " ^ quote name);
    42.6  
    42.7 -val first_upper = implode o nth_map 0 Symbol.to_ascii_upper o explode;
    42.8 -val first_lower = implode o nth_map 0 Symbol.to_ascii_lower o explode;
    42.9 +val first_upper = implode o nth_map 0 Symbol.to_ascii_upper o raw_explode;
   42.10 +val first_lower = implode o nth_map 0 Symbol.to_ascii_lower o raw_explode;
   42.11  
   42.12  fun aux_params vars lhss =
   42.13    let
    43.1 --- a/src/Tools/IsaPlanner/rw_tools.ML	Fri Nov 19 23:48:07 2010 +0100
    43.2 +++ b/src/Tools/IsaPlanner/rw_tools.ML	Sat Nov 20 00:53:26 2010 +0100
    43.3 @@ -20,10 +20,10 @@
    43.4  construction/definition. *)
    43.5  (*
    43.6  fun dest_fake_bound_name n = 
    43.7 -    case (explode n) of 
    43.8 +    case (raw_explode n) of   (* FIXME Symbol.explode (?) *)
    43.9        (":" :: realchars) => implode realchars
   43.10      | _ => n; *)
   43.11 -fun is_fake_bound_name n = (hd (explode n) = ":");
   43.12 +fun is_fake_bound_name n = (hd (raw_explode n) = ":");  (* FIXME Symbol.explode (?) *)
   43.13  fun mk_fake_bound_name n = ":b_" ^ n;
   43.14  
   43.15  
   43.16 @@ -31,20 +31,20 @@
   43.17  (* fake free variable names for local meta variables - these work
   43.18  as placeholders. *)
   43.19  fun dest_fake_fix_name n = 
   43.20 -    case (explode n) of 
   43.21 +    case (raw_explode n) of  (* FIXME Symbol.explode (?) *)
   43.22        ("@" :: realchars) => implode realchars
   43.23      | _ => n;
   43.24 -fun is_fake_fix_name n = (hd (explode n) = "@");
   43.25 +fun is_fake_fix_name n = (hd (raw_explode n) = "@");  (* FIXME Symbol.explode (?) *)
   43.26  fun mk_fake_fix_name n = "@" ^ n;
   43.27  
   43.28  
   43.29  
   43.30  (* fake free variable names for meta level bound variables *)
   43.31  fun dest_fake_all_name n = 
   43.32 -    case (explode n) of 
   43.33 +    case (raw_explode n) of   (* FIXME Symbol.explode (?) *)
   43.34        ("+" :: realchars) => implode realchars
   43.35      | _ => n;
   43.36 -fun is_fake_all_name n = (hd (explode n) = "+");
   43.37 +fun is_fake_all_name n = (hd (raw_explode n) = "+");  (* FIXME Symbol.explode (?) *)
   43.38  fun mk_fake_all_name n = "+" ^ n;
   43.39  
   43.40  
    44.1 --- a/src/Tools/WWW_Find/unicode_symbols.ML	Fri Nov 19 23:48:07 2010 +0100
    44.2 +++ b/src/Tools/WWW_Find/unicode_symbols.ML	Sat Nov 20 00:53:26 2010 +0100
    44.3 @@ -82,7 +82,7 @@
    44.4    -- Scan.many (not o Symbol.is_ascii_blank o Symbol_Pos.symbol)
    44.5    >> (token AsciiSymbol o op ::);
    44.6  
    44.7 -fun not_contains xs c = not (member (op =) (explode xs) (Symbol_Pos.symbol c));
    44.8 +fun not_contains xs c = not (member (op =) (raw_explode xs) (Symbol_Pos.symbol c));
    44.9  val scan_comment =
   44.10    $$$ "#" |-- (Scan.many (not_contains "\n") @@@ ($$$ "\n"))
   44.11    >> token Comment;
    45.1 --- a/src/Tools/cache_io.ML	Fri Nov 19 23:48:07 2010 +0100
    45.2 +++ b/src/Tools/cache_io.ML	Sat Nov 20 00:53:26 2010 +0100
    45.3 @@ -81,7 +81,7 @@
    45.4        File.shell_path cache_path)
    45.5  
    45.6      fun int_of_string s =
    45.7 -      (case read_int (explode s) of
    45.8 +      (case read_int (raw_explode s) of
    45.9          (i, []) => i
   45.10        | _ => err ())    
   45.11