avoid conflict with Alice keywords: renamed pack -> implode, unpack -> explode, any -> many, avoided assert;
--- a/TFL/casesplit.ML Thu Dec 14 22:19:39 2006 +0100
+++ b/TFL/casesplit.ML Fri Dec 15 00:08:06 2006 +0100
@@ -268,7 +268,7 @@
having to (re)search for variables to split. *)
fun splitto splitths genth =
let
- val _ = assert (not (null splitths)) "splitto: no given splitths";
+ val _ = not (null splitths) orelse error "splitto: no given splitths";
val sgn = Thm.sign_of_thm genth;
(* check if we are a member of splitths - FIXME: quicker and
--- a/TFL/rules.ML Thu Dec 14 22:19:39 2006 +0100
+++ b/TFL/rules.ML Fri Dec 15 00:08:06 2006 +0100
@@ -698,9 +698,8 @@
end
fun pq_eliminate (thm,sign,vlist,imp_body,lhs_eq) =
let val ((vstrl, _, used'), args) = dest_pbeta_redex used lhs_eq (length vlist)
- val dummy = assert (forall (op aconv)
- (ListPair.zip (vlist, args)))
- "assertion failed in CONTEXT_REWRITE_RULE"
+ val dummy = forall (op aconv) (ListPair.zip (vlist, args))
+ orelse error "assertion failed in CONTEXT_REWRITE_RULE"
val imp_body1 = subst_free (ListPair.zip (args, vstrl))
imp_body
val tych = cterm_of sign
--- a/src/HOL/Import/hol4rews.ML Thu Dec 14 22:19:39 2006 +0100
+++ b/src/HOL/Import/hol4rews.ML Fri Dec 15 00:08:06 2006 +0100
@@ -584,7 +584,7 @@
if internal
then
let
- val paths = NameSpace.unpack isa
+ val paths = NameSpace.explode isa
val i = Library.drop(length paths - 2,paths)
in
case i of
@@ -638,10 +638,10 @@
fun gen2replay in_thy out_thy s =
let
- val ss = NameSpace.unpack s
+ val ss = NameSpace.explode s
in
if (hd ss = in_thy) then
- NameSpace.pack (out_thy::(tl ss))
+ NameSpace.implode (out_thy::(tl ss))
else
s
end
--- a/src/HOL/Import/importrecorder.ML Thu Dec 14 22:19:39 2006 +0100
+++ b/src/HOL/Import/importrecorder.ML Fri Dec 15 00:08:06 2006 +0100
@@ -188,7 +188,7 @@
fun set_skip_import_dir dir = (history_dir := dir)
fun get_skip_import_dir () = !history_dir
-fun get_filename thyname = Path.pack (Path.append (Path.unpack (the (get_skip_import_dir ()))) (Path.unpack (thyname^".history")))
+fun get_filename thyname = Path.implode (Path.append (Path.explode (the (get_skip_import_dir ()))) (Path.explode (thyname^".history")))
fun save_history thyname =
if get_skip_import () then
@@ -202,7 +202,7 @@
val filename = get_filename thyname
val _ = writeln "load_history / before"
val _ =
- if File.exists (Path.unpack filename) then
+ if File.exists (Path.explode filename) then
(history := XMLConv.read_from_file history_of_xml (get_filename thyname))
else
clear_history ()
--- a/src/HOL/Import/xmlconv.ML Thu Dec 14 22:19:39 2006 +0100
+++ b/src/HOL/Import/xmlconv.ML Fri Dec 15 00:08:06 2006 +0100
@@ -243,12 +243,12 @@
) e
-fun to_file f output fname x = File.write (Path.unpack fname) (f (output x))
+fun to_file f output fname x = File.write (Path.explode fname) (f (output x))
fun from_file f input fname =
let
val _ = writeln "read_from_file enter"
- val s = File.read (Path.unpack fname)
+ val s = File.read (Path.explode fname)
val _ = writeln "done: read file"
val tree = timeit (fn () => f s)
val _ = writeln "done: tree"
--- a/src/HOL/Matrix/cplex/Cplex_tools.ML Thu Dec 14 22:19:39 2006 +0100
+++ b/src/HOL/Matrix/cplex/Cplex_tools.ML Fri Dec 15 00:08:06 2006 +0100
@@ -1136,7 +1136,7 @@
exception Execute of string;
-fun tmp_file s = Path.pack (Path.expand (File.tmp_path (Path.make [s])));
+fun tmp_file s = Path.implode (Path.expand (File.tmp_path (Path.make [s])));
fun wrap s = "\""^s^"\"";
fun solve_glpk prog =
--- a/src/HOL/Nominal/nominal_package.ML Thu Dec 14 22:19:39 2006 +0100
+++ b/src/HOL/Nominal/nominal_package.ML Fri Dec 15 00:08:06 2006 +0100
@@ -733,8 +733,8 @@
(** strips the "_Rep" in type names *)
fun strip_nth_name i s =
- let val xs = NameSpace.unpack s;
- in NameSpace.pack (Library.nth_map (length xs - i) (strip_suffix 4) xs) end;
+ let val xs = NameSpace.explode s;
+ in NameSpace.implode (Library.nth_map (length xs - i) (strip_suffix 4) xs) end;
val (descr'', ndescr) = ListPair.unzip (List.mapPartial
(fn (i, ("Nominal.noption", _, _)) => NONE
--- a/src/HOL/Tools/ATP/AtpCommunication.ML Thu Dec 14 22:19:39 2006 +0100
+++ b/src/HOL/Tools/ATP/AtpCommunication.ML Fri Dec 15 00:08:06 2006 +0100
@@ -128,7 +128,8 @@
(*Return everything in s that comes before the string t*)
fun cut_before t s =
let val (s1,s2) = Substring.position t (Substring.full s)
- val _ = assert (Substring.size s2 <> 0) "cut_before: string not found"
+ val _ = Substring.size s2 <> 0
+ orelse error "cut_before: string not found"
in Substring.string s2 end;
val start_E = "# Proof object starts here."
--- a/src/HOL/Tools/function_package/fundef_lib.ML Thu Dec 14 22:19:39 2006 +0100
+++ b/src/HOL/Tools/function_package/fundef_lib.ML Fri Dec 15 00:08:06 2006 +0100
@@ -54,7 +54,8 @@
val (_, ctx') = ProofContext.add_fixes_i [(n', SOME T, NoSyn)] ctx
val (n'', body) = Term.dest_abs (n', T, b)
- val _ = assert (n' = n'') "dest_all_ctx" (* Note: We assume that n' does not occur in the body. Otherwise it would be fixed. *)
+ val _ = (n' = n'') orelse error "dest_all_ctx"
+ (* Note: We assume that n' does not occur in the body. Otherwise it would be fixed. *)
val (ctx'', vs, bd) = dest_all_all_ctx ctx' body
in
@@ -133,4 +134,4 @@
-end
\ No newline at end of file
+end
--- a/src/HOL/Tools/inductive_realizer.ML Thu Dec 14 22:19:39 2006 +0100
+++ b/src/HOL/Tools/inductive_realizer.ML Fri Dec 15 00:08:06 2006 +0100
@@ -296,12 +296,12 @@
val (_, params) = strip_comb S;
val params' = map dest_Var params;
val rss = [] |> fold add_rule intrs;
- val (prfx, _) = split_last (NameSpace.unpack (fst (hd rss)));
+ val (prfx, _) = split_last (NameSpace.explode (fst (hd rss)));
val tnames = map (fn s => space_implode "_" (s ^ "T" :: vs)) rsets;
val thy1 = thy |>
Theory.root_path |>
- Theory.add_path (NameSpace.pack prfx);
+ Theory.add_path (NameSpace.implode prfx);
val (ty_eqs, rlz_eqs) = split_list
(map (fn (s, rs) => mk_realizes_eqn (not (s mem rsets)) vs rs) rss);
--- a/src/HOL/Tools/record_package.ML Thu Dec 14 22:19:39 2006 +0100
+++ b/src/HOL/Tools/record_package.ML Fri Dec 15 00:08:06 2006 +0100
@@ -439,8 +439,8 @@
fun get_extT_fields thy T =
let
val ((name,Ts),moreT) = dest_recT T;
- val recname = let val (nm::recn::rst) = rev (NameSpace.unpack name)
- in NameSpace.pack (rev (nm::rst)) end;
+ val recname = let val (nm::recn::rst) = rev (NameSpace.explode name)
+ in NameSpace.implode (rev (nm::rst)) end;
val midx = maxidx_of_typs (moreT::Ts);
val varifyT = varifyT midx;
val {records,extfields,...} = RecordsData.get thy;
--- a/src/HOL/Tools/res_atp.ML Thu Dec 14 22:19:39 2006 +0100
+++ b/src/HOL/Tools/res_atp.ML Fri Dec 15 00:08:06 2006 +0100
@@ -99,13 +99,13 @@
"" => error ("Isabelle environment variable " ^ evar ^ " not defined")
| home =>
let val path = home ^ "/" ^ base
- in if File.exists (File.unpack_platform_path path) then path
+ in if File.exists (File.explode_platform_path path) then path
else error ("Could not find the file " ^ path)
end;
fun probfile_nosuffix _ =
if !destdir = "" then File.platform_path (File.tmp_path (Path.basic (!problem_name)))
- else if File.exists (File.unpack_platform_path (!destdir))
+ else if File.exists (File.explode_platform_path (!destdir))
then !destdir ^ "/" ^ !problem_name
else error ("No such directory: " ^ !destdir);
@@ -149,7 +149,7 @@
let val file = !problem_name
in
if !destdir = "" then File.platform_path (File.tmp_path (Path.basic file))
- else if File.exists (File.unpack_platform_path (!destdir))
+ else if File.exists (File.explode_platform_path (!destdir))
then !destdir ^ "/" ^ file
else error ("No such directory: " ^ !destdir)
end;
@@ -463,7 +463,7 @@
(*Reject theorems with names like "List.filter.filter_list_def" or
"Accessible_Part.acc.defs", as these are definitions arising from packages.*)
fun is_package_def a =
- let val names = NameSpace.unpack a
+ let val names = NameSpace.explode a
in
length names > 2 andalso
not (hd names = "local") andalso
@@ -820,7 +820,7 @@
end
fun trace_array fname =
- let val path = File.unpack_platform_path fname
+ let val path = File.explode_platform_path fname
in Array.app (File.append path o (fn s => s ^ "\n")) end;
(*Converting a subgoal into negated conjecture clauses*)
--- a/src/HOL/Tools/res_axioms.ML Thu Dec 14 22:19:39 2006 +0100
+++ b/src/HOL/Tools/res_axioms.ML Fri Dec 15 00:08:06 2006 +0100
@@ -460,7 +460,7 @@
handle THM _ => [];
(*Keep the full complexity of the original name*)
-fun flatten_name s = space_implode "_X" (NameSpace.unpack s);
+fun flatten_name s = space_implode "_X" (NameSpace.explode s);
(*Declare Skolem functions for a theorem, supplied in nnf and with its name.
It returns a modified theory, unless skolemization fails.*)
--- a/src/HOL/Tools/res_clause.ML Thu Dec 14 22:19:39 2006 +0100
+++ b/src/HOL/Tools/res_clause.ML Fri Dec 15 00:08:06 2006 +0100
@@ -745,7 +745,7 @@
val clss = conjectures @ axclauses
val funcs = funcs_of_clauses clss arity_clauses
and preds = preds_of_clauses clss classrel_clauses arity_clauses
- and probname = Path.pack (Path.base (Path.unpack filename))
+ and probname = Path.implode (Path.base (Path.explode filename))
val (axstrs, _) = ListPair.unzip (map clause2dfg axclauses)
val tfree_clss = map dfg_tfree_clause (union_all tfree_litss)
val out = TextIO.openOut filename
--- a/src/HOL/Tools/res_hol_clause.ML Thu Dec 14 22:19:39 2006 +0100
+++ b/src/HOL/Tools/res_hol_clause.ML Fri Dec 15 00:08:06 2006 +0100
@@ -578,7 +578,7 @@
val conjectures = make_conjecture_clauses thms
val (clnames,axclauses') = ListPair.unzip (make_axiom_clauses axclauses)
val (dfg_clss,tfree_litss) = ListPair.unzip (map clause2dfg conjectures)
- and probname = Path.pack (Path.base (Path.unpack filename))
+ and probname = Path.implode (Path.base (Path.explode filename))
val axstrs = map (#1 o clause2dfg) axclauses'
val tfree_clss = map ResClause.dfg_tfree_clause (ResClause.union_all tfree_litss)
val out = TextIO.openOut filename
--- a/src/HOL/Tools/sat_solver.ML Thu Dec 14 22:19:39 2006 +0100
+++ b/src/HOL/Tools/sat_solver.ML Fri Dec 15 00:08:06 2006 +0100
@@ -564,14 +564,14 @@
fun minisat_with_proofs fm =
let
val _ = if (getenv "MINISAT_HOME") = "" then raise SatSolver.NOT_CONFIGURED else ()
- val inpath = File.tmp_path (Path.unpack "isabelle.cnf")
- val outpath = File.tmp_path (Path.unpack "result")
- val proofpath = File.tmp_path (Path.unpack "result.prf")
- val cmd = (getenv "MINISAT_HOME") ^ "/minisat " ^ (Path.pack inpath) ^ " -r " ^ (Path.pack outpath) ^ " -t " ^ (Path.pack proofpath) ^ "> /dev/null"
+ val inpath = File.tmp_path (Path.explode "isabelle.cnf")
+ val outpath = File.tmp_path (Path.explode "result")
+ val proofpath = File.tmp_path (Path.explode "result.prf")
+ val cmd = (getenv "MINISAT_HOME") ^ "/minisat " ^ (Path.implode inpath) ^ " -r " ^ (Path.implode outpath) ^ " -t " ^ (Path.implode proofpath) ^ "> /dev/null"
fun writefn fm = SatSolver.write_dimacs_cnf_file inpath fm
fun readfn () = SatSolver.read_std_result_file outpath ("SAT", "", "UNSAT")
- val _ = if File.exists inpath then warning ("overwriting existing file " ^ quote (Path.pack inpath)) else ()
- val _ = if File.exists outpath then warning ("overwriting existing file " ^ quote (Path.pack outpath)) else ()
+ val _ = if File.exists inpath then warning ("overwriting existing file " ^ quote (Path.implode inpath)) else ()
+ val _ = if File.exists outpath then warning ("overwriting existing file " ^ quote (Path.implode outpath)) else ()
val cnf = PropLogic.defcnf fm
val result = SatSolver.make_external_solver cmd writefn readfn cnf
val _ = try File.rm inpath
@@ -749,13 +749,13 @@
fun minisat fm =
let
val _ = if (getenv "MINISAT_HOME") = "" then raise SatSolver.NOT_CONFIGURED else ()
- val inpath = File.tmp_path (Path.unpack "isabelle.cnf")
- val outpath = File.tmp_path (Path.unpack "result")
- val cmd = (getenv "MINISAT_HOME") ^ "/minisat " ^ (Path.pack inpath) ^ " -r " ^ (Path.pack outpath) ^ " > /dev/null"
+ val inpath = File.tmp_path (Path.explode "isabelle.cnf")
+ val outpath = File.tmp_path (Path.explode "result")
+ val cmd = (getenv "MINISAT_HOME") ^ "/minisat " ^ (Path.implode inpath) ^ " -r " ^ (Path.implode outpath) ^ " > /dev/null"
fun writefn fm = SatSolver.write_dimacs_cnf_file inpath (PropLogic.defcnf fm)
fun readfn () = SatSolver.read_std_result_file outpath ("SAT", "", "UNSAT")
- val _ = if File.exists inpath then warning ("overwriting existing file " ^ quote (Path.pack inpath)) else ()
- val _ = if File.exists outpath then warning ("overwriting existing file " ^ quote (Path.pack outpath)) else ()
+ val _ = if File.exists inpath then warning ("overwriting existing file " ^ quote (Path.implode inpath)) else ()
+ val _ = if File.exists outpath then warning ("overwriting existing file " ^ quote (Path.implode outpath)) else ()
val result = SatSolver.make_external_solver cmd writefn readfn fm
val _ = try File.rm inpath
val _ = try File.rm outpath
@@ -788,7 +788,7 @@
SatSolver.UNSATISFIABLE NONE =>
(let
(* string list *)
- val proof_lines = ((split_lines o File.read) (Path.unpack "resolve_trace"))
+ val proof_lines = ((split_lines o File.read) (Path.explode "resolve_trace"))
handle IO.Io _ => raise INVALID_PROOF "Could not read file \"resolve_trace\""
(* PropLogic.prop_formula -> int *)
fun cnf_number_of_clauses (PropLogic.And (fm1, fm2)) = cnf_number_of_clauses fm1 + cnf_number_of_clauses fm2
@@ -911,13 +911,13 @@
(getenv "ZCHAFF_VERSION") <> "2004.11.15" then raise SatSolver.NOT_CONFIGURED else ()
(* both versions of zChaff appear to have the same interface, so we do *)
(* not actually need to distinguish between them in the following code *)
- val inpath = File.tmp_path (Path.unpack "isabelle.cnf")
- val outpath = File.tmp_path (Path.unpack "result")
- val cmd = (getenv "ZCHAFF_HOME") ^ "/zchaff " ^ (Path.pack inpath) ^ " > " ^ (Path.pack outpath)
+ val inpath = File.tmp_path (Path.explode "isabelle.cnf")
+ val outpath = File.tmp_path (Path.explode "result")
+ val cmd = (getenv "ZCHAFF_HOME") ^ "/zchaff " ^ (Path.implode inpath) ^ " > " ^ (Path.implode outpath)
fun writefn fm = SatSolver.write_dimacs_cnf_file inpath (PropLogic.defcnf fm)
fun readfn () = SatSolver.read_std_result_file outpath ("Instance Satisfiable", "", "Instance Unsatisfiable")
- val _ = if File.exists inpath then warning ("overwriting existing file " ^ quote (Path.pack inpath)) else ()
- val _ = if File.exists outpath then warning ("overwriting existing file " ^ quote (Path.pack outpath)) else ()
+ val _ = if File.exists inpath then warning ("overwriting existing file " ^ quote (Path.implode inpath)) else ()
+ val _ = if File.exists outpath then warning ("overwriting existing file " ^ quote (Path.implode outpath)) else ()
val result = SatSolver.make_external_solver cmd writefn readfn fm
val _ = try File.rm inpath
val _ = try File.rm outpath
@@ -936,13 +936,13 @@
fun berkmin fm =
let
val _ = if (getenv "BERKMIN_HOME") = "" orelse (getenv "BERKMIN_EXE") = "" then raise SatSolver.NOT_CONFIGURED else ()
- val inpath = File.tmp_path (Path.unpack "isabelle.cnf")
- val outpath = File.tmp_path (Path.unpack "result")
- val cmd = (getenv "BERKMIN_HOME") ^ "/" ^ (getenv "BERKMIN_EXE") ^ " " ^ (Path.pack inpath) ^ " > " ^ (Path.pack outpath)
+ val inpath = File.tmp_path (Path.explode "isabelle.cnf")
+ val outpath = File.tmp_path (Path.explode "result")
+ val cmd = (getenv "BERKMIN_HOME") ^ "/" ^ (getenv "BERKMIN_EXE") ^ " " ^ (Path.implode inpath) ^ " > " ^ (Path.implode outpath)
fun writefn fm = SatSolver.write_dimacs_cnf_file inpath (PropLogic.defcnf fm)
fun readfn () = SatSolver.read_std_result_file outpath ("Satisfiable !!", "solution =", "UNSATISFIABLE !!")
- val _ = if File.exists inpath then warning ("overwriting existing file " ^ quote (Path.pack inpath)) else ()
- val _ = if File.exists outpath then warning ("overwriting existing file " ^ quote (Path.pack outpath)) else ()
+ val _ = if File.exists inpath then warning ("overwriting existing file " ^ quote (Path.implode inpath)) else ()
+ val _ = if File.exists outpath then warning ("overwriting existing file " ^ quote (Path.implode outpath)) else ()
val result = SatSolver.make_external_solver cmd writefn readfn fm
val _ = try File.rm inpath
val _ = try File.rm outpath
@@ -961,13 +961,13 @@
fun jerusat fm =
let
val _ = if (getenv "JERUSAT_HOME") = "" then raise SatSolver.NOT_CONFIGURED else ()
- val inpath = File.tmp_path (Path.unpack "isabelle.cnf")
- val outpath = File.tmp_path (Path.unpack "result")
- val cmd = (getenv "JERUSAT_HOME") ^ "/Jerusat1.3 " ^ (Path.pack inpath) ^ " > " ^ (Path.pack outpath)
+ val inpath = File.tmp_path (Path.explode "isabelle.cnf")
+ val outpath = File.tmp_path (Path.explode "result")
+ val cmd = (getenv "JERUSAT_HOME") ^ "/Jerusat1.3 " ^ (Path.implode inpath) ^ " > " ^ (Path.implode outpath)
fun writefn fm = SatSolver.write_dimacs_cnf_file inpath (PropLogic.defcnf fm)
fun readfn () = SatSolver.read_std_result_file outpath ("s SATISFIABLE", "v ", "s UNSATISFIABLE")
- val _ = if File.exists inpath then warning ("overwriting existing file " ^ quote (Path.pack inpath)) else ()
- val _ = if File.exists outpath then warning ("overwriting existing file " ^ quote (Path.pack outpath)) else ()
+ val _ = if File.exists inpath then warning ("overwriting existing file " ^ quote (Path.implode inpath)) else ()
+ val _ = if File.exists outpath then warning ("overwriting existing file " ^ quote (Path.implode outpath)) else ()
val result = SatSolver.make_external_solver cmd writefn readfn fm
val _ = try File.rm inpath
val _ = try File.rm outpath
--- a/src/HOL/Tools/specification_package.ML Thu Dec 14 22:19:39 2006 +0100
+++ b/src/HOL/Tools/specification_package.ML Fri Dec 15 00:08:06 2006 +0100
@@ -128,8 +128,8 @@
fun proc_single prop =
let
val frees = Term.term_frees prop
- val _ = assert (forall (fn v => Sign.of_sort thy (type_of v,HOLogic.typeS)) frees)
- "Specificaton: Only free variables of sort 'type' allowed"
+ val _ = forall (fn v => Sign.of_sort thy (type_of v,HOLogic.typeS)) frees
+ orelse error "Specificaton: Only free variables of sort 'type' allowed"
val prop_closed = foldr (fn ((vname,T),prop) => HOLogic.mk_all (vname,T,prop)) prop (map dest_Free frees)
in
(prop_closed,frees)
@@ -145,8 +145,8 @@
val (altcos,overloaded) = Library.split_list cos
val (names,sconsts) = Library.split_list altcos
val consts = map (term_of o Thm.read_cterm thy o rpair TypeInfer.logicT) sconsts
- val _ = assert (not (Library.exists (not o Term.is_Const) consts))
- "Specification: Non-constant found as parameter"
+ val _ = not (Library.exists (not o Term.is_Const) consts)
+ orelse error "Specification: Non-constant found as parameter"
fun proc_const c =
let
--- a/src/Pure/General/file.ML Thu Dec 14 22:19:39 2006 +0100
+++ b/src/Pure/General/file.ML Fri Dec 15 00:08:06 2006 +0100
@@ -7,8 +7,8 @@
signature FILE =
sig
- val unpack_platform_path_fn: (string -> Path.T) ref
- val unpack_platform_path: string -> Path.T
+ val explode_platform_path_fn: (string -> Path.T) ref
+ val explode_platform_path: string -> Path.T
val platform_path_fn: (Path.T -> string) ref
val platform_path: Path.T -> string
val shell_path_fn: (Path.T -> string) ref
@@ -22,7 +22,7 @@
eqtype info
val info: Path.T -> info option
val exists: Path.T -> bool
- val assert: Path.T -> unit
+ val check: Path.T -> unit
val rm: Path.T -> unit
val mkdir: Path.T -> unit
val read: Path.T -> string
@@ -41,20 +41,20 @@
(* platform specific path representations *)
-val unpack_platform_path_fn = ref Path.unpack;
-fun unpack_platform_path s = ! unpack_platform_path_fn s;
+val explode_platform_path_fn = ref Path.explode;
+fun explode_platform_path s = ! explode_platform_path_fn s;
-val platform_path_fn = ref (Path.pack o Path.expand);
+val platform_path_fn = ref (Path.implode o Path.expand);
fun platform_path path = ! platform_path_fn path;
-val shell_path_fn = ref (enclose "'" "'" o Path.pack o Path.expand);
+val shell_path_fn = ref (enclose "'" "'" o Path.implode o Path.expand);
fun shell_path path = ! shell_path_fn path;
(* current path *)
val cd = Library.cd o platform_path;
-val pwd = unpack_platform_path o Library.pwd;
+val pwd = explode_platform_path o Library.pwd;
fun norm_absolute p =
let
@@ -94,9 +94,9 @@
val exists = is_some o info;
-fun assert path =
+fun check path =
if exists path then ()
- else error ("No such file or directory: " ^ quote (Path.pack path));
+ else error ("No such file or directory: " ^ quote (Path.implode path));
val rm = OS.FileSys.remove o platform_path;
@@ -137,12 +137,12 @@
SOME ids => OS.FileSys.compare ids = EQUAL
| NONE => false);
-fun copy from to = conditional (not (eq (from, to))) (fn () =>
- let val target = if is_dir to then Path.append to (Path.base from) else to
- in write target (read from) end);
+fun copy src dst = conditional (not (eq (src, dst))) (fn () =>
+ let val target = if is_dir dst then Path.append dst (Path.base src) else dst
+ in write target (read src) end);
-fun copy_dir from to = conditional (not (eq (from, to))) (fn () =>
- (system_command ("cp -r -f " ^ shell_path from ^ "/. " ^ shell_path to); ()))
+fun copy_dir src dst = conditional (not (eq (src, dst))) (fn () =>
+ (system_command ("cp -r -f " ^ shell_path src ^ "/. " ^ shell_path dst); ()))
(* use ML files *)
--- a/src/Pure/General/name_space.ML Thu Dec 14 22:19:39 2006 +0100
+++ b/src/Pure/General/name_space.ML Fri Dec 15 00:08:06 2006 +0100
@@ -22,8 +22,8 @@
val hidden: string -> string
val separator: string (*single char*)
val is_qualified: string -> bool
- val pack: string list -> string
- val unpack: string -> string list
+ val implode: string list -> string
+ val explode: string -> string list
val append: string -> string -> string
val qualified: string -> string -> string
val base: string -> string
@@ -70,8 +70,8 @@
val separator = ".";
val is_qualified = exists_string (fn s => s = separator);
-val pack = space_implode separator;
-val unpack = space_explode separator;
+val implode_name = space_implode separator;
+val explode_name = space_explode separator;
fun append name1 "" = name1
| append "" name2 = name2
@@ -82,15 +82,15 @@
else path ^ separator ^ name;
fun base "" = ""
- | base name = List.last (unpack name);
+ | base name = List.last (explode_name name);
fun qualifier "" = ""
- | qualifier name = pack (#1 (split_last (unpack name)));
+ | qualifier name = implode_name (#1 (split_last (explode_name name)));
fun map_base _ "" = ""
| map_base f name =
- let val names = unpack name
- in pack (nth_map (length names - 1) f names) end;
+ let val names = explode_name name
+ in implode_name (nth_map (length names - 1) f names) end;
(* accesses *)
@@ -117,8 +117,8 @@
[xs @ ys] @@ prefixes1 zs @@ [ws];
in sfxs @ pfxs end;
-val accesses = map pack o suffixes_prefixes o unpack;
-val accesses' = map pack o Library.suffixes1 o unpack;
+val accesses = map implode_name o suffixes_prefixes o explode_name;
+val accesses' = map implode_name o Library.suffixes1 o explode_name;
@@ -228,10 +228,10 @@
if is_hidden name then
error ("Attempt to declare hidden name " ^ quote name)
else
- let val names = unpack name in
+ let val names = explode_name name in
conditional (null names orelse exists (fn s => s = "") names) (fn () =>
error ("Bad name declaration " ^ quote name));
- fold (add_name name) (map pack (accs names)) space
+ fold (add_name name) (map implode_name (accs names)) space
end;
@@ -258,7 +258,7 @@
fun sticky_prefix prfx (Naming (path, (qualify, _))) =
Naming (append path prfx,
- (qualify, suffixes_prefixes_split (length (unpack path)) (length (unpack prfx))));
+ (qualify, suffixes_prefixes_split (length (explode_name path)) (length (explode_name prfx))));
fun set_policy policy (Naming (path, _)) = Naming (path, policy);
@@ -284,6 +284,11 @@
fun dest_table tab = map (apfst #1) (ext_table tab);
fun extern_table tab = map (apfst #2) (ext_table tab);
+
+(*final declarations of this structure!*)
+val implode = implode_name;
+val explode = explode_name;
+
end;
structure BasicNameSpace: BASIC_NAME_SPACE = NameSpace;
--- a/src/Pure/General/path.ML Thu Dec 14 22:19:39 2006 +0100
+++ b/src/Pure/General/path.ML Fri Dec 15 00:08:06 2006 +0100
@@ -21,8 +21,8 @@
val append: T -> T -> T
val appends: T list -> T
val make: string list -> T
- val pack: T -> string
- val unpack: string -> T
+ val implode: T -> string
+ val explode: string -> T
val dir: T -> T
val base: T -> T
val ext: string -> T -> T
@@ -95,35 +95,35 @@
fun norm path = rev_app [] path;
-(* pack *)
+(* implode *)
-fun pack_elem Root = ""
- | pack_elem Parent = ".."
- | pack_elem (Basic s) = s
- | pack_elem (Variable s) = "$" ^ s;
+fun implode_elem Root = ""
+ | implode_elem Parent = ".."
+ | implode_elem (Basic s) = s
+ | implode_elem (Variable s) = "$" ^ s;
-fun pack (Path []) = "."
- | pack (Path (Root :: xs)) = "/" ^ space_implode "/" (map pack_elem xs)
- | pack (Path xs) = space_implode "/" (map pack_elem xs);
+fun implode_path (Path []) = "."
+ | implode_path (Path (Root :: xs)) = "/" ^ space_implode "/" (map implode_elem xs)
+ | implode_path (Path xs) = space_implode "/" (map implode_elem xs);
-(* unpack *)
+(* explode *)
-fun unpack_elem "" = Root
- | unpack_elem ".." = Parent
- | unpack_elem "~" = Variable "HOME"
- | unpack_elem "~~" = Variable "ISABELLE_HOME"
- | unpack_elem s =
+fun explode_elem "" = Root
+ | explode_elem ".." = Parent
+ | explode_elem "~" = Variable "HOME"
+ | explode_elem "~~" = Variable "ISABELLE_HOME"
+ | explode_elem s =
(case explode s of
"$" :: cs => variable_elem cs
| cs => basic_elem cs);
-val unpack_elems = map unpack_elem o filter_out (fn c => c = "" orelse c = ".");
+val explode_elems = map explode_elem o filter_out (fn c => c = "" orelse c = ".");
-fun unpack str = Path (norm
+fun explode_path str = Path (norm
(case space_explode "/" str of
- "" :: ss => Root :: unpack_elems ss
- | ss => unpack_elems ss));
+ "" :: ss => Root :: explode_elems ss
+ | ss => explode_elems ss));
(* base element *)
@@ -131,7 +131,7 @@
fun split_path f (path as Path xs) =
(case try split_last xs of
SOME (prfx, Basic s) => f (prfx, s)
- | _ => error ("Cannot split path into dir/base: " ^ quote (pack path)));
+ | _ => error ("Cannot split path into dir/base: " ^ quote (implode_path path)));
val dir = split_path (fn (prfx, _) => Path prfx);
val base = split_path (fn (_, s) => Path [Basic s]);
@@ -150,10 +150,15 @@
fun eval (Variable s) =
(case getenv s of
"" => error ("Undefined Isabelle environment variable: " ^ quote s)
- | path => rep (unpack path))
+ | path => rep (explode_path path))
| eval x = [x];
val expand = rep #> maps eval #> norm #> Path;
-val position = expand #> pack #> quote #> Position.line_name 1;
+val position = expand #> implode_path #> quote #> Position.line_name 1;
+
+
+(*final declarations of this structure!*)
+val implode = implode_path;
+val explode = explode_path;
end;
--- a/src/Pure/General/scan.ML Thu Dec 14 22:19:39 2006 +0100
+++ b/src/Pure/General/scan.ML Fri Dec 15 00:08:06 2006 +0100
@@ -42,8 +42,8 @@
val one: ('a -> bool) -> 'a list -> 'a * 'a list
val this: string list -> string list -> string list * string list
val this_string: string -> string list -> string * string list
- val any: ('a -> bool) -> 'a list -> 'a list * 'a list
- val any1: ('a -> bool) -> 'a list -> 'a list * 'a list
+ val many: ('a -> bool) -> 'a list -> 'a list * 'a list
+ val many1: ('a -> bool) -> 'a list -> 'a list * 'a list
val optional: ('a -> 'b * 'a) -> 'b -> 'a -> 'b * 'a
val option: ('a -> 'b * 'a) -> 'a -> 'b option * 'a
val repeat: ('a -> 'b * 'a) -> 'a -> 'b list * 'a
@@ -143,12 +143,12 @@
fun this_string s = this (explode s) >> K s; (*primitive string -- no symbols here!*)
-fun any _ [] = raise MORE NONE
- | any pred (lst as x :: xs) =
- if pred x then apfst (cons x) (any pred xs)
+fun many _ [] = raise MORE NONE
+ | many pred (lst as x :: xs) =
+ if pred x then apfst (cons x) (many pred xs)
else ([], lst);
-fun any1 pred = one pred -- any pred >> op ::;
+fun many1 pred = one pred -- many pred >> op ::;
fun optional scan def = scan || succeed def;
fun option scan = (scan >> SOME) || succeed NONE;
--- a/src/Pure/General/symbol.ML Thu Dec 14 22:19:39 2006 +0100
+++ b/src/Pure/General/symbol.ML Fri Dec 15 00:08:06 2006 +0100
@@ -403,7 +403,7 @@
(* scan *)
-val scan_id = Scan.one is_letter ^^ (Scan.any is_letdig >> implode);
+val scan_id = Scan.one is_letter ^^ (Scan.many is_letdig >> implode);
local
@@ -413,8 +413,8 @@
$$ "\\" -- Scan.optional ($$ "\\") "" -- Scan.this_string "<^newline>" >> K "\n";
val scan_raw =
- Scan.this_string "raw:" ^^ (Scan.any raw_chr >> implode) ||
- Scan.this_string "raw" ^^ (Scan.any1 is_ascii_digit >> implode);
+ Scan.this_string "raw:" ^^ (Scan.many raw_chr >> implode) ||
+ Scan.this_string "raw" ^^ (Scan.many1 is_ascii_digit >> implode);
in
@@ -431,7 +431,7 @@
(* source *)
val recover =
- Scan.any (fn s => not (is_blank s) andalso s <> "\"" andalso not_eof s) >> K [malformed];
+ Scan.many (fn s => not (is_blank s) andalso s <> "\"" andalso not_eof s) >> K [malformed];
fun source do_recover src =
Source.source stopper (Scan.bulk scan) (if do_recover then SOME recover else NONE) src;
--- a/src/Pure/General/url.ML Thu Dec 14 22:19:39 2006 +0100
+++ b/src/Pure/General/url.ML Fri Dec 15 00:08:06 2006 +0100
@@ -13,8 +13,8 @@
Http of string * Path.T |
Ftp of string * Path.T
val append: T -> T -> T
- val pack: T -> string
- val unpack: string -> T
+ val implode: T -> string
+ val explode: string -> T
end;
structure Url: URL =
@@ -38,26 +38,26 @@
| append _ url = url;
-(* pack *)
+(* implode *)
-fun pack_path p = if Path.is_current p then "" else Path.pack p;
+fun implode_path p = if Path.is_current p then "" else Path.implode p;
-fun pack (File p) = pack_path p
- | pack (RemoteFile (h, p)) = "file://" ^ h ^ pack_path p
- | pack (Http (h, p)) = "http://" ^ h ^ pack_path p
- | pack (Ftp (h, p)) = "ftp://" ^ h ^ pack_path p;
+fun implode_url (File p) = implode_path p
+ | implode_url (RemoteFile (h, p)) = "file://" ^ h ^ implode_path p
+ | implode_url (Http (h, p)) = "http://" ^ h ^ implode_path p
+ | implode_url (Ftp (h, p)) = "ftp://" ^ h ^ implode_path p;
-(* unpack *)
+(* explode *)
local
val scan_host =
- (Scan.any1 (fn s => s <> "/" andalso Symbol.not_eof s) >> implode) --|
+ (Scan.many1 (fn s => s <> "/" andalso Symbol.not_eof s) >> implode) --|
Scan.ahead ($$ "/" || Scan.one Symbol.is_eof);
-val scan_path = Scan.any Symbol.not_eof >> (Path.unpack o implode);
-val scan_path_root = Scan.any Symbol.not_eof >> (Path.unpack o implode o cons "/");
+val scan_path = Scan.many Symbol.not_eof >> (Path.explode o implode);
+val scan_path_root = Scan.many Symbol.not_eof >> (Path.explode o implode o cons "/");
val scan_url =
Scan.unless (Scan.this_string "file:" ||
@@ -71,8 +71,13 @@
in
-fun unpack s = Symbol.scanner "Malformed URL" scan_url (Symbol.explode s);
+fun explode_url s = Symbol.scanner "Malformed URL" scan_url (Symbol.explode s);
end;
+
+(*final declarations of this structure!*)
+val implode = implode_url;
+val explode = explode_url;
+
end;
--- a/src/Pure/General/xml.ML Thu Dec 14 22:19:39 2006 +0100
+++ b/src/Pure/General/xml.ML Fri Dec 15 00:08:06 2006 +0100
@@ -118,7 +118,7 @@
fun err s (xs, _) =
"XML parsing error: " ^ s ^ "\nfound: " ^ quote (Symbol.beginning 100 xs);
-val scan_whspc = Scan.any Symbol.is_blank;
+val scan_whspc = Scan.many Symbol.is_blank;
val scan_special = $$ "&" ^^ Symbol.scan_id ^^ $$ ";" >> decode;
--- a/src/Pure/Isar/isar_cmd.ML Thu Dec 14 22:19:39 2006 +0100
+++ b/src/Pure/Isar/isar_cmd.ML Fri Dec 15 00:08:06 2006 +0100
@@ -192,7 +192,7 @@
(* init and exit *)
fun begin_theory name imports uses =
- ThyInfo.begin_theory Present.begin_theory name imports (map (apfst Path.unpack) uses);
+ ThyInfo.begin_theory Present.begin_theory name imports (map (apfst Path.explode) uses);
fun end_theory thy =
if ThyInfo.check_known_thy (Context.theory_name thy) then ThyInfo.end_theory thy else thy;
@@ -298,7 +298,7 @@
(* current working directory *)
fun cd path = Toplevel.imperative (fn () => (File.cd path));
-val pwd = Toplevel.imperative (fn () => writeln (Path.pack (File.pwd ())));
+val pwd = Toplevel.imperative (fn () => writeln (Path.implode (File.pwd ())));
(* load theory files *)
@@ -496,7 +496,7 @@
(* markup commands *)
fun add_header s = Toplevel.keep' (fn int => fn state =>
- (Toplevel.assert (Toplevel.is_toplevel state);
+ (if Toplevel.is_toplevel state then () else raise Toplevel.UNDEF;
if int then OuterSyntax.check_text s NONE else ()));
local
--- a/src/Pure/Isar/isar_output.ML Thu Dec 14 22:19:39 2006 +0100
+++ b/src/Pure/Isar/isar_output.ML Fri Dec 15 00:08:06 2006 +0100
@@ -305,10 +305,10 @@
local
val space_proper =
- Scan.one T.is_blank -- Scan.any T.is_comment -- Scan.one T.is_proper;
+ Scan.one T.is_blank -- Scan.many T.is_comment -- Scan.one T.is_proper;
val is_improper = not o (T.is_proper orf T.is_begin_ignore orf T.is_end_ignore);
-val improper = Scan.any is_improper;
+val improper = Scan.many is_improper;
val improper_end = Scan.repeat (Scan.unless space_proper (Scan.one is_improper));
val blank_end = Scan.repeat (Scan.unless space_proper (Scan.one T.is_blank));
@@ -375,7 +375,7 @@
val cmd = Scan.one (is_some o fst);
val non_cmd = Scan.one (is_none o fst andf not o #2 stopper) >> #2;
- val comments = Scan.any (comment_token o fst o snd);
+ val comments = Scan.many (comment_token o fst o snd);
val blank = Scan.one (blank_token o fst o snd);
val newline = Scan.one (newline_token o fst o snd);
val before_cmd =
--- a/src/Pure/Isar/outer_lex.ML Thu Dec 14 22:19:39 2006 +0100
+++ b/src/Pure/Isar/outer_lex.ML Fri Dec 15 00:08:06 2006 +0100
@@ -193,7 +193,7 @@
val is_sym_char = member (op =) (explode "!#$%&*+-/<=>?@^_|~");
val scan_symid =
- Scan.any1 is_sym_char >> implode ||
+ Scan.many1 is_sym_char >> implode ||
Scan.one Symbol.is_symbolic;
fun is_symid str =
@@ -249,8 +249,8 @@
fun is_space s = Symbol.is_blank s andalso s <> "\n";
val scan_space =
- (keep_line (Scan.any1 is_space) -- Scan.optional (incr_line ($$ "\n")) "" ||
- keep_line (Scan.any is_space) -- incr_line ($$ "\n")) >> (fn (cs, c) => implode cs ^ c);
+ (keep_line (Scan.many1 is_space) -- Scan.optional (incr_line ($$ "\n")) "" ||
+ keep_line (Scan.many is_space) -- incr_line ($$ "\n")) >> (fn (cs, c) => implode cs ^ c);
(* scan nested comments *)
@@ -303,7 +303,7 @@
(* token sources *)
val is_junk = (not o Symbol.is_blank) andf Symbol.not_sync andf Symbol.not_eof;
-fun recover xs = (keep_line (Scan.any is_junk) >> (fn ts => [malformed_of ts])) xs;
+fun recover xs = (keep_line (Scan.many is_junk) >> (fn ts => [malformed_of ts])) xs;
fun source do_recover get_lex pos src =
Source.source' pos Symbol.stopper (Scan.bulk (fn xs => scan (get_lex ()) xs))
--- a/src/Pure/Isar/outer_parse.ML Thu Dec 14 22:19:39 2006 +0100
+++ b/src/Pure/Isar/outer_parse.ML Fri Dec 15 00:08:06 2006 +0100
@@ -220,7 +220,7 @@
val name = group "name declaration" (short_ident || sym_ident || string || number);
val xname = group "name reference" (short_ident || long_ident || sym_ident || string || number);
val text = group "text" (short_ident || long_ident || sym_ident || string || number || verbatim);
-val path = group "file name/path specification" name >> Path.unpack;
+val path = group "file name/path specification" name >> Path.explode;
val parname = Scan.optional ($$$ "(" |-- name --| $$$ ")") "";
--- a/src/Pure/Isar/outer_syntax.ML Thu Dec 14 22:19:39 2006 +0100
+++ b/src/Pure/Isar/outer_syntax.ML Fri Dec 15 00:08:06 2006 +0100
@@ -253,9 +253,9 @@
val ml_file = if ml andalso is_some (ThyLoad.check_file NONE ml_path) then [ml_path] else [];
in
if name <> name' then
- error ("Filename " ^ quote (Path.pack path) ^
+ error ("Filename " ^ quote (Path.implode path) ^
" does not agree with theory name " ^ quote name')
- else (parents, map (Path.unpack o #1) files @ ml_file)
+ else (parents, map (Path.explode o #1) files @ ml_file)
end;
@@ -268,7 +268,7 @@
if is_none (ThyLoad.check_file NONE path) then ()
else
let
- val _ = warning ("Loading legacy ML script " ^ quote (Path.pack path));
+ val _ = warning ("Loading legacy ML script " ^ quote (Path.implode path));
val tr = Toplevel.imperative (fn () => ThyInfo.load_file time path);
val tr_name = if time then "time_use" else "use";
in Toplevel.excursion [Toplevel.empty |> Toplevel.name tr_name |> tr] end
--- a/src/Pure/Isar/session.ML Thu Dec 14 22:19:39 2006 +0100
+++ b/src/Pure/Isar/session.ML Fri Dec 15 00:08:06 2006 +0100
@@ -71,11 +71,11 @@
if is_some (! remote_path) then
error "Path for remote theory browsing information may only be set once"
else
- remote_path := SOME (Url.unpack rpath);
+ remote_path := SOME (Url.explode rpath);
(! remote_path, rpath <> ""));
fun dumping (_, "") = NONE
- | dumping (cp, path) = SOME (cp, Path.unpack path);
+ | dumping (cp, path) = SOME (cp, Path.explode path);
fun use_dir root build modes reset info doc doc_graph doc_versions
parent name dump rpath level verbose =
--- a/src/Pure/Proof/extraction.ML Thu Dec 14 22:19:39 2006 +0100
+++ b/src/Pure/Proof/extraction.ML Fri Dec 15 00:08:06 2006 +0100
@@ -315,7 +315,7 @@
in fn (thm, (vs, s1, s2)) =>
let
val name = Thm.get_name thm;
- val _ = assert (name <> "") "add_realizers: unnamed theorem";
+ val _ = name <> "" orelse error "add_realizers: unnamed theorem";
val prop = Pattern.rewrite_term thy'
(map (Logic.dest_equals o prop_of) defs) [] (prop_of thm);
val vars = vars_of prop;
@@ -360,7 +360,7 @@
defs, expand, prep} = ExtractionData.get thy;
val name = Thm.get_name thm;
- val _ = assert (name <> "") "add_expand_thms: unnamed theorem";
+ val _ = name <> "" orelse error "add_expand_thms: unnamed theorem";
val is_def =
(case strip_comb (fst (Logic.dest_equals (prop_of thm))) of
@@ -568,7 +568,7 @@
NONE => (case find vs' (find' name defs') of
NONE =>
let
- val _ = assert (T = nullT) "corr: internal error";
+ val _ = T = nullT orelse error "corr: internal error";
val _ = msg d ("Building correctness proof for " ^ quote name ^
(if null vs' then ""
else " (relevant variables: " ^ commas_quote vs' ^ ")"));
@@ -720,8 +720,8 @@
let
val {prop, der = (_, prf), sign, ...} = rep_thm thm;
val name = Thm.get_name thm;
- val _ = assert (name <> "") "extraction: unnamed theorem";
- val _ = assert (etype_of thy' vs [] prop <> nullT) ("theorem " ^
+ val _ = name <> "" orelse error "extraction: unnamed theorem";
+ val _ = etype_of thy' vs [] prop <> nullT orelse error ("theorem " ^
quote name ^ " has no computational content")
in (Reconstruct.reconstruct_proof sign prop prf, vs) end;
--- a/src/Pure/Proof/proof_syntax.ML Thu Dec 14 22:19:39 2006 +0100
+++ b/src/Pure/Proof/proof_syntax.ML Fri Dec 15 00:08:06 2006 +0100
@@ -134,16 +134,16 @@
fun prf_of [] (Bound i) = PBound i
| prf_of Ts (Const (s, Type ("proof", _))) =
change_type (if ty then SOME Ts else NONE)
- (case NameSpace.unpack s of
+ (case NameSpace.explode s of
"axm" :: xs =>
let
- val name = NameSpace.pack xs;
+ val name = NameSpace.implode xs;
val prop = (case AList.lookup (op =) axms name of
SOME prop => prop
| NONE => error ("Unknown axiom " ^ quote name))
in PAxm (name, prop, NONE) end
| "thm" :: xs =>
- let val name = NameSpace.pack xs;
+ let val name = NameSpace.implode xs;
in (case AList.lookup (op =) thms name of
SOME thm => fst (strip_combt (Thm.proof_of thm))
| NONE => (case Symtab.lookup tab name of
--- a/src/Pure/ProofGeneral/pgip_output.ML Thu Dec 14 22:19:39 2006 +0100
+++ b/src/Pure/ProofGeneral/pgip_output.ML Fri Dec 15 00:08:06 2006 +0100
@@ -184,7 +184,7 @@
("version", version),
("instance", instance),
("descr", descr),
- ("url", Url.pack url),
+ ("url", Url.implode url),
("filenameextns", filenameextns)],
[])
end
--- a/src/Pure/ProofGeneral/pgip_types.ML Thu Dec 14 22:19:39 2006 +0100
+++ b/src/Pure/ProofGeneral/pgip_types.ML Fri Dec 15 00:08:06 2006 +0100
@@ -279,7 +279,7 @@
(** Url operations **)
fun pgipurl_of_string url = (* only handle file:/// or file://localhost/ *)
- case Url.unpack url of
+ case Url.explode url of
(Url.File path) => path
| _ => raise PGIP ("Cannot access non-local URL " ^ url)
@@ -291,7 +291,7 @@
val pgipurl_of_attrs = pgipurl_of_string o (get_attr "url")
fun pgipurl_of_url (Url.File p) = p
- | pgipurl_of_url url = raise PGIP ("Cannot access non-local/non-file URL " ^ (Url.pack url))
+ | pgipurl_of_url url = raise PGIP ("Cannot access non-local/non-file URL " ^ (Url.implode url))
(** Messages and errors **)
--- a/src/Pure/ProofGeneral/proof_general_emacs.ML Thu Dec 14 22:19:39 2006 +0100
+++ b/src/Pure/ProofGeneral/proof_general_emacs.ML Fri Dec 15 00:08:06 2006 +0100
@@ -176,7 +176,7 @@
(* prepare theory context *)
-val thy_name = Path.pack o #1 o Path.split_ext o Path.base o Path.unpack;
+val thy_name = Path.implode o #1 o Path.split_ext o Path.base o Path.explode;
(* FIXME general treatment of tracing*)
val update_thy_only = setmp MetaSimplifier.trace_simp false ThyInfo.update_thy_only;
@@ -187,7 +187,7 @@
| NONE => "");
fun try_update_thy_only file =
- ThyLoad.cond_add_path (Path.dir (Path.unpack file)) (fn () =>
+ ThyLoad.cond_add_path (Path.dir (Path.explode file)) (fn () =>
let val name = thy_name file in
if is_some (ThyLoad.check_file NONE (ThyLoad.thy_path name))
then update_thy_only name
@@ -207,13 +207,13 @@
(ThyInfo.touch_child_thys name;
ThyInfo.pretend_use_thy_only name handle ERROR msg =>
(warning msg; warning ("Failed to register theory: " ^ quote name);
- tell_file_retracted (Path.base (Path.unpack file))))
+ tell_file_retracted (Path.base (Path.explode file))))
else raise Toplevel.UNDEF
end;
fun vacuous_inform_file_processed file state =
(warning ("No theory " ^ quote (thy_name file));
- tell_file_retracted (Path.base (Path.unpack file)));
+ tell_file_retracted (Path.base (Path.explode file)));
(* restart top-level loop (keeps most state information) *)
@@ -371,7 +371,7 @@
fun write_keywords s =
(init_outer_syntax ();
- File.write (Path.unpack ("isar-keywords" ^ (if s = "" then "" else "-" ^ s) ^".el"))
+ File.write (Path.explode ("isar-keywords" ^ (if s = "" then "" else "-" ^ s) ^".el"))
(make_elisp_syntax (OuterSyntax.dest_keywords (), OuterSyntax.dest_parsers ())));
end;
--- a/src/Pure/ProofGeneral/proof_general_pgip.ML Thu Dec 14 22:19:39 2006 +0100
+++ b/src/Pure/ProofGeneral/proof_general_pgip.ML Fri Dec 15 00:08:06 2006 +0100
@@ -271,7 +271,7 @@
(* prepare theory context *)
-val thy_name = Path.pack o #1 o Path.split_ext o Path.base o Path.unpack;
+val thy_name = Path.implode o #1 o Path.split_ext o Path.base o Path.explode;
(* FIXME general treatment of tracing*)
val update_thy_only = setmp MetaSimplifier.trace_simp false ThyInfo.update_thy_only;
@@ -282,7 +282,7 @@
| NONE => "");
fun try_update_thy_only file =
- ThyLoad.cond_add_path (Path.dir (Path.unpack file)) (fn () =>
+ ThyLoad.cond_add_path (Path.dir (Path.explode file)) (fn () =>
let val name = thy_name file in
if is_some (ThyLoad.check_file NONE (ThyLoad.thy_path name))
then update_thy_only name
@@ -302,13 +302,13 @@
(ThyInfo.touch_child_thys name;
ThyInfo.pretend_use_thy_only name handle ERROR msg =>
(warning msg; warning ("Failed to register theory: " ^ quote name);
- tell_file_retracted (Path.base (Path.unpack file))))
+ tell_file_retracted (Path.base (Path.explode file))))
else raise Toplevel.UNDEF
end;
fun vacuous_inform_file_processed file state =
(warning ("No theory " ^ quote (thy_name file));
- tell_file_retracted (Path.base (Path.unpack file)));
+ tell_file_retracted (Path.base (Path.explode file)));
(* restart top-level loop (keeps most state information) *)
@@ -387,15 +387,15 @@
in
fun send_pgip_config () =
let
- val path = Path.unpack (config_file())
+ val path = Path.explode (config_file())
val exists = File.exists path
val wwwpage =
- (Url.unpack (isabelle_www()))
+ (Url.explode (isabelle_www()))
handle _ =>
(Output.panic
("Error in URL in environment variable ISABELLE_HOMEPAGE.");
- Url.unpack isabellewww)
+ Url.explode isabellewww)
val proverinfo =
Proverinfo { name = "Isabelle",
@@ -459,11 +459,11 @@
fun use_thy_or_ml_file file =
let
- val (path,extn) = Path.split_ext (Path.unpack file)
+ val (path,extn) = Path.split_ext (Path.explode file)
in
case extn of
- "" => isarcmd ("use_thy " ^ (quote (Path.pack path)))
- | "thy" => isarcmd ("use_thy " ^ (quote (Path.pack path)))
+ "" => isarcmd ("use_thy " ^ (quote (Path.implode path)))
+ | "thy" => isarcmd ("use_thy " ^ (quote (Path.implode path)))
| "ML" => isarcmd ("use " ^ quote file)
| other => error ("Don't know how to read a file with extension " ^ other)
end
--- a/src/Pure/ROOT.ML Thu Dec 14 22:19:39 2006 +0100
+++ b/src/Pure/ROOT.ML Fri Dec 15 00:08:06 2006 +0100
@@ -99,7 +99,7 @@
(*final ML setup*)
use "install_pp.ML";
val use = ThyInfo.use;
-val cd = File.cd o Path.unpack;
+val cd = File.cd o Path.explode;
ml_prompts "ML> " "ML# ";
proofs := 0;
--- a/src/Pure/Syntax/lexicon.ML Thu Dec 14 22:19:39 2006 +0100
+++ b/src/Pure/Syntax/lexicon.ML Fri Dec 15 00:08:06 2006 +0100
@@ -93,10 +93,10 @@
(** basic scanners **)
-val scan_letter_letdigs = Scan.one Symbol.is_letter -- Scan.any Symbol.is_letdig >> op ::;
-val scan_digits1 = Scan.any1 Symbol.is_digit;
-val scan_hex1 = Scan.any1 (Symbol.is_digit orf Symbol.is_hex_letter);
-val scan_bin1 = Scan.any1 (fn s => s = "0" orelse s = "1");
+val scan_letter_letdigs = Scan.one Symbol.is_letter -- Scan.many Symbol.is_letdig >> op ::;
+val scan_digits1 = Scan.many1 Symbol.is_digit;
+val scan_hex1 = Scan.many1 (Symbol.is_digit orf Symbol.is_hex_letter);
+val scan_bin1 = Scan.many1 (fn s => s = "0" orelse s = "1");
val scan_id = scan_letter_letdigs >> implode;
val scan_longid = scan_id ^^ (Scan.repeat1 ($$ "." ^^ scan_id) >> implode);
@@ -344,7 +344,7 @@
let
val scan =
$$ "?" |-- scan_indexname --| Scan.ahead (Scan.one Symbol.is_eof) >> var ||
- Scan.any Symbol.not_eof >> (free o implode);
+ Scan.many Symbol.not_eof >> (free o implode);
in the (Scan.read Symbol.stopper scan (Symbol.explode str)) end;
@@ -388,7 +388,7 @@
val ten = ord "0" + 10;
val a = ord "a";
val A = ord "A";
-val _ = assert (a > A) "Bad ASCII";
+val _ = a > A orelse error "Bad ASCII";
fun remap_hex c =
let val x = ord c in
@@ -421,8 +421,8 @@
fun read_idents str =
let
- val blanks = Scan.any Symbol.is_blank;
- val junk = Scan.any Symbol.not_eof;
+ val blanks = Scan.many Symbol.is_blank;
+ val junk = Scan.many Symbol.not_eof;
val idents = Scan.repeat1 (blanks |-- scan_id --| blanks) -- junk;
in
(case Scan.read Symbol.stopper idents (Symbol.explode str) of
--- a/src/Pure/Syntax/syn_ext.ML Thu Dec 14 22:19:39 2006 +0100
+++ b/src/Pure/Syntax/syn_ext.ML Fri Dec 15 00:08:06 2006 +0100
@@ -203,11 +203,11 @@
val scan_sym =
$$ "_" >> K (Argument ("", 0)) ||
$$ "\\<index>" >> K index ||
- $$ "(" |-- Scan.any Symbol.is_digit >> (Bg o read_int) ||
+ $$ "(" |-- Scan.many Symbol.is_digit >> (Bg o read_int) ||
$$ ")" >> K En ||
$$ "/" -- $$ "/" >> K (Brk ~1) ||
- $$ "/" |-- Scan.any Symbol.is_blank >> (Brk o length) ||
- Scan.any1 Symbol.is_blank >> (Space o implode) ||
+ $$ "/" |-- Scan.many Symbol.is_blank >> (Brk o length) ||
+ Scan.many1 Symbol.is_blank >> (Space o implode) ||
Scan.repeat1 scan_delim_char >> (Delim o implode);
val scan_symb =
--- a/src/Pure/Thy/html.ML Thu Dec 14 22:19:39 2006 +0100
+++ b/src/Pure/Thy/html.ML Fri Dec 15 00:08:06 2006 +0100
@@ -266,13 +266,13 @@
val keyword = enclose "<span class=\"keyword\">" "</span>" o output;
val keyword_width = apfst (enclose "<span class=\"keyword\">" "</span>") o output_width;
val file_name = enclose "<span class=\"filename\">" "</span>" o output;
-val file_path = file_name o Url.pack;
+val file_path = file_name o Url.implode;
(* misc *)
fun href_name s txt = "<a href=" ^ Library.quote s ^ ">" ^ txt ^ "</a>";
-fun href_path path txt = href_name (Url.pack path) txt;
+fun href_path path txt = href_name (Url.implode path) txt;
fun href_opt_name NONE txt = txt
| href_opt_name (SOME s) txt = href_name s txt;
@@ -400,7 +400,7 @@
(* ML file *)
fun ml_file path str =
- begin_document ("File " ^ Url.pack path) ^
+ begin_document ("File " ^ Url.implode path) ^
"\n</div>\n<hr><div class=\"mlsource\">\n" ^
verbatim str ^
"\n</div>\n<hr>\n<div class=\"mlfooter\">\n" ^
--- a/src/Pure/Thy/present.ML Thu Dec 14 22:19:39 2006 +0100
+++ b/src/Pure/Thy/present.ML Fri Dec 15 00:08:06 2006 +0100
@@ -60,15 +60,15 @@
val graph_eps_path = Path.basic "session_graph.eps";
val session_path = Path.basic ".session";
-val session_entries_path = Path.unpack ".session/entries";
-val pre_index_path = Path.unpack ".session/pre-index";
+val session_entries_path = Path.explode ".session/entries";
+val pre_index_path = Path.explode ".session/pre-index";
fun mk_rel_path [] ys = Path.make ys
| mk_rel_path xs [] = Path.appends (replicate (length xs) Path.parent)
| mk_rel_path (ps as x :: xs) (qs as y :: ys) = if x = y then mk_rel_path xs ys else
Path.appends (replicate (length ps) Path.parent @ [Path.make qs]);
-fun show_path path = Path.pack (Path.append (File.pwd ()) path);
+fun show_path path = Path.implode (Path.append (File.pwd ()) path);
@@ -108,7 +108,7 @@
fun display_graph gr =
let
val _ = writeln "Generating graph ...";
- val path = File.tmp_path (Path.unpack "tmp.graph");
+ val path = File.tmp_path (Path.explode "tmp.graph");
val _ = write_graph gr path;
val _ = File.isatool ("browser -c " ^ File.shell_path path ^ " &");
in () end;
@@ -126,9 +126,9 @@
path =
if null session then "" else
if is_some remote_path andalso not is_local then
- Url.pack (Url.append (the remote_path) (Url.File
+ Url.implode (Url.append (the remote_path) (Url.File
(Path.append (Path.make session) (html_path name))))
- else Path.pack (Path.append (mk_rel_path curr_sess session) (html_path name)),
+ else Path.implode (Path.append (mk_rel_path curr_sess session) (html_path name)),
unfold = false,
parents =
map (fn s => ID_of (#session (get_info (ThyInfo.theory s))) s) (ThyInfo.get_preds name)}
@@ -271,7 +271,7 @@
fun update_index dir name =
(case try get_entries dir of
- NONE => warning ("Browser info: cannot access session index of " ^ quote (Path.pack dir))
+ NONE => warning ("Browser info: cannot access session index of " ^ quote (Path.implode dir))
| SOME es => (put_entries ((remove (op =) name es) @ [name]) dir; create_index dir));
@@ -323,7 +323,7 @@
(case readme of NONE => [] | SOME p => [(Url.File p, "README")]) @
map (fn (name, _) => (Url.File (Path.ext doc (Path.basic name)), name)) documents;
val index_text = HTML.begin_index (index_up_lnk, parent_name)
- (Url.File index_path, session_name) docs (Url.unpack "medium.html");
+ (Url.File index_path, session_name) docs (Url.explode "medium.html");
in
session_info := SOME (make_session_info (name, parent_name, session_name, path, html_prefix,
info, doc, doc_graph, documents, doc_prefix1, doc_prefix2, remote_path, verbose, readme));
@@ -407,10 +407,10 @@
if length path > 1 then update_index parent_html_prefix name else ();
(case readme of NONE => () | SOME path => File.copy path html_prefix);
write_graph graph (Path.append html_prefix graph_path);
- File.copy (Path.unpack "~~/lib/browser/GraphBrowser.jar") html_prefix;
+ File.copy (Path.explode "~~/lib/browser/GraphBrowser.jar") html_prefix;
List.app (fn (a, txt) => File.write (Path.append html_prefix (Path.basic a)) txt)
(HTML.applet_pages name (Url.File index_path, name));
- File.copy (Path.unpack "~~/lib/html/isabelle.css") html_prefix;
+ File.copy (Path.explode "~~/lib/html/isabelle.css") html_prefix;
List.app finish_html thys;
List.app (uncurry File.write) files;
conditional verbose (fn () =>
@@ -474,7 +474,7 @@
HTML.ml_file (Url.File base) (File.read path));
(SOME (Url.File base_html), Url.File raw_path, loadit)
end
- | NONE => (warning ("Browser info: expected to find ML file" ^ quote (Path.pack raw_path));
+ | NONE => (warning ("Browser info: expected to find ML file" ^ quote (Path.implode raw_path));
(NONE, Url.File raw_path, loadit)));
val files_html = map prep_file files;
@@ -487,7 +487,7 @@
val entry =
{name = name, ID = ID_of path name, dir = sess_name, unfold = true,
- path = Path.pack (html_path name),
+ path = Path.implode (html_path name),
parents = map (fn s => ID_of (#session (get_info (ThyInfo.theory s))) s) raw_parents};
in
@@ -523,11 +523,11 @@
let
val base = Path.base path;
val name =
- (case Path.pack (#1 (Path.split_ext base)) of "" => gensym "DUMMY" | s => s);
+ (case Path.implode (#1 (Path.split_ext base)) of "" => gensym "DUMMY" | s => s);
in
if File.exists path then
(Buffer.add (Latex.theory_entry name) tex_index, (name, base, File.read path))
- else error ("Bad file: " ^ quote (Path.pack path))
+ else error ("Bad file: " ^ quote (Path.implode path))
end;
val (tex_index, srcs) = foldl_map prep_draft (Buffer.empty, src_paths);
@@ -535,7 +535,7 @@
val result_path = Path.append doc_path Path.parent;
val _ = File.mkdir doc_path;
val root_path = Path.append doc_path (Path.basic "root.tex");
- val _ = File.copy (Path.unpack "~~/lib/texinputs/draft.tex") root_path;
+ val _ = File.copy (Path.explode "~~/lib/texinputs/draft.tex") root_path;
val _ = File.isatool ("latex -o sty " ^ File.shell_path root_path);
val _ = File.isatool ("latex -o syms " ^ File.shell_path root_path);
@@ -547,7 +547,7 @@
val _ = srcs |> List.app (fn (name, base, txt) =>
Symbol.explode txt
- |> Latex.symbol_source (known_syms, known_ctrls) (Path.pack base)
+ |> Latex.symbol_source (known_syms, known_ctrls) (Path.implode base)
|> File.write (Path.append doc_path (tex_path name)));
val _ = write_tex_index tex_index doc_path;
in isatool_document false doc_format documentN "" doc_path result_path end;
--- a/src/Pure/Thy/thm_database.ML Thu Dec 14 22:19:39 2006 +0100
+++ b/src/Pure/Thy/thm_database.ML Fri Dec 15 00:08:06 2006 +0100
@@ -78,7 +78,7 @@
NameSpace.intern space xname = name then
SOME (prfx, (bname, xname, length (the (Symtab.lookup thms name)) = 1))
else NONE;
- val names = NameSpace.unpack name;
+ val names = NameSpace.explode name;
in
(case #2 (chop (length names - 2) names) of
[bname] => result "" bname
--- a/src/Pure/Thy/thm_deps.ML Thu Dec 14 22:19:39 2006 +0100
+++ b/src/Pure/Thy/thm_deps.ML Fri Dec 15 00:08:06 2006 +0100
@@ -43,7 +43,7 @@
if not (Symtab.defined gra name) then
let
val (gra', parents') = make_deps_graph prf' (gra, []);
- val prefx = #1 (Library.split_last (NameSpace.unpack name));
+ val prefx = #1 (Library.split_last (NameSpace.explode name));
val session =
(case prefx of
(x :: _) =>
--- a/src/Pure/Thy/thy_info.ML Thu Dec 14 22:19:39 2006 +0100
+++ b/src/Pure/Thy/thy_info.ML Fri Dec 15 00:08:06 2006 +0100
@@ -256,7 +256,7 @@
fun provide path name info (deps as SOME {present, outdated, master, files}) =
(if exists (equal path o #1) files then ()
else warning (loader_msg "undeclared dependency of theory" [name] ^
- " on file: " ^ quote (Path.pack path));
+ " on file: " ^ quote (Path.implode path));
SOME (make_deps present outdated master (AList.update (op =) (path, SOME info) files)))
| provide _ _ _ NONE = NONE;
@@ -272,7 +272,7 @@
fun load_file time path = Output.toplevel_errors (fn () =>
if time then
- let val name = Path.pack path in
+ let val name = Path.implode path in
timeit (fn () =>
(priority ("\n**** Starting file " ^ quote name ^ " ****");
run_file path;
@@ -280,8 +280,8 @@
end
else run_file path) ();
-val use = load_file false o Path.unpack;
-val time_use = load_file true o Path.unpack;
+val use = load_file false o Path.explode;
+val time_use = load_file true o Path.explode;
end;
@@ -303,7 +303,7 @@
else #1 (ThyLoad.deps_thy dir name ml);
val files = get_files name;
- val missing_files = map_filter (fn (path, NONE) => SOME (Path.pack path) | _ => NONE) files;
+ val missing_files = map_filter (fn (path, NONE) => SOME (Path.implode path) | _ => NONE) files;
in
if null missing_files then ()
else warning (loader_msg "unresolved dependencies of theory" [name] ^
@@ -315,7 +315,7 @@
(* require_thy *)
-fun base_of_path s = Path.pack (Path.base (Path.unpack s));
+fun base_of_path s = Path.implode (Path.base (Path.explode s));
local
@@ -333,7 +333,7 @@
| SOME deps =>
let
fun get_name s = (case opt_path'' (lookup_deps s) of NONE => s
- | SOME p => Path.pack (Path.append p (Path.basic s)));
+ | SOME p => Path.implode (Path.append p (Path.basic s)));
val same_deps = (NONE, map get_name (thy_graph Graph.imm_preds name))
in
(case deps of
@@ -349,8 +349,8 @@
fun require_thy really ml time strict keep_strict initiators prfx (visited, str) =
let
- val path = Path.expand (Path.unpack str);
- val name = Path.pack (Path.base path);
+ val path = Path.expand (Path.explode str);
+ val name = Path.implode (Path.base path);
in
if member (op =) initiators name then error (cycle_msg initiators) else ();
if known_thy name andalso is_finished name orelse member (op =) visited name then
@@ -422,7 +422,7 @@
let val illegal = map (fn ext => Path.ext ext (Path.basic name)) ThyLoad.ml_exts in
(case find_first (member (op =) illegal o Path.base o Path.expand o #1) uses of
NONE => ()
- | SOME (path, _) => error ("Illegal use of theory ML file: " ^ quote (Path.pack path)))
+ | SOME (path, _) => error ("Illegal use of theory ML file: " ^ quote (Path.implode path)))
end;
fun begin_theory present name parents uses int =
--- a/src/Pure/Thy/thy_load.ML Thu Dec 14 22:19:39 2006 +0100
+++ b/src/Pure/Thy/thy_load.ML Fri Dec 15 00:08:06 2006 +0100
@@ -49,12 +49,12 @@
val load_path = ref [Path.current];
fun change_path f = load_path := f (! load_path);
-fun show_path () = map Path.pack (! load_path);
-fun del_path s = change_path (filter_out (equal (Path.unpack s)));
-fun add_path s = (del_path s; change_path (cons (Path.unpack s)));
-fun path_add s = (del_path s; change_path (fn path => path @ [Path.unpack s]));
+fun show_path () = map Path.implode (! load_path);
+fun del_path s = change_path (filter_out (equal (Path.explode s)));
+fun add_path s = (del_path s; change_path (cons (Path.explode s)));
+fun path_add s = (del_path s; change_path (fn path => path @ [Path.explode s]));
fun reset_path () = load_path := [Path.current];
-fun with_paths ss f x = Library.setmp load_path (! load_path @ map Path.unpack ss) f x;
+fun with_paths ss f x = Library.setmp load_path (! load_path @ map Path.explode ss) f x;
fun with_path s f x = with_paths [s] f x;
fun cond_add_path path f x =
@@ -95,7 +95,7 @@
fun load_file current raw_path =
(case check_file current raw_path of
- NONE => error ("Could not find ML file " ^ quote (Path.pack raw_path))
+ NONE => error ("Could not find ML file " ^ quote (Path.implode raw_path))
| SOME (path, info) => (File.use path; (path, info)));
@@ -113,7 +113,7 @@
fun check_thy_aux (name, ml) =
let val thy_file = thy_path name in
case check_file NONE thy_file of
- NONE => error ("Could not find theory file " ^ quote (Path.pack thy_file) ^
+ NONE => error ("Could not find theory file " ^ quote (Path.implode thy_file) ^
" in dir(s) " ^ commas_quote (show_path ()))
| SOME thy_info => (thy_info, if ml then check_file NONE (ml_path name) else NONE)
end;
--- a/src/Pure/Tools/codegen_names.ML Thu Dec 14 22:19:39 2006 +0100
+++ b/src/Pure/Tools/codegen_names.ML Fri Dec 15 00:08:06 2006 +0100
@@ -176,12 +176,12 @@
let
fun is_valid s = Symbol.is_ascii_letter s orelse Symbol.is_ascii_digit s orelse s = "'";
val is_junk = not o is_valid andf Symbol.not_eof;
- val junk = Scan.any is_junk;
+ val junk = Scan.many is_junk;
val scan_valids = Symbol.scanner "Malformed input"
((junk |--
- (Scan.optional (Scan.one Symbol.is_ascii_letter) "x" ^^ (Scan.any is_valid >> implode)
+ (Scan.optional (Scan.one Symbol.is_ascii_letter) "x" ^^ (Scan.many is_valid >> implode)
--| junk))
- -- Scan.repeat ((Scan.any1 is_valid >> implode) --| junk) >> op ::);
+ -- Scan.repeat ((Scan.many1 is_valid >> implode) --| junk) >> op ::);
in explode #> scan_valids #> space_implode "_" end;
fun purify_op "0" = "zero"
@@ -212,11 +212,11 @@
fun check_modulename mn =
let
- val mns = NameSpace.unpack mn;
+ val mns = NameSpace.explode mn;
val mns' = map purify_upper mns;
in
if mns' = mns then mn else error ("Invalid module name: " ^ quote mn ^ "\n"
- ^ "perhaps try " ^ quote (NameSpace.pack mns'))
+ ^ "perhaps try " ^ quote (NameSpace.implode mns'))
end
fun purify_var "" = "x"
@@ -234,9 +234,9 @@
fun policy thy get_basename get_thyname name =
let
- val prefix = (purify_prefix o NameSpace.unpack o get_thyname thy) name;
+ val prefix = (purify_prefix o NameSpace.explode o get_thyname thy) name;
val base = (purify_base o get_basename) name;
- in NameSpace.pack (prefix @ [base]) end;
+ in NameSpace.implode (prefix @ [base]) end;
fun class_policy thy = policy thy NameSpace.base thyname_of_class;
fun tyco_policy thy = policy thy NameSpace.base thyname_of_tyco;
@@ -258,10 +258,10 @@
case force_thyname thy (c, tys)
of NONE => policy thy NameSpace.base thyname_of_const c
| SOME thyname => let
- val prefix = (purify_prefix o NameSpace.unpack) thyname;
+ val prefix = (purify_prefix o NameSpace.explode) thyname;
val tycos = map_filter (fn Type (tyco, _) => SOME tyco | _ => NONE) tys;
val base = map (purify_base o NameSpace.base) (c :: tycos);
- in NameSpace.pack (prefix @ [space_implode "_" base]) end;
+ in NameSpace.implode (prefix @ [space_implode "_" base]) end;
(* shallow name spaces *)
@@ -274,20 +274,20 @@
fun add_nsp shallow name =
name
- |> NameSpace.unpack
+ |> NameSpace.explode
|> split_last
|> apsnd (single #> cons shallow)
|> (op @)
- |> NameSpace.pack;
+ |> NameSpace.implode;
fun dest_nsp nsp nspname =
let
- val xs = NameSpace.unpack nspname;
+ val xs = NameSpace.explode nspname;
val (ys, base) = split_last xs;
val (module, shallow) = split_last ys;
in
if nsp = shallow
- then (SOME o NameSpace.pack) (module @ [base])
+ then (SOME o NameSpace.implode) (module @ [base])
else NONE
end;
--- a/src/Pure/Tools/codegen_serializer.ML Thu Dec 14 22:19:39 2006 +0100
+++ b/src/Pure/Tools/codegen_serializer.ML Fri Dec 15 00:08:06 2006 +0100
@@ -235,7 +235,7 @@
fun dest_name name =
let
- val (names, name_base) = (split_last o NameSpace.unpack) name;
+ val (names, name_base) = (split_last o NameSpace.explode) name;
val (names_mod, name_shallow) = split_last names;
in (names_mod, (name_shallow, name_base)) end;
@@ -257,7 +257,7 @@
fun dictvar v =
first_upper v ^ "_";
val label = translate_string (fn "." => "__" | c => c)
- o NameSpace.pack o op @ o apsnd single o apfst (fst o split_last) o split_last o NameSpace.unpack;
+ o NameSpace.implode o op @ o apsnd single o apfst (fst o split_last) o split_last o NameSpace.explode;
fun pr_tyvar (v, []) =
str "()"
| pr_tyvar (v, sort) =
@@ -584,7 +584,7 @@
fun dictvar v =
first_upper v ^ "_";
val label = translate_string (fn "." => "__" | c => c)
- o NameSpace.pack o op @ o apsnd single o apfst (fst o split_last) o split_last o NameSpace.unpack;
+ o NameSpace.implode o op @ o apsnd single o apfst (fst o split_last) o split_last o NameSpace.explode;
fun pr_tyvar (v, []) =
str "()"
| pr_tyvar (v, sort) =
@@ -924,9 +924,9 @@
val init_vars = CodegenThingol.make_vars (ML_Syntax.reserved_names @ reserved_user);
fun name_modl modl =
let
- val modlname = NameSpace.pack modl
+ val modlname = NameSpace.implode modl
in case module_alias modlname
- of SOME modlname' => NameSpace.unpack modlname'
+ of SOME modlname' => NameSpace.explode modlname'
| NONE => map (fn name => (the_single o fst)
(Name.variants [name] empty_names)) modl
end;
@@ -992,14 +992,14 @@
val (modl'', defname'') = (apfst name_modl o dest_name) name'';
in if modl' = modl'' then
map_node modl'
- (Graph.add_edge (NameSpace.pack (modl @ [fst defname, snd defname]), name''))
+ (Graph.add_edge (NameSpace.implode (modl @ [fst defname, snd defname]), name''))
else let
val (common, (diff1::_, diff2::_)) = chop_prefix (op =) (modl', modl'');
in
map_node common
(fn gr => Graph.add_edge_acyclic (diff1, diff2) gr
handle Graph.CYCLES _ => error ("Dependency "
- ^ quote (NameSpace.pack (modl' @ [fst defname, snd defname]))
+ ^ quote (NameSpace.implode (modl' @ [fst defname, snd defname]))
^ " -> " ^ quote name'' ^ " would result in module dependency cycle"))
end end;
in
@@ -1039,7 +1039,7 @@
|> fold (fn m => fn g => case Graph.get_node g m
of Module (_, (_, g)) => g) modl'
|> (fn g => case Graph.get_node g name of Def (defname, _) => defname);
- in NameSpace.pack (remainder @ [defname']) end handle Graph.UNDEF _ =>
+ in NameSpace.implode (remainder @ [defname']) end handle Graph.UNDEF _ =>
"(raise Fail \"undefined name " ^ name ^ "\")";
fun the_prolog modlname = case module_prolog modlname
of NONE => []
@@ -1049,7 +1049,7 @@
| pr_node prefix (Def (_, SOME def)) =
SOME (pr_def tyco_syntax const_syntax init_vars (deresolver prefix) def)
| pr_node prefix (Module (dmodlname, (_, nodes))) =
- SOME (pr_modl dmodlname (the_prolog (NameSpace.pack (prefix @ [dmodlname]))
+ SOME (pr_modl dmodlname (the_prolog (NameSpace.implode (prefix @ [dmodlname]))
@ separate (str "") ((map_filter (pr_node (prefix @ [dmodlname]) o Graph.get_node nodes)
o rev o flat o Graph.strong_conn) nodes)));
val p = pr_modl "ROOT" (the_prolog "" @ separate (str "") ((map_filter
@@ -1058,7 +1058,7 @@
val isar_seri_sml =
let
- fun output_file file p = File.write (Path.unpack file) (Pretty.output p ^ "\n");
+ fun output_file file p = File.write (Path.explode file) (Pretty.output p ^ "\n");
fun output_diag p = Pretty.writeln p;
fun output_internal p = use_text Output.ml_output false (Pretty.output p);
in
@@ -1070,7 +1070,7 @@
val isar_seri_ocaml =
let
- fun output_file file p = File.write (Path.unpack file) (Pretty.output p ^ "\n");
+ fun output_file file p = File.write (Path.explode file) (Pretty.output p ^ "\n");
fun output_diag p = Pretty.writeln p;
in
parse_args ((Args.$$$ "-" >> K output_diag
@@ -1330,16 +1330,16 @@
fun seri_haskell module_prefix destination string_classes reserved_user module_alias module_prolog
class_syntax tyco_syntax const_syntax code =
let
- val _ = Option.map File.assert destination;
+ val _ = Option.map File.check destination;
val empty_names = Name.make_context (reserved_haskell @ reserved_user);
fun name_modl modl =
let
- val modlname = NameSpace.pack modl
+ val modlname = NameSpace.implode modl
in (modlname, case module_alias modlname
of SOME modlname' => (case module_prefix
of NONE => modlname'
| SOME module_prefix => NameSpace.append module_prefix modlname')
- | NONE => NameSpace.pack (map_filter I (module_prefix :: map (fn name => (SOME o the_single o fst)
+ | NONE => NameSpace.implode (map_filter I (module_prefix :: map (fn name => (SOME o the_single o fst)
(Name.variants [name] empty_names)) modl)))
end;
fun add_def (name, (def, deps)) =
@@ -1409,8 +1409,8 @@
fun write_module (SOME destination) modlname p =
let
val filename = case modlname
- of "" => Path.unpack "Main.hs"
- | _ => (Path.ext "hs" o Path.unpack o implode o separate "/" o NameSpace.unpack) modlname;
+ of "" => Path.explode "Main.hs"
+ | _ => (Path.ext "hs" o Path.explode o implode o separate "/" o NameSpace.explode) modlname;
val pathname = Path.append destination filename;
val _ = File.mkdir (Path.dir pathname);
in File.write pathname (Pretty.setmp_margin 999999 Pretty.output p ^ "\n") end
@@ -1435,7 +1435,7 @@
-- Scan.optional (Args.$$$ "string_classes" >> K true) false
-- (Args.$$$ "-" >> K NONE || Args.name >> SOME)
>> (fn ((module_prefix, string_classes), destination) =>
- seri_haskell module_prefix (Option.map Path.unpack destination) string_classes));
+ seri_haskell module_prefix (Option.map Path.explode destination) string_classes));
(** diagnosis serializer **)
--- a/src/Pure/codegen.ML Thu Dec 14 22:19:39 2006 +0100
+++ b/src/Pure/codegen.ML Fri Dec 15 00:08:06 2006 +0100
@@ -443,7 +443,7 @@
| (true, "isup") => "" :: check_str zs
| (ctrl, s') => (if ctrl then "ctrl_" ^ s' else s') :: check_str zs)
| (ys, zs) => implode ys :: check_str zs);
- val s' = space_implode "_" (maps (check_str o Symbol.explode) (NameSpace.unpack s))
+ val s' = space_implode "_" (maps (check_str o Symbol.explode) (NameSpace.explode s))
in
if Symbol.is_ascii_letter (hd (explode s')) then s' else "id_" ^ s'
end;
@@ -453,7 +453,7 @@
fun find_name [] = sys_error "mk_long_id"
| find_name (ys :: yss) =
let
- val s' = NameSpace.pack ys
+ val s' = NameSpace.implode ys
val s'' = NameSpace.append module s'
in case Symtab.lookup used s'' of
NONE => ((module, s'),
@@ -462,7 +462,7 @@
| SOME _ => find_name yss
end
in case Symtab.lookup tab s of
- NONE => find_name (Library.suffixes1 (NameSpace.unpack s))
+ NONE => find_name (Library.suffixes1 (NameSpace.explode s))
| SOME name => (name, p)
end;
@@ -874,9 +874,9 @@
fun gen_generate_code prep_term thy modules module =
setmp print_mode [] (Pretty.setmp_margin (!margin) (fn xs =>
let
- val _ = assert (module <> "" orelse
+ val _ = (module <> "" orelse
member (op =) (!mode) "library" andalso forall (equal "" o fst) xs)
- "missing module name";
+ orelse error "missing module name";
val graphs = get_modules thy;
val defs = mk_deftab thy;
val gr = new_node ("<Top>", (NONE, module, ""))
@@ -958,10 +958,10 @@
fun test_term thy sz i t =
let
- val _ = assert (null (term_tvars t) andalso null (term_tfrees t))
- "Term to be tested contains type variables";
- val _ = assert (null (term_vars t))
- "Term to be tested contains schematic variables";
+ val _ = (null (term_tvars t) andalso null (term_tfrees t)) orelse
+ error "Term to be tested contains type variables";
+ val _ = null (term_vars t) orelse
+ error "Term to be tested contains schematic variables";
val frees = map dest_Free (term_frees t);
val frees' = frees ~~
map (fn i => "arg" ^ string_of_int i) (1 upto length frees);
@@ -1028,10 +1028,10 @@
fun eval_term thy = setmp print_mode [] (fn t =>
let
- val _ = assert (null (term_tvars t) andalso null (term_tfrees t))
- "Term to be evaluated contains type variables";
- val _ = assert (null (term_vars t) andalso null (term_frees t))
- "Term to be evaluated contains variables";
+ val _ = (null (term_tvars t) andalso null (term_tfrees t)) orelse
+ error "Term to be evaluated contains type variables";
+ val _ = (null (term_vars t) andalso null (term_frees t)) orelse
+ error "Term to be evaluated contains variables";
val (code, gr) = setmp mode ["term_of"]
(generate_code_i thy [] "Generated") [("result", t)];
val s = "structure EvalTerm =\nstruct\n\n" ^
@@ -1155,10 +1155,10 @@
| SOME fname =>
if lib then
app (fn (name, s) => File.write
- (Path.append (Path.unpack fname) (Path.basic (name ^ ".ML"))) s)
+ (Path.append (Path.explode fname) (Path.basic (name ^ ".ML"))) s)
(("ROOT", implode (map (fn (name, _) =>
"use \"" ^ name ^ ".ML\";\n") code)) :: code)
- else File.write (Path.unpack fname) (snd (hd code)));
+ else File.write (Path.explode fname) (snd (hd code)));
if lib then thy
else map_modules (Symtab.update (module, gr)) thy)
end));
--- a/src/Pure/proof_general.ML Thu Dec 14 22:19:39 2006 +0100
+++ b/src/Pure/proof_general.ML Fri Dec 15 00:08:06 2006 +0100
@@ -402,7 +402,7 @@
(* prepare theory context *)
-val thy_name = Path.pack o #1 o Path.split_ext o Path.base o Path.unpack;
+val thy_name = Path.implode o #1 o Path.split_ext o Path.base o Path.explode;
(* FIXME general treatment of tracing*)
val update_thy_only = setmp MetaSimplifier.trace_simp false ThyInfo.update_thy_only;
@@ -413,7 +413,7 @@
| NONE => "");
fun try_update_thy_only file =
- ThyLoad.cond_add_path (Path.dir (Path.unpack file)) (fn () =>
+ ThyLoad.cond_add_path (Path.dir (Path.explode file)) (fn () =>
let val name = thy_name file in
if is_some (ThyLoad.check_file NONE (ThyLoad.thy_path name))
then update_thy_only name
@@ -433,13 +433,13 @@
(ThyInfo.touch_child_thys name;
ThyInfo.pretend_use_thy_only name handle ERROR msg =>
(warning msg; warning ("Failed to register theory: " ^ quote name);
- tell_file_retracted (Path.base (Path.unpack file))))
+ tell_file_retracted (Path.base (Path.explode file))))
else raise Toplevel.UNDEF
end;
fun vacuous_inform_file_processed file state =
(warning ("No theory " ^ quote (thy_name file));
- tell_file_retracted (Path.base (Path.unpack file)));
+ tell_file_retracted (Path.base (Path.explode file)));
(* restart top-level loop (keeps most state information) *)
@@ -653,7 +653,7 @@
in
fun send_pgip_config () =
let
- val path = Path.unpack (config_file())
+ val path = Path.explode (config_file())
val exists = File.exists path
val proverinfo =
XML.element "proverinfo"
@@ -678,7 +678,7 @@
fun send_informguise (openfile, opentheory, openproofpos) =
let val guisefile =
case openfile of SOME f => [XML.element "guisefile"
- [("url",Url.pack (Url.File (Path.unpack f)))] []]
+ [("url",Url.implode (Url.File (Path.explode f)))] []]
| _ => []
val guisetheory =
case opentheory of SOME t => [XML.element "guisetheory" [("thyname", t)] []]
@@ -1172,11 +1172,11 @@
fun use_thy_or_ml_file file =
let
- val (path,extn) = Path.split_ext (Path.unpack file)
+ val (path,extn) = Path.split_ext (Path.explode file)
in
case extn of
- "" => isarcmd ("use_thy " ^ (quote (Path.pack path)))
- | "thy" => isarcmd ("use_thy " ^ (quote (Path.pack path)))
+ "" => isarcmd ("use_thy " ^ (quote (Path.implode path)))
+ | "thy" => isarcmd ("use_thy " ^ (quote (Path.implode path)))
| "ML" => isarcmd ("use " ^ quote file)
| other => error ("Don't know how to read a file with extension " ^ other)
end
@@ -1199,7 +1199,7 @@
val name_attr = xmlattr "name"
fun localfile_of_url url = (* only handle file:/// or file://localhost/ *)
- case Url.unpack url of
+ case Url.explode url of
(Url.File path) => File.platform_path path
| _ => error ("Cannot access non-local URL " ^ url)
@@ -1515,7 +1515,7 @@
fun write_keywords s =
(init_outer_syntax ();
- File.write (Path.unpack ("isar-keywords" ^ (if s = "" then "" else "-" ^ s) ^".el"))
+ File.write (Path.explode ("isar-keywords" ^ (if s = "" then "" else "-" ^ s) ^".el"))
(make_elisp_syntax (OuterSyntax.dest_keywords (), OuterSyntax.dest_parsers ())));
end;
--- a/src/Pure/type.ML Thu Dec 14 22:19:39 2006 +0100
+++ b/src/Pure/type.ML Fri Dec 15 00:08:06 2006 +0100
@@ -535,7 +535,8 @@
fun map_types f = map_tsig (fn (classes, default, types) =>
let
val (space', tab') = f types;
- val _ = assert (NameSpace.intern space' "dummy" = "dummy") "Illegal declaration of dummy type";
+ val _ = NameSpace.intern space' "dummy" = "dummy" orelse
+ error "Illegal declaration of dummy type";
in (classes, default, (space', tab')) end);
fun syntactic types (Type (c, Ts)) =