avoid conflict with Alice keywords: renamed pack -> implode, unpack -> explode, any -> many, avoided assert;
1.1 --- a/TFL/casesplit.ML Thu Dec 14 22:19:39 2006 +0100
1.2 +++ b/TFL/casesplit.ML Fri Dec 15 00:08:06 2006 +0100
1.3 @@ -268,7 +268,7 @@
1.4 having to (re)search for variables to split. *)
1.5 fun splitto splitths genth =
1.6 let
1.7 - val _ = assert (not (null splitths)) "splitto: no given splitths";
1.8 + val _ = not (null splitths) orelse error "splitto: no given splitths";
1.9 val sgn = Thm.sign_of_thm genth;
1.10
1.11 (* check if we are a member of splitths - FIXME: quicker and
2.1 --- a/TFL/rules.ML Thu Dec 14 22:19:39 2006 +0100
2.2 +++ b/TFL/rules.ML Fri Dec 15 00:08:06 2006 +0100
2.3 @@ -698,9 +698,8 @@
2.4 end
2.5 fun pq_eliminate (thm,sign,vlist,imp_body,lhs_eq) =
2.6 let val ((vstrl, _, used'), args) = dest_pbeta_redex used lhs_eq (length vlist)
2.7 - val dummy = assert (forall (op aconv)
2.8 - (ListPair.zip (vlist, args)))
2.9 - "assertion failed in CONTEXT_REWRITE_RULE"
2.10 + val dummy = forall (op aconv) (ListPair.zip (vlist, args))
2.11 + orelse error "assertion failed in CONTEXT_REWRITE_RULE"
2.12 val imp_body1 = subst_free (ListPair.zip (args, vstrl))
2.13 imp_body
2.14 val tych = cterm_of sign
3.1 --- a/src/HOL/Import/hol4rews.ML Thu Dec 14 22:19:39 2006 +0100
3.2 +++ b/src/HOL/Import/hol4rews.ML Fri Dec 15 00:08:06 2006 +0100
3.3 @@ -584,7 +584,7 @@
3.4 if internal
3.5 then
3.6 let
3.7 - val paths = NameSpace.unpack isa
3.8 + val paths = NameSpace.explode isa
3.9 val i = Library.drop(length paths - 2,paths)
3.10 in
3.11 case i of
3.12 @@ -638,10 +638,10 @@
3.13
3.14 fun gen2replay in_thy out_thy s =
3.15 let
3.16 - val ss = NameSpace.unpack s
3.17 + val ss = NameSpace.explode s
3.18 in
3.19 if (hd ss = in_thy) then
3.20 - NameSpace.pack (out_thy::(tl ss))
3.21 + NameSpace.implode (out_thy::(tl ss))
3.22 else
3.23 s
3.24 end
4.1 --- a/src/HOL/Import/importrecorder.ML Thu Dec 14 22:19:39 2006 +0100
4.2 +++ b/src/HOL/Import/importrecorder.ML Fri Dec 15 00:08:06 2006 +0100
4.3 @@ -188,7 +188,7 @@
4.4 fun set_skip_import_dir dir = (history_dir := dir)
4.5 fun get_skip_import_dir () = !history_dir
4.6
4.7 -fun get_filename thyname = Path.pack (Path.append (Path.unpack (the (get_skip_import_dir ()))) (Path.unpack (thyname^".history")))
4.8 +fun get_filename thyname = Path.implode (Path.append (Path.explode (the (get_skip_import_dir ()))) (Path.explode (thyname^".history")))
4.9
4.10 fun save_history thyname =
4.11 if get_skip_import () then
4.12 @@ -202,7 +202,7 @@
4.13 val filename = get_filename thyname
4.14 val _ = writeln "load_history / before"
4.15 val _ =
4.16 - if File.exists (Path.unpack filename) then
4.17 + if File.exists (Path.explode filename) then
4.18 (history := XMLConv.read_from_file history_of_xml (get_filename thyname))
4.19 else
4.20 clear_history ()
5.1 --- a/src/HOL/Import/xmlconv.ML Thu Dec 14 22:19:39 2006 +0100
5.2 +++ b/src/HOL/Import/xmlconv.ML Fri Dec 15 00:08:06 2006 +0100
5.3 @@ -243,12 +243,12 @@
5.4 ) e
5.5
5.6
5.7 -fun to_file f output fname x = File.write (Path.unpack fname) (f (output x))
5.8 +fun to_file f output fname x = File.write (Path.explode fname) (f (output x))
5.9
5.10 fun from_file f input fname =
5.11 let
5.12 val _ = writeln "read_from_file enter"
5.13 - val s = File.read (Path.unpack fname)
5.14 + val s = File.read (Path.explode fname)
5.15 val _ = writeln "done: read file"
5.16 val tree = timeit (fn () => f s)
5.17 val _ = writeln "done: tree"
6.1 --- a/src/HOL/Matrix/cplex/Cplex_tools.ML Thu Dec 14 22:19:39 2006 +0100
6.2 +++ b/src/HOL/Matrix/cplex/Cplex_tools.ML Fri Dec 15 00:08:06 2006 +0100
6.3 @@ -1136,7 +1136,7 @@
6.4
6.5 exception Execute of string;
6.6
6.7 -fun tmp_file s = Path.pack (Path.expand (File.tmp_path (Path.make [s])));
6.8 +fun tmp_file s = Path.implode (Path.expand (File.tmp_path (Path.make [s])));
6.9 fun wrap s = "\""^s^"\"";
6.10
6.11 fun solve_glpk prog =
7.1 --- a/src/HOL/Nominal/nominal_package.ML Thu Dec 14 22:19:39 2006 +0100
7.2 +++ b/src/HOL/Nominal/nominal_package.ML Fri Dec 15 00:08:06 2006 +0100
7.3 @@ -733,8 +733,8 @@
7.4
7.5 (** strips the "_Rep" in type names *)
7.6 fun strip_nth_name i s =
7.7 - let val xs = NameSpace.unpack s;
7.8 - in NameSpace.pack (Library.nth_map (length xs - i) (strip_suffix 4) xs) end;
7.9 + let val xs = NameSpace.explode s;
7.10 + in NameSpace.implode (Library.nth_map (length xs - i) (strip_suffix 4) xs) end;
7.11
7.12 val (descr'', ndescr) = ListPair.unzip (List.mapPartial
7.13 (fn (i, ("Nominal.noption", _, _)) => NONE
8.1 --- a/src/HOL/Tools/ATP/AtpCommunication.ML Thu Dec 14 22:19:39 2006 +0100
8.2 +++ b/src/HOL/Tools/ATP/AtpCommunication.ML Fri Dec 15 00:08:06 2006 +0100
8.3 @@ -128,7 +128,8 @@
8.4 (*Return everything in s that comes before the string t*)
8.5 fun cut_before t s =
8.6 let val (s1,s2) = Substring.position t (Substring.full s)
8.7 - val _ = assert (Substring.size s2 <> 0) "cut_before: string not found"
8.8 + val _ = Substring.size s2 <> 0
8.9 + orelse error "cut_before: string not found"
8.10 in Substring.string s2 end;
8.11
8.12 val start_E = "# Proof object starts here."
9.1 --- a/src/HOL/Tools/function_package/fundef_lib.ML Thu Dec 14 22:19:39 2006 +0100
9.2 +++ b/src/HOL/Tools/function_package/fundef_lib.ML Fri Dec 15 00:08:06 2006 +0100
9.3 @@ -54,7 +54,8 @@
9.4 val (_, ctx') = ProofContext.add_fixes_i [(n', SOME T, NoSyn)] ctx
9.5
9.6 val (n'', body) = Term.dest_abs (n', T, b)
9.7 - val _ = assert (n' = n'') "dest_all_ctx" (* Note: We assume that n' does not occur in the body. Otherwise it would be fixed. *)
9.8 + val _ = (n' = n'') orelse error "dest_all_ctx"
9.9 + (* Note: We assume that n' does not occur in the body. Otherwise it would be fixed. *)
9.10
9.11 val (ctx'', vs, bd) = dest_all_all_ctx ctx' body
9.12 in
9.13 @@ -133,4 +134,4 @@
9.14
9.15
9.16
9.17 -end
9.18 \ No newline at end of file
9.19 +end
10.1 --- a/src/HOL/Tools/inductive_realizer.ML Thu Dec 14 22:19:39 2006 +0100
10.2 +++ b/src/HOL/Tools/inductive_realizer.ML Fri Dec 15 00:08:06 2006 +0100
10.3 @@ -296,12 +296,12 @@
10.4 val (_, params) = strip_comb S;
10.5 val params' = map dest_Var params;
10.6 val rss = [] |> fold add_rule intrs;
10.7 - val (prfx, _) = split_last (NameSpace.unpack (fst (hd rss)));
10.8 + val (prfx, _) = split_last (NameSpace.explode (fst (hd rss)));
10.9 val tnames = map (fn s => space_implode "_" (s ^ "T" :: vs)) rsets;
10.10
10.11 val thy1 = thy |>
10.12 Theory.root_path |>
10.13 - Theory.add_path (NameSpace.pack prfx);
10.14 + Theory.add_path (NameSpace.implode prfx);
10.15 val (ty_eqs, rlz_eqs) = split_list
10.16 (map (fn (s, rs) => mk_realizes_eqn (not (s mem rsets)) vs rs) rss);
10.17
11.1 --- a/src/HOL/Tools/record_package.ML Thu Dec 14 22:19:39 2006 +0100
11.2 +++ b/src/HOL/Tools/record_package.ML Fri Dec 15 00:08:06 2006 +0100
11.3 @@ -439,8 +439,8 @@
11.4 fun get_extT_fields thy T =
11.5 let
11.6 val ((name,Ts),moreT) = dest_recT T;
11.7 - val recname = let val (nm::recn::rst) = rev (NameSpace.unpack name)
11.8 - in NameSpace.pack (rev (nm::rst)) end;
11.9 + val recname = let val (nm::recn::rst) = rev (NameSpace.explode name)
11.10 + in NameSpace.implode (rev (nm::rst)) end;
11.11 val midx = maxidx_of_typs (moreT::Ts);
11.12 val varifyT = varifyT midx;
11.13 val {records,extfields,...} = RecordsData.get thy;
12.1 --- a/src/HOL/Tools/res_atp.ML Thu Dec 14 22:19:39 2006 +0100
12.2 +++ b/src/HOL/Tools/res_atp.ML Fri Dec 15 00:08:06 2006 +0100
12.3 @@ -99,13 +99,13 @@
12.4 "" => error ("Isabelle environment variable " ^ evar ^ " not defined")
12.5 | home =>
12.6 let val path = home ^ "/" ^ base
12.7 - in if File.exists (File.unpack_platform_path path) then path
12.8 + in if File.exists (File.explode_platform_path path) then path
12.9 else error ("Could not find the file " ^ path)
12.10 end;
12.11
12.12 fun probfile_nosuffix _ =
12.13 if !destdir = "" then File.platform_path (File.tmp_path (Path.basic (!problem_name)))
12.14 - else if File.exists (File.unpack_platform_path (!destdir))
12.15 + else if File.exists (File.explode_platform_path (!destdir))
12.16 then !destdir ^ "/" ^ !problem_name
12.17 else error ("No such directory: " ^ !destdir);
12.18
12.19 @@ -149,7 +149,7 @@
12.20 let val file = !problem_name
12.21 in
12.22 if !destdir = "" then File.platform_path (File.tmp_path (Path.basic file))
12.23 - else if File.exists (File.unpack_platform_path (!destdir))
12.24 + else if File.exists (File.explode_platform_path (!destdir))
12.25 then !destdir ^ "/" ^ file
12.26 else error ("No such directory: " ^ !destdir)
12.27 end;
12.28 @@ -463,7 +463,7 @@
12.29 (*Reject theorems with names like "List.filter.filter_list_def" or
12.30 "Accessible_Part.acc.defs", as these are definitions arising from packages.*)
12.31 fun is_package_def a =
12.32 - let val names = NameSpace.unpack a
12.33 + let val names = NameSpace.explode a
12.34 in
12.35 length names > 2 andalso
12.36 not (hd names = "local") andalso
12.37 @@ -820,7 +820,7 @@
12.38 end
12.39
12.40 fun trace_array fname =
12.41 - let val path = File.unpack_platform_path fname
12.42 + let val path = File.explode_platform_path fname
12.43 in Array.app (File.append path o (fn s => s ^ "\n")) end;
12.44
12.45 (*Converting a subgoal into negated conjecture clauses*)
13.1 --- a/src/HOL/Tools/res_axioms.ML Thu Dec 14 22:19:39 2006 +0100
13.2 +++ b/src/HOL/Tools/res_axioms.ML Fri Dec 15 00:08:06 2006 +0100
13.3 @@ -460,7 +460,7 @@
13.4 handle THM _ => [];
13.5
13.6 (*Keep the full complexity of the original name*)
13.7 -fun flatten_name s = space_implode "_X" (NameSpace.unpack s);
13.8 +fun flatten_name s = space_implode "_X" (NameSpace.explode s);
13.9
13.10 (*Declare Skolem functions for a theorem, supplied in nnf and with its name.
13.11 It returns a modified theory, unless skolemization fails.*)
14.1 --- a/src/HOL/Tools/res_clause.ML Thu Dec 14 22:19:39 2006 +0100
14.2 +++ b/src/HOL/Tools/res_clause.ML Fri Dec 15 00:08:06 2006 +0100
14.3 @@ -745,7 +745,7 @@
14.4 val clss = conjectures @ axclauses
14.5 val funcs = funcs_of_clauses clss arity_clauses
14.6 and preds = preds_of_clauses clss classrel_clauses arity_clauses
14.7 - and probname = Path.pack (Path.base (Path.unpack filename))
14.8 + and probname = Path.implode (Path.base (Path.explode filename))
14.9 val (axstrs, _) = ListPair.unzip (map clause2dfg axclauses)
14.10 val tfree_clss = map dfg_tfree_clause (union_all tfree_litss)
14.11 val out = TextIO.openOut filename
15.1 --- a/src/HOL/Tools/res_hol_clause.ML Thu Dec 14 22:19:39 2006 +0100
15.2 +++ b/src/HOL/Tools/res_hol_clause.ML Fri Dec 15 00:08:06 2006 +0100
15.3 @@ -578,7 +578,7 @@
15.4 val conjectures = make_conjecture_clauses thms
15.5 val (clnames,axclauses') = ListPair.unzip (make_axiom_clauses axclauses)
15.6 val (dfg_clss,tfree_litss) = ListPair.unzip (map clause2dfg conjectures)
15.7 - and probname = Path.pack (Path.base (Path.unpack filename))
15.8 + and probname = Path.implode (Path.base (Path.explode filename))
15.9 val axstrs = map (#1 o clause2dfg) axclauses'
15.10 val tfree_clss = map ResClause.dfg_tfree_clause (ResClause.union_all tfree_litss)
15.11 val out = TextIO.openOut filename
16.1 --- a/src/HOL/Tools/sat_solver.ML Thu Dec 14 22:19:39 2006 +0100
16.2 +++ b/src/HOL/Tools/sat_solver.ML Fri Dec 15 00:08:06 2006 +0100
16.3 @@ -564,14 +564,14 @@
16.4 fun minisat_with_proofs fm =
16.5 let
16.6 val _ = if (getenv "MINISAT_HOME") = "" then raise SatSolver.NOT_CONFIGURED else ()
16.7 - val inpath = File.tmp_path (Path.unpack "isabelle.cnf")
16.8 - val outpath = File.tmp_path (Path.unpack "result")
16.9 - val proofpath = File.tmp_path (Path.unpack "result.prf")
16.10 - val cmd = (getenv "MINISAT_HOME") ^ "/minisat " ^ (Path.pack inpath) ^ " -r " ^ (Path.pack outpath) ^ " -t " ^ (Path.pack proofpath) ^ "> /dev/null"
16.11 + val inpath = File.tmp_path (Path.explode "isabelle.cnf")
16.12 + val outpath = File.tmp_path (Path.explode "result")
16.13 + val proofpath = File.tmp_path (Path.explode "result.prf")
16.14 + val cmd = (getenv "MINISAT_HOME") ^ "/minisat " ^ (Path.implode inpath) ^ " -r " ^ (Path.implode outpath) ^ " -t " ^ (Path.implode proofpath) ^ "> /dev/null"
16.15 fun writefn fm = SatSolver.write_dimacs_cnf_file inpath fm
16.16 fun readfn () = SatSolver.read_std_result_file outpath ("SAT", "", "UNSAT")
16.17 - val _ = if File.exists inpath then warning ("overwriting existing file " ^ quote (Path.pack inpath)) else ()
16.18 - val _ = if File.exists outpath then warning ("overwriting existing file " ^ quote (Path.pack outpath)) else ()
16.19 + val _ = if File.exists inpath then warning ("overwriting existing file " ^ quote (Path.implode inpath)) else ()
16.20 + val _ = if File.exists outpath then warning ("overwriting existing file " ^ quote (Path.implode outpath)) else ()
16.21 val cnf = PropLogic.defcnf fm
16.22 val result = SatSolver.make_external_solver cmd writefn readfn cnf
16.23 val _ = try File.rm inpath
16.24 @@ -749,13 +749,13 @@
16.25 fun minisat fm =
16.26 let
16.27 val _ = if (getenv "MINISAT_HOME") = "" then raise SatSolver.NOT_CONFIGURED else ()
16.28 - val inpath = File.tmp_path (Path.unpack "isabelle.cnf")
16.29 - val outpath = File.tmp_path (Path.unpack "result")
16.30 - val cmd = (getenv "MINISAT_HOME") ^ "/minisat " ^ (Path.pack inpath) ^ " -r " ^ (Path.pack outpath) ^ " > /dev/null"
16.31 + val inpath = File.tmp_path (Path.explode "isabelle.cnf")
16.32 + val outpath = File.tmp_path (Path.explode "result")
16.33 + val cmd = (getenv "MINISAT_HOME") ^ "/minisat " ^ (Path.implode inpath) ^ " -r " ^ (Path.implode outpath) ^ " > /dev/null"
16.34 fun writefn fm = SatSolver.write_dimacs_cnf_file inpath (PropLogic.defcnf fm)
16.35 fun readfn () = SatSolver.read_std_result_file outpath ("SAT", "", "UNSAT")
16.36 - val _ = if File.exists inpath then warning ("overwriting existing file " ^ quote (Path.pack inpath)) else ()
16.37 - val _ = if File.exists outpath then warning ("overwriting existing file " ^ quote (Path.pack outpath)) else ()
16.38 + val _ = if File.exists inpath then warning ("overwriting existing file " ^ quote (Path.implode inpath)) else ()
16.39 + val _ = if File.exists outpath then warning ("overwriting existing file " ^ quote (Path.implode outpath)) else ()
16.40 val result = SatSolver.make_external_solver cmd writefn readfn fm
16.41 val _ = try File.rm inpath
16.42 val _ = try File.rm outpath
16.43 @@ -788,7 +788,7 @@
16.44 SatSolver.UNSATISFIABLE NONE =>
16.45 (let
16.46 (* string list *)
16.47 - val proof_lines = ((split_lines o File.read) (Path.unpack "resolve_trace"))
16.48 + val proof_lines = ((split_lines o File.read) (Path.explode "resolve_trace"))
16.49 handle IO.Io _ => raise INVALID_PROOF "Could not read file \"resolve_trace\""
16.50 (* PropLogic.prop_formula -> int *)
16.51 fun cnf_number_of_clauses (PropLogic.And (fm1, fm2)) = cnf_number_of_clauses fm1 + cnf_number_of_clauses fm2
16.52 @@ -911,13 +911,13 @@
16.53 (getenv "ZCHAFF_VERSION") <> "2004.11.15" then raise SatSolver.NOT_CONFIGURED else ()
16.54 (* both versions of zChaff appear to have the same interface, so we do *)
16.55 (* not actually need to distinguish between them in the following code *)
16.56 - val inpath = File.tmp_path (Path.unpack "isabelle.cnf")
16.57 - val outpath = File.tmp_path (Path.unpack "result")
16.58 - val cmd = (getenv "ZCHAFF_HOME") ^ "/zchaff " ^ (Path.pack inpath) ^ " > " ^ (Path.pack outpath)
16.59 + val inpath = File.tmp_path (Path.explode "isabelle.cnf")
16.60 + val outpath = File.tmp_path (Path.explode "result")
16.61 + val cmd = (getenv "ZCHAFF_HOME") ^ "/zchaff " ^ (Path.implode inpath) ^ " > " ^ (Path.implode outpath)
16.62 fun writefn fm = SatSolver.write_dimacs_cnf_file inpath (PropLogic.defcnf fm)
16.63 fun readfn () = SatSolver.read_std_result_file outpath ("Instance Satisfiable", "", "Instance Unsatisfiable")
16.64 - val _ = if File.exists inpath then warning ("overwriting existing file " ^ quote (Path.pack inpath)) else ()
16.65 - val _ = if File.exists outpath then warning ("overwriting existing file " ^ quote (Path.pack outpath)) else ()
16.66 + val _ = if File.exists inpath then warning ("overwriting existing file " ^ quote (Path.implode inpath)) else ()
16.67 + val _ = if File.exists outpath then warning ("overwriting existing file " ^ quote (Path.implode outpath)) else ()
16.68 val result = SatSolver.make_external_solver cmd writefn readfn fm
16.69 val _ = try File.rm inpath
16.70 val _ = try File.rm outpath
16.71 @@ -936,13 +936,13 @@
16.72 fun berkmin fm =
16.73 let
16.74 val _ = if (getenv "BERKMIN_HOME") = "" orelse (getenv "BERKMIN_EXE") = "" then raise SatSolver.NOT_CONFIGURED else ()
16.75 - val inpath = File.tmp_path (Path.unpack "isabelle.cnf")
16.76 - val outpath = File.tmp_path (Path.unpack "result")
16.77 - val cmd = (getenv "BERKMIN_HOME") ^ "/" ^ (getenv "BERKMIN_EXE") ^ " " ^ (Path.pack inpath) ^ " > " ^ (Path.pack outpath)
16.78 + val inpath = File.tmp_path (Path.explode "isabelle.cnf")
16.79 + val outpath = File.tmp_path (Path.explode "result")
16.80 + val cmd = (getenv "BERKMIN_HOME") ^ "/" ^ (getenv "BERKMIN_EXE") ^ " " ^ (Path.implode inpath) ^ " > " ^ (Path.implode outpath)
16.81 fun writefn fm = SatSolver.write_dimacs_cnf_file inpath (PropLogic.defcnf fm)
16.82 fun readfn () = SatSolver.read_std_result_file outpath ("Satisfiable !!", "solution =", "UNSATISFIABLE !!")
16.83 - val _ = if File.exists inpath then warning ("overwriting existing file " ^ quote (Path.pack inpath)) else ()
16.84 - val _ = if File.exists outpath then warning ("overwriting existing file " ^ quote (Path.pack outpath)) else ()
16.85 + val _ = if File.exists inpath then warning ("overwriting existing file " ^ quote (Path.implode inpath)) else ()
16.86 + val _ = if File.exists outpath then warning ("overwriting existing file " ^ quote (Path.implode outpath)) else ()
16.87 val result = SatSolver.make_external_solver cmd writefn readfn fm
16.88 val _ = try File.rm inpath
16.89 val _ = try File.rm outpath
16.90 @@ -961,13 +961,13 @@
16.91 fun jerusat fm =
16.92 let
16.93 val _ = if (getenv "JERUSAT_HOME") = "" then raise SatSolver.NOT_CONFIGURED else ()
16.94 - val inpath = File.tmp_path (Path.unpack "isabelle.cnf")
16.95 - val outpath = File.tmp_path (Path.unpack "result")
16.96 - val cmd = (getenv "JERUSAT_HOME") ^ "/Jerusat1.3 " ^ (Path.pack inpath) ^ " > " ^ (Path.pack outpath)
16.97 + val inpath = File.tmp_path (Path.explode "isabelle.cnf")
16.98 + val outpath = File.tmp_path (Path.explode "result")
16.99 + val cmd = (getenv "JERUSAT_HOME") ^ "/Jerusat1.3 " ^ (Path.implode inpath) ^ " > " ^ (Path.implode outpath)
16.100 fun writefn fm = SatSolver.write_dimacs_cnf_file inpath (PropLogic.defcnf fm)
16.101 fun readfn () = SatSolver.read_std_result_file outpath ("s SATISFIABLE", "v ", "s UNSATISFIABLE")
16.102 - val _ = if File.exists inpath then warning ("overwriting existing file " ^ quote (Path.pack inpath)) else ()
16.103 - val _ = if File.exists outpath then warning ("overwriting existing file " ^ quote (Path.pack outpath)) else ()
16.104 + val _ = if File.exists inpath then warning ("overwriting existing file " ^ quote (Path.implode inpath)) else ()
16.105 + val _ = if File.exists outpath then warning ("overwriting existing file " ^ quote (Path.implode outpath)) else ()
16.106 val result = SatSolver.make_external_solver cmd writefn readfn fm
16.107 val _ = try File.rm inpath
16.108 val _ = try File.rm outpath
17.1 --- a/src/HOL/Tools/specification_package.ML Thu Dec 14 22:19:39 2006 +0100
17.2 +++ b/src/HOL/Tools/specification_package.ML Fri Dec 15 00:08:06 2006 +0100
17.3 @@ -128,8 +128,8 @@
17.4 fun proc_single prop =
17.5 let
17.6 val frees = Term.term_frees prop
17.7 - val _ = assert (forall (fn v => Sign.of_sort thy (type_of v,HOLogic.typeS)) frees)
17.8 - "Specificaton: Only free variables of sort 'type' allowed"
17.9 + val _ = forall (fn v => Sign.of_sort thy (type_of v,HOLogic.typeS)) frees
17.10 + orelse error "Specificaton: Only free variables of sort 'type' allowed"
17.11 val prop_closed = foldr (fn ((vname,T),prop) => HOLogic.mk_all (vname,T,prop)) prop (map dest_Free frees)
17.12 in
17.13 (prop_closed,frees)
17.14 @@ -145,8 +145,8 @@
17.15 val (altcos,overloaded) = Library.split_list cos
17.16 val (names,sconsts) = Library.split_list altcos
17.17 val consts = map (term_of o Thm.read_cterm thy o rpair TypeInfer.logicT) sconsts
17.18 - val _ = assert (not (Library.exists (not o Term.is_Const) consts))
17.19 - "Specification: Non-constant found as parameter"
17.20 + val _ = not (Library.exists (not o Term.is_Const) consts)
17.21 + orelse error "Specification: Non-constant found as parameter"
17.22
17.23 fun proc_const c =
17.24 let
18.1 --- a/src/Pure/General/file.ML Thu Dec 14 22:19:39 2006 +0100
18.2 +++ b/src/Pure/General/file.ML Fri Dec 15 00:08:06 2006 +0100
18.3 @@ -7,8 +7,8 @@
18.4
18.5 signature FILE =
18.6 sig
18.7 - val unpack_platform_path_fn: (string -> Path.T) ref
18.8 - val unpack_platform_path: string -> Path.T
18.9 + val explode_platform_path_fn: (string -> Path.T) ref
18.10 + val explode_platform_path: string -> Path.T
18.11 val platform_path_fn: (Path.T -> string) ref
18.12 val platform_path: Path.T -> string
18.13 val shell_path_fn: (Path.T -> string) ref
18.14 @@ -22,7 +22,7 @@
18.15 eqtype info
18.16 val info: Path.T -> info option
18.17 val exists: Path.T -> bool
18.18 - val assert: Path.T -> unit
18.19 + val check: Path.T -> unit
18.20 val rm: Path.T -> unit
18.21 val mkdir: Path.T -> unit
18.22 val read: Path.T -> string
18.23 @@ -41,20 +41,20 @@
18.24
18.25 (* platform specific path representations *)
18.26
18.27 -val unpack_platform_path_fn = ref Path.unpack;
18.28 -fun unpack_platform_path s = ! unpack_platform_path_fn s;
18.29 +val explode_platform_path_fn = ref Path.explode;
18.30 +fun explode_platform_path s = ! explode_platform_path_fn s;
18.31
18.32 -val platform_path_fn = ref (Path.pack o Path.expand);
18.33 +val platform_path_fn = ref (Path.implode o Path.expand);
18.34 fun platform_path path = ! platform_path_fn path;
18.35
18.36 -val shell_path_fn = ref (enclose "'" "'" o Path.pack o Path.expand);
18.37 +val shell_path_fn = ref (enclose "'" "'" o Path.implode o Path.expand);
18.38 fun shell_path path = ! shell_path_fn path;
18.39
18.40
18.41 (* current path *)
18.42
18.43 val cd = Library.cd o platform_path;
18.44 -val pwd = unpack_platform_path o Library.pwd;
18.45 +val pwd = explode_platform_path o Library.pwd;
18.46
18.47 fun norm_absolute p =
18.48 let
18.49 @@ -94,9 +94,9 @@
18.50
18.51 val exists = is_some o info;
18.52
18.53 -fun assert path =
18.54 +fun check path =
18.55 if exists path then ()
18.56 - else error ("No such file or directory: " ^ quote (Path.pack path));
18.57 + else error ("No such file or directory: " ^ quote (Path.implode path));
18.58
18.59 val rm = OS.FileSys.remove o platform_path;
18.60
18.61 @@ -137,12 +137,12 @@
18.62 SOME ids => OS.FileSys.compare ids = EQUAL
18.63 | NONE => false);
18.64
18.65 -fun copy from to = conditional (not (eq (from, to))) (fn () =>
18.66 - let val target = if is_dir to then Path.append to (Path.base from) else to
18.67 - in write target (read from) end);
18.68 +fun copy src dst = conditional (not (eq (src, dst))) (fn () =>
18.69 + let val target = if is_dir dst then Path.append dst (Path.base src) else dst
18.70 + in write target (read src) end);
18.71
18.72 -fun copy_dir from to = conditional (not (eq (from, to))) (fn () =>
18.73 - (system_command ("cp -r -f " ^ shell_path from ^ "/. " ^ shell_path to); ()))
18.74 +fun copy_dir src dst = conditional (not (eq (src, dst))) (fn () =>
18.75 + (system_command ("cp -r -f " ^ shell_path src ^ "/. " ^ shell_path dst); ()))
18.76
18.77
18.78 (* use ML files *)
19.1 --- a/src/Pure/General/name_space.ML Thu Dec 14 22:19:39 2006 +0100
19.2 +++ b/src/Pure/General/name_space.ML Fri Dec 15 00:08:06 2006 +0100
19.3 @@ -22,8 +22,8 @@
19.4 val hidden: string -> string
19.5 val separator: string (*single char*)
19.6 val is_qualified: string -> bool
19.7 - val pack: string list -> string
19.8 - val unpack: string -> string list
19.9 + val implode: string list -> string
19.10 + val explode: string -> string list
19.11 val append: string -> string -> string
19.12 val qualified: string -> string -> string
19.13 val base: string -> string
19.14 @@ -70,8 +70,8 @@
19.15 val separator = ".";
19.16 val is_qualified = exists_string (fn s => s = separator);
19.17
19.18 -val pack = space_implode separator;
19.19 -val unpack = space_explode separator;
19.20 +val implode_name = space_implode separator;
19.21 +val explode_name = space_explode separator;
19.22
19.23 fun append name1 "" = name1
19.24 | append "" name2 = name2
19.25 @@ -82,15 +82,15 @@
19.26 else path ^ separator ^ name;
19.27
19.28 fun base "" = ""
19.29 - | base name = List.last (unpack name);
19.30 + | base name = List.last (explode_name name);
19.31
19.32 fun qualifier "" = ""
19.33 - | qualifier name = pack (#1 (split_last (unpack name)));
19.34 + | qualifier name = implode_name (#1 (split_last (explode_name name)));
19.35
19.36 fun map_base _ "" = ""
19.37 | map_base f name =
19.38 - let val names = unpack name
19.39 - in pack (nth_map (length names - 1) f names) end;
19.40 + let val names = explode_name name
19.41 + in implode_name (nth_map (length names - 1) f names) end;
19.42
19.43
19.44 (* accesses *)
19.45 @@ -117,8 +117,8 @@
19.46 [xs @ ys] @@ prefixes1 zs @@ [ws];
19.47 in sfxs @ pfxs end;
19.48
19.49 -val accesses = map pack o suffixes_prefixes o unpack;
19.50 -val accesses' = map pack o Library.suffixes1 o unpack;
19.51 +val accesses = map implode_name o suffixes_prefixes o explode_name;
19.52 +val accesses' = map implode_name o Library.suffixes1 o explode_name;
19.53
19.54
19.55
19.56 @@ -228,10 +228,10 @@
19.57 if is_hidden name then
19.58 error ("Attempt to declare hidden name " ^ quote name)
19.59 else
19.60 - let val names = unpack name in
19.61 + let val names = explode_name name in
19.62 conditional (null names orelse exists (fn s => s = "") names) (fn () =>
19.63 error ("Bad name declaration " ^ quote name));
19.64 - fold (add_name name) (map pack (accs names)) space
19.65 + fold (add_name name) (map implode_name (accs names)) space
19.66 end;
19.67
19.68
19.69 @@ -258,7 +258,7 @@
19.70
19.71 fun sticky_prefix prfx (Naming (path, (qualify, _))) =
19.72 Naming (append path prfx,
19.73 - (qualify, suffixes_prefixes_split (length (unpack path)) (length (unpack prfx))));
19.74 + (qualify, suffixes_prefixes_split (length (explode_name path)) (length (explode_name prfx))));
19.75
19.76 fun set_policy policy (Naming (path, _)) = Naming (path, policy);
19.77
19.78 @@ -284,6 +284,11 @@
19.79 fun dest_table tab = map (apfst #1) (ext_table tab);
19.80 fun extern_table tab = map (apfst #2) (ext_table tab);
19.81
19.82 +
19.83 +(*final declarations of this structure!*)
19.84 +val implode = implode_name;
19.85 +val explode = explode_name;
19.86 +
19.87 end;
19.88
19.89 structure BasicNameSpace: BASIC_NAME_SPACE = NameSpace;
20.1 --- a/src/Pure/General/path.ML Thu Dec 14 22:19:39 2006 +0100
20.2 +++ b/src/Pure/General/path.ML Fri Dec 15 00:08:06 2006 +0100
20.3 @@ -21,8 +21,8 @@
20.4 val append: T -> T -> T
20.5 val appends: T list -> T
20.6 val make: string list -> T
20.7 - val pack: T -> string
20.8 - val unpack: string -> T
20.9 + val implode: T -> string
20.10 + val explode: string -> T
20.11 val dir: T -> T
20.12 val base: T -> T
20.13 val ext: string -> T -> T
20.14 @@ -95,35 +95,35 @@
20.15 fun norm path = rev_app [] path;
20.16
20.17
20.18 -(* pack *)
20.19 +(* implode *)
20.20
20.21 -fun pack_elem Root = ""
20.22 - | pack_elem Parent = ".."
20.23 - | pack_elem (Basic s) = s
20.24 - | pack_elem (Variable s) = "$" ^ s;
20.25 +fun implode_elem Root = ""
20.26 + | implode_elem Parent = ".."
20.27 + | implode_elem (Basic s) = s
20.28 + | implode_elem (Variable s) = "$" ^ s;
20.29
20.30 -fun pack (Path []) = "."
20.31 - | pack (Path (Root :: xs)) = "/" ^ space_implode "/" (map pack_elem xs)
20.32 - | pack (Path xs) = space_implode "/" (map pack_elem xs);
20.33 +fun implode_path (Path []) = "."
20.34 + | implode_path (Path (Root :: xs)) = "/" ^ space_implode "/" (map implode_elem xs)
20.35 + | implode_path (Path xs) = space_implode "/" (map implode_elem xs);
20.36
20.37
20.38 -(* unpack *)
20.39 +(* explode *)
20.40
20.41 -fun unpack_elem "" = Root
20.42 - | unpack_elem ".." = Parent
20.43 - | unpack_elem "~" = Variable "HOME"
20.44 - | unpack_elem "~~" = Variable "ISABELLE_HOME"
20.45 - | unpack_elem s =
20.46 +fun explode_elem "" = Root
20.47 + | explode_elem ".." = Parent
20.48 + | explode_elem "~" = Variable "HOME"
20.49 + | explode_elem "~~" = Variable "ISABELLE_HOME"
20.50 + | explode_elem s =
20.51 (case explode s of
20.52 "$" :: cs => variable_elem cs
20.53 | cs => basic_elem cs);
20.54
20.55 -val unpack_elems = map unpack_elem o filter_out (fn c => c = "" orelse c = ".");
20.56 +val explode_elems = map explode_elem o filter_out (fn c => c = "" orelse c = ".");
20.57
20.58 -fun unpack str = Path (norm
20.59 +fun explode_path str = Path (norm
20.60 (case space_explode "/" str of
20.61 - "" :: ss => Root :: unpack_elems ss
20.62 - | ss => unpack_elems ss));
20.63 + "" :: ss => Root :: explode_elems ss
20.64 + | ss => explode_elems ss));
20.65
20.66
20.67 (* base element *)
20.68 @@ -131,7 +131,7 @@
20.69 fun split_path f (path as Path xs) =
20.70 (case try split_last xs of
20.71 SOME (prfx, Basic s) => f (prfx, s)
20.72 - | _ => error ("Cannot split path into dir/base: " ^ quote (pack path)));
20.73 + | _ => error ("Cannot split path into dir/base: " ^ quote (implode_path path)));
20.74
20.75 val dir = split_path (fn (prfx, _) => Path prfx);
20.76 val base = split_path (fn (_, s) => Path [Basic s]);
20.77 @@ -150,10 +150,15 @@
20.78 fun eval (Variable s) =
20.79 (case getenv s of
20.80 "" => error ("Undefined Isabelle environment variable: " ^ quote s)
20.81 - | path => rep (unpack path))
20.82 + | path => rep (explode_path path))
20.83 | eval x = [x];
20.84
20.85 val expand = rep #> maps eval #> norm #> Path;
20.86 -val position = expand #> pack #> quote #> Position.line_name 1;
20.87 +val position = expand #> implode_path #> quote #> Position.line_name 1;
20.88 +
20.89 +
20.90 +(*final declarations of this structure!*)
20.91 +val implode = implode_path;
20.92 +val explode = explode_path;
20.93
20.94 end;
21.1 --- a/src/Pure/General/scan.ML Thu Dec 14 22:19:39 2006 +0100
21.2 +++ b/src/Pure/General/scan.ML Fri Dec 15 00:08:06 2006 +0100
21.3 @@ -42,8 +42,8 @@
21.4 val one: ('a -> bool) -> 'a list -> 'a * 'a list
21.5 val this: string list -> string list -> string list * string list
21.6 val this_string: string -> string list -> string * string list
21.7 - val any: ('a -> bool) -> 'a list -> 'a list * 'a list
21.8 - val any1: ('a -> bool) -> 'a list -> 'a list * 'a list
21.9 + val many: ('a -> bool) -> 'a list -> 'a list * 'a list
21.10 + val many1: ('a -> bool) -> 'a list -> 'a list * 'a list
21.11 val optional: ('a -> 'b * 'a) -> 'b -> 'a -> 'b * 'a
21.12 val option: ('a -> 'b * 'a) -> 'a -> 'b option * 'a
21.13 val repeat: ('a -> 'b * 'a) -> 'a -> 'b list * 'a
21.14 @@ -143,12 +143,12 @@
21.15
21.16 fun this_string s = this (explode s) >> K s; (*primitive string -- no symbols here!*)
21.17
21.18 -fun any _ [] = raise MORE NONE
21.19 - | any pred (lst as x :: xs) =
21.20 - if pred x then apfst (cons x) (any pred xs)
21.21 +fun many _ [] = raise MORE NONE
21.22 + | many pred (lst as x :: xs) =
21.23 + if pred x then apfst (cons x) (many pred xs)
21.24 else ([], lst);
21.25
21.26 -fun any1 pred = one pred -- any pred >> op ::;
21.27 +fun many1 pred = one pred -- many pred >> op ::;
21.28
21.29 fun optional scan def = scan || succeed def;
21.30 fun option scan = (scan >> SOME) || succeed NONE;
22.1 --- a/src/Pure/General/symbol.ML Thu Dec 14 22:19:39 2006 +0100
22.2 +++ b/src/Pure/General/symbol.ML Fri Dec 15 00:08:06 2006 +0100
22.3 @@ -403,7 +403,7 @@
22.4
22.5 (* scan *)
22.6
22.7 -val scan_id = Scan.one is_letter ^^ (Scan.any is_letdig >> implode);
22.8 +val scan_id = Scan.one is_letter ^^ (Scan.many is_letdig >> implode);
22.9
22.10 local
22.11
22.12 @@ -413,8 +413,8 @@
22.13 $$ "\\" -- Scan.optional ($$ "\\") "" -- Scan.this_string "<^newline>" >> K "\n";
22.14
22.15 val scan_raw =
22.16 - Scan.this_string "raw:" ^^ (Scan.any raw_chr >> implode) ||
22.17 - Scan.this_string "raw" ^^ (Scan.any1 is_ascii_digit >> implode);
22.18 + Scan.this_string "raw:" ^^ (Scan.many raw_chr >> implode) ||
22.19 + Scan.this_string "raw" ^^ (Scan.many1 is_ascii_digit >> implode);
22.20
22.21 in
22.22
22.23 @@ -431,7 +431,7 @@
22.24 (* source *)
22.25
22.26 val recover =
22.27 - Scan.any (fn s => not (is_blank s) andalso s <> "\"" andalso not_eof s) >> K [malformed];
22.28 + Scan.many (fn s => not (is_blank s) andalso s <> "\"" andalso not_eof s) >> K [malformed];
22.29
22.30 fun source do_recover src =
22.31 Source.source stopper (Scan.bulk scan) (if do_recover then SOME recover else NONE) src;
23.1 --- a/src/Pure/General/url.ML Thu Dec 14 22:19:39 2006 +0100
23.2 +++ b/src/Pure/General/url.ML Fri Dec 15 00:08:06 2006 +0100
23.3 @@ -13,8 +13,8 @@
23.4 Http of string * Path.T |
23.5 Ftp of string * Path.T
23.6 val append: T -> T -> T
23.7 - val pack: T -> string
23.8 - val unpack: string -> T
23.9 + val implode: T -> string
23.10 + val explode: string -> T
23.11 end;
23.12
23.13 structure Url: URL =
23.14 @@ -38,26 +38,26 @@
23.15 | append _ url = url;
23.16
23.17
23.18 -(* pack *)
23.19 +(* implode *)
23.20
23.21 -fun pack_path p = if Path.is_current p then "" else Path.pack p;
23.22 +fun implode_path p = if Path.is_current p then "" else Path.implode p;
23.23
23.24 -fun pack (File p) = pack_path p
23.25 - | pack (RemoteFile (h, p)) = "file://" ^ h ^ pack_path p
23.26 - | pack (Http (h, p)) = "http://" ^ h ^ pack_path p
23.27 - | pack (Ftp (h, p)) = "ftp://" ^ h ^ pack_path p;
23.28 +fun implode_url (File p) = implode_path p
23.29 + | implode_url (RemoteFile (h, p)) = "file://" ^ h ^ implode_path p
23.30 + | implode_url (Http (h, p)) = "http://" ^ h ^ implode_path p
23.31 + | implode_url (Ftp (h, p)) = "ftp://" ^ h ^ implode_path p;
23.32
23.33
23.34 -(* unpack *)
23.35 +(* explode *)
23.36
23.37 local
23.38
23.39 val scan_host =
23.40 - (Scan.any1 (fn s => s <> "/" andalso Symbol.not_eof s) >> implode) --|
23.41 + (Scan.many1 (fn s => s <> "/" andalso Symbol.not_eof s) >> implode) --|
23.42 Scan.ahead ($$ "/" || Scan.one Symbol.is_eof);
23.43
23.44 -val scan_path = Scan.any Symbol.not_eof >> (Path.unpack o implode);
23.45 -val scan_path_root = Scan.any Symbol.not_eof >> (Path.unpack o implode o cons "/");
23.46 +val scan_path = Scan.many Symbol.not_eof >> (Path.explode o implode);
23.47 +val scan_path_root = Scan.many Symbol.not_eof >> (Path.explode o implode o cons "/");
23.48
23.49 val scan_url =
23.50 Scan.unless (Scan.this_string "file:" ||
23.51 @@ -71,8 +71,13 @@
23.52
23.53 in
23.54
23.55 -fun unpack s = Symbol.scanner "Malformed URL" scan_url (Symbol.explode s);
23.56 +fun explode_url s = Symbol.scanner "Malformed URL" scan_url (Symbol.explode s);
23.57
23.58 end;
23.59
23.60 +
23.61 +(*final declarations of this structure!*)
23.62 +val implode = implode_url;
23.63 +val explode = explode_url;
23.64 +
23.65 end;
24.1 --- a/src/Pure/General/xml.ML Thu Dec 14 22:19:39 2006 +0100
24.2 +++ b/src/Pure/General/xml.ML Fri Dec 15 00:08:06 2006 +0100
24.3 @@ -118,7 +118,7 @@
24.4 fun err s (xs, _) =
24.5 "XML parsing error: " ^ s ^ "\nfound: " ^ quote (Symbol.beginning 100 xs);
24.6
24.7 -val scan_whspc = Scan.any Symbol.is_blank;
24.8 +val scan_whspc = Scan.many Symbol.is_blank;
24.9
24.10 val scan_special = $$ "&" ^^ Symbol.scan_id ^^ $$ ";" >> decode;
24.11
25.1 --- a/src/Pure/Isar/isar_cmd.ML Thu Dec 14 22:19:39 2006 +0100
25.2 +++ b/src/Pure/Isar/isar_cmd.ML Fri Dec 15 00:08:06 2006 +0100
25.3 @@ -192,7 +192,7 @@
25.4 (* init and exit *)
25.5
25.6 fun begin_theory name imports uses =
25.7 - ThyInfo.begin_theory Present.begin_theory name imports (map (apfst Path.unpack) uses);
25.8 + ThyInfo.begin_theory Present.begin_theory name imports (map (apfst Path.explode) uses);
25.9
25.10 fun end_theory thy =
25.11 if ThyInfo.check_known_thy (Context.theory_name thy) then ThyInfo.end_theory thy else thy;
25.12 @@ -298,7 +298,7 @@
25.13 (* current working directory *)
25.14
25.15 fun cd path = Toplevel.imperative (fn () => (File.cd path));
25.16 -val pwd = Toplevel.imperative (fn () => writeln (Path.pack (File.pwd ())));
25.17 +val pwd = Toplevel.imperative (fn () => writeln (Path.implode (File.pwd ())));
25.18
25.19
25.20 (* load theory files *)
25.21 @@ -496,7 +496,7 @@
25.22 (* markup commands *)
25.23
25.24 fun add_header s = Toplevel.keep' (fn int => fn state =>
25.25 - (Toplevel.assert (Toplevel.is_toplevel state);
25.26 + (if Toplevel.is_toplevel state then () else raise Toplevel.UNDEF;
25.27 if int then OuterSyntax.check_text s NONE else ()));
25.28
25.29 local
26.1 --- a/src/Pure/Isar/isar_output.ML Thu Dec 14 22:19:39 2006 +0100
26.2 +++ b/src/Pure/Isar/isar_output.ML Fri Dec 15 00:08:06 2006 +0100
26.3 @@ -305,10 +305,10 @@
26.4 local
26.5
26.6 val space_proper =
26.7 - Scan.one T.is_blank -- Scan.any T.is_comment -- Scan.one T.is_proper;
26.8 + Scan.one T.is_blank -- Scan.many T.is_comment -- Scan.one T.is_proper;
26.9
26.10 val is_improper = not o (T.is_proper orf T.is_begin_ignore orf T.is_end_ignore);
26.11 -val improper = Scan.any is_improper;
26.12 +val improper = Scan.many is_improper;
26.13 val improper_end = Scan.repeat (Scan.unless space_proper (Scan.one is_improper));
26.14 val blank_end = Scan.repeat (Scan.unless space_proper (Scan.one T.is_blank));
26.15
26.16 @@ -375,7 +375,7 @@
26.17 val cmd = Scan.one (is_some o fst);
26.18 val non_cmd = Scan.one (is_none o fst andf not o #2 stopper) >> #2;
26.19
26.20 - val comments = Scan.any (comment_token o fst o snd);
26.21 + val comments = Scan.many (comment_token o fst o snd);
26.22 val blank = Scan.one (blank_token o fst o snd);
26.23 val newline = Scan.one (newline_token o fst o snd);
26.24 val before_cmd =
27.1 --- a/src/Pure/Isar/outer_lex.ML Thu Dec 14 22:19:39 2006 +0100
27.2 +++ b/src/Pure/Isar/outer_lex.ML Fri Dec 15 00:08:06 2006 +0100
27.3 @@ -193,7 +193,7 @@
27.4 val is_sym_char = member (op =) (explode "!#$%&*+-/<=>?@^_|~");
27.5
27.6 val scan_symid =
27.7 - Scan.any1 is_sym_char >> implode ||
27.8 + Scan.many1 is_sym_char >> implode ||
27.9 Scan.one Symbol.is_symbolic;
27.10
27.11 fun is_symid str =
27.12 @@ -249,8 +249,8 @@
27.13 fun is_space s = Symbol.is_blank s andalso s <> "\n";
27.14
27.15 val scan_space =
27.16 - (keep_line (Scan.any1 is_space) -- Scan.optional (incr_line ($$ "\n")) "" ||
27.17 - keep_line (Scan.any is_space) -- incr_line ($$ "\n")) >> (fn (cs, c) => implode cs ^ c);
27.18 + (keep_line (Scan.many1 is_space) -- Scan.optional (incr_line ($$ "\n")) "" ||
27.19 + keep_line (Scan.many is_space) -- incr_line ($$ "\n")) >> (fn (cs, c) => implode cs ^ c);
27.20
27.21
27.22 (* scan nested comments *)
27.23 @@ -303,7 +303,7 @@
27.24 (* token sources *)
27.25
27.26 val is_junk = (not o Symbol.is_blank) andf Symbol.not_sync andf Symbol.not_eof;
27.27 -fun recover xs = (keep_line (Scan.any is_junk) >> (fn ts => [malformed_of ts])) xs;
27.28 +fun recover xs = (keep_line (Scan.many is_junk) >> (fn ts => [malformed_of ts])) xs;
27.29
27.30 fun source do_recover get_lex pos src =
27.31 Source.source' pos Symbol.stopper (Scan.bulk (fn xs => scan (get_lex ()) xs))
28.1 --- a/src/Pure/Isar/outer_parse.ML Thu Dec 14 22:19:39 2006 +0100
28.2 +++ b/src/Pure/Isar/outer_parse.ML Fri Dec 15 00:08:06 2006 +0100
28.3 @@ -220,7 +220,7 @@
28.4 val name = group "name declaration" (short_ident || sym_ident || string || number);
28.5 val xname = group "name reference" (short_ident || long_ident || sym_ident || string || number);
28.6 val text = group "text" (short_ident || long_ident || sym_ident || string || number || verbatim);
28.7 -val path = group "file name/path specification" name >> Path.unpack;
28.8 +val path = group "file name/path specification" name >> Path.explode;
28.9
28.10 val parname = Scan.optional ($$$ "(" |-- name --| $$$ ")") "";
28.11
29.1 --- a/src/Pure/Isar/outer_syntax.ML Thu Dec 14 22:19:39 2006 +0100
29.2 +++ b/src/Pure/Isar/outer_syntax.ML Fri Dec 15 00:08:06 2006 +0100
29.3 @@ -253,9 +253,9 @@
29.4 val ml_file = if ml andalso is_some (ThyLoad.check_file NONE ml_path) then [ml_path] else [];
29.5 in
29.6 if name <> name' then
29.7 - error ("Filename " ^ quote (Path.pack path) ^
29.8 + error ("Filename " ^ quote (Path.implode path) ^
29.9 " does not agree with theory name " ^ quote name')
29.10 - else (parents, map (Path.unpack o #1) files @ ml_file)
29.11 + else (parents, map (Path.explode o #1) files @ ml_file)
29.12 end;
29.13
29.14
29.15 @@ -268,7 +268,7 @@
29.16 if is_none (ThyLoad.check_file NONE path) then ()
29.17 else
29.18 let
29.19 - val _ = warning ("Loading legacy ML script " ^ quote (Path.pack path));
29.20 + val _ = warning ("Loading legacy ML script " ^ quote (Path.implode path));
29.21 val tr = Toplevel.imperative (fn () => ThyInfo.load_file time path);
29.22 val tr_name = if time then "time_use" else "use";
29.23 in Toplevel.excursion [Toplevel.empty |> Toplevel.name tr_name |> tr] end
30.1 --- a/src/Pure/Isar/session.ML Thu Dec 14 22:19:39 2006 +0100
30.2 +++ b/src/Pure/Isar/session.ML Fri Dec 15 00:08:06 2006 +0100
30.3 @@ -71,11 +71,11 @@
30.4 if is_some (! remote_path) then
30.5 error "Path for remote theory browsing information may only be set once"
30.6 else
30.7 - remote_path := SOME (Url.unpack rpath);
30.8 + remote_path := SOME (Url.explode rpath);
30.9 (! remote_path, rpath <> ""));
30.10
30.11 fun dumping (_, "") = NONE
30.12 - | dumping (cp, path) = SOME (cp, Path.unpack path);
30.13 + | dumping (cp, path) = SOME (cp, Path.explode path);
30.14
30.15 fun use_dir root build modes reset info doc doc_graph doc_versions
30.16 parent name dump rpath level verbose =
31.1 --- a/src/Pure/Proof/extraction.ML Thu Dec 14 22:19:39 2006 +0100
31.2 +++ b/src/Pure/Proof/extraction.ML Fri Dec 15 00:08:06 2006 +0100
31.3 @@ -315,7 +315,7 @@
31.4 in fn (thm, (vs, s1, s2)) =>
31.5 let
31.6 val name = Thm.get_name thm;
31.7 - val _ = assert (name <> "") "add_realizers: unnamed theorem";
31.8 + val _ = name <> "" orelse error "add_realizers: unnamed theorem";
31.9 val prop = Pattern.rewrite_term thy'
31.10 (map (Logic.dest_equals o prop_of) defs) [] (prop_of thm);
31.11 val vars = vars_of prop;
31.12 @@ -360,7 +360,7 @@
31.13 defs, expand, prep} = ExtractionData.get thy;
31.14
31.15 val name = Thm.get_name thm;
31.16 - val _ = assert (name <> "") "add_expand_thms: unnamed theorem";
31.17 + val _ = name <> "" orelse error "add_expand_thms: unnamed theorem";
31.18
31.19 val is_def =
31.20 (case strip_comb (fst (Logic.dest_equals (prop_of thm))) of
31.21 @@ -568,7 +568,7 @@
31.22 NONE => (case find vs' (find' name defs') of
31.23 NONE =>
31.24 let
31.25 - val _ = assert (T = nullT) "corr: internal error";
31.26 + val _ = T = nullT orelse error "corr: internal error";
31.27 val _ = msg d ("Building correctness proof for " ^ quote name ^
31.28 (if null vs' then ""
31.29 else " (relevant variables: " ^ commas_quote vs' ^ ")"));
31.30 @@ -720,8 +720,8 @@
31.31 let
31.32 val {prop, der = (_, prf), sign, ...} = rep_thm thm;
31.33 val name = Thm.get_name thm;
31.34 - val _ = assert (name <> "") "extraction: unnamed theorem";
31.35 - val _ = assert (etype_of thy' vs [] prop <> nullT) ("theorem " ^
31.36 + val _ = name <> "" orelse error "extraction: unnamed theorem";
31.37 + val _ = etype_of thy' vs [] prop <> nullT orelse error ("theorem " ^
31.38 quote name ^ " has no computational content")
31.39 in (Reconstruct.reconstruct_proof sign prop prf, vs) end;
31.40
32.1 --- a/src/Pure/Proof/proof_syntax.ML Thu Dec 14 22:19:39 2006 +0100
32.2 +++ b/src/Pure/Proof/proof_syntax.ML Fri Dec 15 00:08:06 2006 +0100
32.3 @@ -134,16 +134,16 @@
32.4 fun prf_of [] (Bound i) = PBound i
32.5 | prf_of Ts (Const (s, Type ("proof", _))) =
32.6 change_type (if ty then SOME Ts else NONE)
32.7 - (case NameSpace.unpack s of
32.8 + (case NameSpace.explode s of
32.9 "axm" :: xs =>
32.10 let
32.11 - val name = NameSpace.pack xs;
32.12 + val name = NameSpace.implode xs;
32.13 val prop = (case AList.lookup (op =) axms name of
32.14 SOME prop => prop
32.15 | NONE => error ("Unknown axiom " ^ quote name))
32.16 in PAxm (name, prop, NONE) end
32.17 | "thm" :: xs =>
32.18 - let val name = NameSpace.pack xs;
32.19 + let val name = NameSpace.implode xs;
32.20 in (case AList.lookup (op =) thms name of
32.21 SOME thm => fst (strip_combt (Thm.proof_of thm))
32.22 | NONE => (case Symtab.lookup tab name of
33.1 --- a/src/Pure/ProofGeneral/pgip_output.ML Thu Dec 14 22:19:39 2006 +0100
33.2 +++ b/src/Pure/ProofGeneral/pgip_output.ML Fri Dec 15 00:08:06 2006 +0100
33.3 @@ -184,7 +184,7 @@
33.4 ("version", version),
33.5 ("instance", instance),
33.6 ("descr", descr),
33.7 - ("url", Url.pack url),
33.8 + ("url", Url.implode url),
33.9 ("filenameextns", filenameextns)],
33.10 [])
33.11 end
34.1 --- a/src/Pure/ProofGeneral/pgip_types.ML Thu Dec 14 22:19:39 2006 +0100
34.2 +++ b/src/Pure/ProofGeneral/pgip_types.ML Fri Dec 15 00:08:06 2006 +0100
34.3 @@ -279,7 +279,7 @@
34.4 (** Url operations **)
34.5
34.6 fun pgipurl_of_string url = (* only handle file:/// or file://localhost/ *)
34.7 - case Url.unpack url of
34.8 + case Url.explode url of
34.9 (Url.File path) => path
34.10 | _ => raise PGIP ("Cannot access non-local URL " ^ url)
34.11
34.12 @@ -291,7 +291,7 @@
34.13 val pgipurl_of_attrs = pgipurl_of_string o (get_attr "url")
34.14
34.15 fun pgipurl_of_url (Url.File p) = p
34.16 - | pgipurl_of_url url = raise PGIP ("Cannot access non-local/non-file URL " ^ (Url.pack url))
34.17 + | pgipurl_of_url url = raise PGIP ("Cannot access non-local/non-file URL " ^ (Url.implode url))
34.18
34.19
34.20 (** Messages and errors **)
35.1 --- a/src/Pure/ProofGeneral/proof_general_emacs.ML Thu Dec 14 22:19:39 2006 +0100
35.2 +++ b/src/Pure/ProofGeneral/proof_general_emacs.ML Fri Dec 15 00:08:06 2006 +0100
35.3 @@ -176,7 +176,7 @@
35.4
35.5 (* prepare theory context *)
35.6
35.7 -val thy_name = Path.pack o #1 o Path.split_ext o Path.base o Path.unpack;
35.8 +val thy_name = Path.implode o #1 o Path.split_ext o Path.base o Path.explode;
35.9
35.10 (* FIXME general treatment of tracing*)
35.11 val update_thy_only = setmp MetaSimplifier.trace_simp false ThyInfo.update_thy_only;
35.12 @@ -187,7 +187,7 @@
35.13 | NONE => "");
35.14
35.15 fun try_update_thy_only file =
35.16 - ThyLoad.cond_add_path (Path.dir (Path.unpack file)) (fn () =>
35.17 + ThyLoad.cond_add_path (Path.dir (Path.explode file)) (fn () =>
35.18 let val name = thy_name file in
35.19 if is_some (ThyLoad.check_file NONE (ThyLoad.thy_path name))
35.20 then update_thy_only name
35.21 @@ -207,13 +207,13 @@
35.22 (ThyInfo.touch_child_thys name;
35.23 ThyInfo.pretend_use_thy_only name handle ERROR msg =>
35.24 (warning msg; warning ("Failed to register theory: " ^ quote name);
35.25 - tell_file_retracted (Path.base (Path.unpack file))))
35.26 + tell_file_retracted (Path.base (Path.explode file))))
35.27 else raise Toplevel.UNDEF
35.28 end;
35.29
35.30 fun vacuous_inform_file_processed file state =
35.31 (warning ("No theory " ^ quote (thy_name file));
35.32 - tell_file_retracted (Path.base (Path.unpack file)));
35.33 + tell_file_retracted (Path.base (Path.explode file)));
35.34
35.35
35.36 (* restart top-level loop (keeps most state information) *)
35.37 @@ -371,7 +371,7 @@
35.38
35.39 fun write_keywords s =
35.40 (init_outer_syntax ();
35.41 - File.write (Path.unpack ("isar-keywords" ^ (if s = "" then "" else "-" ^ s) ^".el"))
35.42 + File.write (Path.explode ("isar-keywords" ^ (if s = "" then "" else "-" ^ s) ^".el"))
35.43 (make_elisp_syntax (OuterSyntax.dest_keywords (), OuterSyntax.dest_parsers ())));
35.44
35.45 end;
36.1 --- a/src/Pure/ProofGeneral/proof_general_pgip.ML Thu Dec 14 22:19:39 2006 +0100
36.2 +++ b/src/Pure/ProofGeneral/proof_general_pgip.ML Fri Dec 15 00:08:06 2006 +0100
36.3 @@ -271,7 +271,7 @@
36.4
36.5 (* prepare theory context *)
36.6
36.7 -val thy_name = Path.pack o #1 o Path.split_ext o Path.base o Path.unpack;
36.8 +val thy_name = Path.implode o #1 o Path.split_ext o Path.base o Path.explode;
36.9
36.10 (* FIXME general treatment of tracing*)
36.11 val update_thy_only = setmp MetaSimplifier.trace_simp false ThyInfo.update_thy_only;
36.12 @@ -282,7 +282,7 @@
36.13 | NONE => "");
36.14
36.15 fun try_update_thy_only file =
36.16 - ThyLoad.cond_add_path (Path.dir (Path.unpack file)) (fn () =>
36.17 + ThyLoad.cond_add_path (Path.dir (Path.explode file)) (fn () =>
36.18 let val name = thy_name file in
36.19 if is_some (ThyLoad.check_file NONE (ThyLoad.thy_path name))
36.20 then update_thy_only name
36.21 @@ -302,13 +302,13 @@
36.22 (ThyInfo.touch_child_thys name;
36.23 ThyInfo.pretend_use_thy_only name handle ERROR msg =>
36.24 (warning msg; warning ("Failed to register theory: " ^ quote name);
36.25 - tell_file_retracted (Path.base (Path.unpack file))))
36.26 + tell_file_retracted (Path.base (Path.explode file))))
36.27 else raise Toplevel.UNDEF
36.28 end;
36.29
36.30 fun vacuous_inform_file_processed file state =
36.31 (warning ("No theory " ^ quote (thy_name file));
36.32 - tell_file_retracted (Path.base (Path.unpack file)));
36.33 + tell_file_retracted (Path.base (Path.explode file)));
36.34
36.35
36.36 (* restart top-level loop (keeps most state information) *)
36.37 @@ -387,15 +387,15 @@
36.38 in
36.39 fun send_pgip_config () =
36.40 let
36.41 - val path = Path.unpack (config_file())
36.42 + val path = Path.explode (config_file())
36.43 val exists = File.exists path
36.44
36.45 val wwwpage =
36.46 - (Url.unpack (isabelle_www()))
36.47 + (Url.explode (isabelle_www()))
36.48 handle _ =>
36.49 (Output.panic
36.50 ("Error in URL in environment variable ISABELLE_HOMEPAGE.");
36.51 - Url.unpack isabellewww)
36.52 + Url.explode isabellewww)
36.53
36.54 val proverinfo =
36.55 Proverinfo { name = "Isabelle",
36.56 @@ -459,11 +459,11 @@
36.57
36.58 fun use_thy_or_ml_file file =
36.59 let
36.60 - val (path,extn) = Path.split_ext (Path.unpack file)
36.61 + val (path,extn) = Path.split_ext (Path.explode file)
36.62 in
36.63 case extn of
36.64 - "" => isarcmd ("use_thy " ^ (quote (Path.pack path)))
36.65 - | "thy" => isarcmd ("use_thy " ^ (quote (Path.pack path)))
36.66 + "" => isarcmd ("use_thy " ^ (quote (Path.implode path)))
36.67 + | "thy" => isarcmd ("use_thy " ^ (quote (Path.implode path)))
36.68 | "ML" => isarcmd ("use " ^ quote file)
36.69 | other => error ("Don't know how to read a file with extension " ^ other)
36.70 end
37.1 --- a/src/Pure/ROOT.ML Thu Dec 14 22:19:39 2006 +0100
37.2 +++ b/src/Pure/ROOT.ML Fri Dec 15 00:08:06 2006 +0100
37.3 @@ -99,7 +99,7 @@
37.4 (*final ML setup*)
37.5 use "install_pp.ML";
37.6 val use = ThyInfo.use;
37.7 -val cd = File.cd o Path.unpack;
37.8 +val cd = File.cd o Path.explode;
37.9 ml_prompts "ML> " "ML# ";
37.10
37.11 proofs := 0;
38.1 --- a/src/Pure/Syntax/lexicon.ML Thu Dec 14 22:19:39 2006 +0100
38.2 +++ b/src/Pure/Syntax/lexicon.ML Fri Dec 15 00:08:06 2006 +0100
38.3 @@ -93,10 +93,10 @@
38.4
38.5 (** basic scanners **)
38.6
38.7 -val scan_letter_letdigs = Scan.one Symbol.is_letter -- Scan.any Symbol.is_letdig >> op ::;
38.8 -val scan_digits1 = Scan.any1 Symbol.is_digit;
38.9 -val scan_hex1 = Scan.any1 (Symbol.is_digit orf Symbol.is_hex_letter);
38.10 -val scan_bin1 = Scan.any1 (fn s => s = "0" orelse s = "1");
38.11 +val scan_letter_letdigs = Scan.one Symbol.is_letter -- Scan.many Symbol.is_letdig >> op ::;
38.12 +val scan_digits1 = Scan.many1 Symbol.is_digit;
38.13 +val scan_hex1 = Scan.many1 (Symbol.is_digit orf Symbol.is_hex_letter);
38.14 +val scan_bin1 = Scan.many1 (fn s => s = "0" orelse s = "1");
38.15
38.16 val scan_id = scan_letter_letdigs >> implode;
38.17 val scan_longid = scan_id ^^ (Scan.repeat1 ($$ "." ^^ scan_id) >> implode);
38.18 @@ -344,7 +344,7 @@
38.19 let
38.20 val scan =
38.21 $$ "?" |-- scan_indexname --| Scan.ahead (Scan.one Symbol.is_eof) >> var ||
38.22 - Scan.any Symbol.not_eof >> (free o implode);
38.23 + Scan.many Symbol.not_eof >> (free o implode);
38.24 in the (Scan.read Symbol.stopper scan (Symbol.explode str)) end;
38.25
38.26
38.27 @@ -388,7 +388,7 @@
38.28 val ten = ord "0" + 10;
38.29 val a = ord "a";
38.30 val A = ord "A";
38.31 -val _ = assert (a > A) "Bad ASCII";
38.32 +val _ = a > A orelse error "Bad ASCII";
38.33
38.34 fun remap_hex c =
38.35 let val x = ord c in
38.36 @@ -421,8 +421,8 @@
38.37
38.38 fun read_idents str =
38.39 let
38.40 - val blanks = Scan.any Symbol.is_blank;
38.41 - val junk = Scan.any Symbol.not_eof;
38.42 + val blanks = Scan.many Symbol.is_blank;
38.43 + val junk = Scan.many Symbol.not_eof;
38.44 val idents = Scan.repeat1 (blanks |-- scan_id --| blanks) -- junk;
38.45 in
38.46 (case Scan.read Symbol.stopper idents (Symbol.explode str) of
39.1 --- a/src/Pure/Syntax/syn_ext.ML Thu Dec 14 22:19:39 2006 +0100
39.2 +++ b/src/Pure/Syntax/syn_ext.ML Fri Dec 15 00:08:06 2006 +0100
39.3 @@ -203,11 +203,11 @@
39.4 val scan_sym =
39.5 $$ "_" >> K (Argument ("", 0)) ||
39.6 $$ "\\<index>" >> K index ||
39.7 - $$ "(" |-- Scan.any Symbol.is_digit >> (Bg o read_int) ||
39.8 + $$ "(" |-- Scan.many Symbol.is_digit >> (Bg o read_int) ||
39.9 $$ ")" >> K En ||
39.10 $$ "/" -- $$ "/" >> K (Brk ~1) ||
39.11 - $$ "/" |-- Scan.any Symbol.is_blank >> (Brk o length) ||
39.12 - Scan.any1 Symbol.is_blank >> (Space o implode) ||
39.13 + $$ "/" |-- Scan.many Symbol.is_blank >> (Brk o length) ||
39.14 + Scan.many1 Symbol.is_blank >> (Space o implode) ||
39.15 Scan.repeat1 scan_delim_char >> (Delim o implode);
39.16
39.17 val scan_symb =
40.1 --- a/src/Pure/Thy/html.ML Thu Dec 14 22:19:39 2006 +0100
40.2 +++ b/src/Pure/Thy/html.ML Fri Dec 15 00:08:06 2006 +0100
40.3 @@ -266,13 +266,13 @@
40.4 val keyword = enclose "<span class=\"keyword\">" "</span>" o output;
40.5 val keyword_width = apfst (enclose "<span class=\"keyword\">" "</span>") o output_width;
40.6 val file_name = enclose "<span class=\"filename\">" "</span>" o output;
40.7 -val file_path = file_name o Url.pack;
40.8 +val file_path = file_name o Url.implode;
40.9
40.10
40.11 (* misc *)
40.12
40.13 fun href_name s txt = "<a href=" ^ Library.quote s ^ ">" ^ txt ^ "</a>";
40.14 -fun href_path path txt = href_name (Url.pack path) txt;
40.15 +fun href_path path txt = href_name (Url.implode path) txt;
40.16
40.17 fun href_opt_name NONE txt = txt
40.18 | href_opt_name (SOME s) txt = href_name s txt;
40.19 @@ -400,7 +400,7 @@
40.20 (* ML file *)
40.21
40.22 fun ml_file path str =
40.23 - begin_document ("File " ^ Url.pack path) ^
40.24 + begin_document ("File " ^ Url.implode path) ^
40.25 "\n</div>\n<hr><div class=\"mlsource\">\n" ^
40.26 verbatim str ^
40.27 "\n</div>\n<hr>\n<div class=\"mlfooter\">\n" ^
41.1 --- a/src/Pure/Thy/present.ML Thu Dec 14 22:19:39 2006 +0100
41.2 +++ b/src/Pure/Thy/present.ML Fri Dec 15 00:08:06 2006 +0100
41.3 @@ -60,15 +60,15 @@
41.4 val graph_eps_path = Path.basic "session_graph.eps";
41.5
41.6 val session_path = Path.basic ".session";
41.7 -val session_entries_path = Path.unpack ".session/entries";
41.8 -val pre_index_path = Path.unpack ".session/pre-index";
41.9 +val session_entries_path = Path.explode ".session/entries";
41.10 +val pre_index_path = Path.explode ".session/pre-index";
41.11
41.12 fun mk_rel_path [] ys = Path.make ys
41.13 | mk_rel_path xs [] = Path.appends (replicate (length xs) Path.parent)
41.14 | mk_rel_path (ps as x :: xs) (qs as y :: ys) = if x = y then mk_rel_path xs ys else
41.15 Path.appends (replicate (length ps) Path.parent @ [Path.make qs]);
41.16
41.17 -fun show_path path = Path.pack (Path.append (File.pwd ()) path);
41.18 +fun show_path path = Path.implode (Path.append (File.pwd ()) path);
41.19
41.20
41.21
41.22 @@ -108,7 +108,7 @@
41.23 fun display_graph gr =
41.24 let
41.25 val _ = writeln "Generating graph ...";
41.26 - val path = File.tmp_path (Path.unpack "tmp.graph");
41.27 + val path = File.tmp_path (Path.explode "tmp.graph");
41.28 val _ = write_graph gr path;
41.29 val _ = File.isatool ("browser -c " ^ File.shell_path path ^ " &");
41.30 in () end;
41.31 @@ -126,9 +126,9 @@
41.32 path =
41.33 if null session then "" else
41.34 if is_some remote_path andalso not is_local then
41.35 - Url.pack (Url.append (the remote_path) (Url.File
41.36 + Url.implode (Url.append (the remote_path) (Url.File
41.37 (Path.append (Path.make session) (html_path name))))
41.38 - else Path.pack (Path.append (mk_rel_path curr_sess session) (html_path name)),
41.39 + else Path.implode (Path.append (mk_rel_path curr_sess session) (html_path name)),
41.40 unfold = false,
41.41 parents =
41.42 map (fn s => ID_of (#session (get_info (ThyInfo.theory s))) s) (ThyInfo.get_preds name)}
41.43 @@ -271,7 +271,7 @@
41.44
41.45 fun update_index dir name =
41.46 (case try get_entries dir of
41.47 - NONE => warning ("Browser info: cannot access session index of " ^ quote (Path.pack dir))
41.48 + NONE => warning ("Browser info: cannot access session index of " ^ quote (Path.implode dir))
41.49 | SOME es => (put_entries ((remove (op =) name es) @ [name]) dir; create_index dir));
41.50
41.51
41.52 @@ -323,7 +323,7 @@
41.53 (case readme of NONE => [] | SOME p => [(Url.File p, "README")]) @
41.54 map (fn (name, _) => (Url.File (Path.ext doc (Path.basic name)), name)) documents;
41.55 val index_text = HTML.begin_index (index_up_lnk, parent_name)
41.56 - (Url.File index_path, session_name) docs (Url.unpack "medium.html");
41.57 + (Url.File index_path, session_name) docs (Url.explode "medium.html");
41.58 in
41.59 session_info := SOME (make_session_info (name, parent_name, session_name, path, html_prefix,
41.60 info, doc, doc_graph, documents, doc_prefix1, doc_prefix2, remote_path, verbose, readme));
41.61 @@ -407,10 +407,10 @@
41.62 if length path > 1 then update_index parent_html_prefix name else ();
41.63 (case readme of NONE => () | SOME path => File.copy path html_prefix);
41.64 write_graph graph (Path.append html_prefix graph_path);
41.65 - File.copy (Path.unpack "~~/lib/browser/GraphBrowser.jar") html_prefix;
41.66 + File.copy (Path.explode "~~/lib/browser/GraphBrowser.jar") html_prefix;
41.67 List.app (fn (a, txt) => File.write (Path.append html_prefix (Path.basic a)) txt)
41.68 (HTML.applet_pages name (Url.File index_path, name));
41.69 - File.copy (Path.unpack "~~/lib/html/isabelle.css") html_prefix;
41.70 + File.copy (Path.explode "~~/lib/html/isabelle.css") html_prefix;
41.71 List.app finish_html thys;
41.72 List.app (uncurry File.write) files;
41.73 conditional verbose (fn () =>
41.74 @@ -474,7 +474,7 @@
41.75 HTML.ml_file (Url.File base) (File.read path));
41.76 (SOME (Url.File base_html), Url.File raw_path, loadit)
41.77 end
41.78 - | NONE => (warning ("Browser info: expected to find ML file" ^ quote (Path.pack raw_path));
41.79 + | NONE => (warning ("Browser info: expected to find ML file" ^ quote (Path.implode raw_path));
41.80 (NONE, Url.File raw_path, loadit)));
41.81
41.82 val files_html = map prep_file files;
41.83 @@ -487,7 +487,7 @@
41.84
41.85 val entry =
41.86 {name = name, ID = ID_of path name, dir = sess_name, unfold = true,
41.87 - path = Path.pack (html_path name),
41.88 + path = Path.implode (html_path name),
41.89 parents = map (fn s => ID_of (#session (get_info (ThyInfo.theory s))) s) raw_parents};
41.90
41.91 in
41.92 @@ -523,11 +523,11 @@
41.93 let
41.94 val base = Path.base path;
41.95 val name =
41.96 - (case Path.pack (#1 (Path.split_ext base)) of "" => gensym "DUMMY" | s => s);
41.97 + (case Path.implode (#1 (Path.split_ext base)) of "" => gensym "DUMMY" | s => s);
41.98 in
41.99 if File.exists path then
41.100 (Buffer.add (Latex.theory_entry name) tex_index, (name, base, File.read path))
41.101 - else error ("Bad file: " ^ quote (Path.pack path))
41.102 + else error ("Bad file: " ^ quote (Path.implode path))
41.103 end;
41.104 val (tex_index, srcs) = foldl_map prep_draft (Buffer.empty, src_paths);
41.105
41.106 @@ -535,7 +535,7 @@
41.107 val result_path = Path.append doc_path Path.parent;
41.108 val _ = File.mkdir doc_path;
41.109 val root_path = Path.append doc_path (Path.basic "root.tex");
41.110 - val _ = File.copy (Path.unpack "~~/lib/texinputs/draft.tex") root_path;
41.111 + val _ = File.copy (Path.explode "~~/lib/texinputs/draft.tex") root_path;
41.112 val _ = File.isatool ("latex -o sty " ^ File.shell_path root_path);
41.113 val _ = File.isatool ("latex -o syms " ^ File.shell_path root_path);
41.114
41.115 @@ -547,7 +547,7 @@
41.116
41.117 val _ = srcs |> List.app (fn (name, base, txt) =>
41.118 Symbol.explode txt
41.119 - |> Latex.symbol_source (known_syms, known_ctrls) (Path.pack base)
41.120 + |> Latex.symbol_source (known_syms, known_ctrls) (Path.implode base)
41.121 |> File.write (Path.append doc_path (tex_path name)));
41.122 val _ = write_tex_index tex_index doc_path;
41.123 in isatool_document false doc_format documentN "" doc_path result_path end;
42.1 --- a/src/Pure/Thy/thm_database.ML Thu Dec 14 22:19:39 2006 +0100
42.2 +++ b/src/Pure/Thy/thm_database.ML Fri Dec 15 00:08:06 2006 +0100
42.3 @@ -78,7 +78,7 @@
42.4 NameSpace.intern space xname = name then
42.5 SOME (prfx, (bname, xname, length (the (Symtab.lookup thms name)) = 1))
42.6 else NONE;
42.7 - val names = NameSpace.unpack name;
42.8 + val names = NameSpace.explode name;
42.9 in
42.10 (case #2 (chop (length names - 2) names) of
42.11 [bname] => result "" bname
43.1 --- a/src/Pure/Thy/thm_deps.ML Thu Dec 14 22:19:39 2006 +0100
43.2 +++ b/src/Pure/Thy/thm_deps.ML Fri Dec 15 00:08:06 2006 +0100
43.3 @@ -43,7 +43,7 @@
43.4 if not (Symtab.defined gra name) then
43.5 let
43.6 val (gra', parents') = make_deps_graph prf' (gra, []);
43.7 - val prefx = #1 (Library.split_last (NameSpace.unpack name));
43.8 + val prefx = #1 (Library.split_last (NameSpace.explode name));
43.9 val session =
43.10 (case prefx of
43.11 (x :: _) =>
44.1 --- a/src/Pure/Thy/thy_info.ML Thu Dec 14 22:19:39 2006 +0100
44.2 +++ b/src/Pure/Thy/thy_info.ML Fri Dec 15 00:08:06 2006 +0100
44.3 @@ -256,7 +256,7 @@
44.4 fun provide path name info (deps as SOME {present, outdated, master, files}) =
44.5 (if exists (equal path o #1) files then ()
44.6 else warning (loader_msg "undeclared dependency of theory" [name] ^
44.7 - " on file: " ^ quote (Path.pack path));
44.8 + " on file: " ^ quote (Path.implode path));
44.9 SOME (make_deps present outdated master (AList.update (op =) (path, SOME info) files)))
44.10 | provide _ _ _ NONE = NONE;
44.11
44.12 @@ -272,7 +272,7 @@
44.13
44.14 fun load_file time path = Output.toplevel_errors (fn () =>
44.15 if time then
44.16 - let val name = Path.pack path in
44.17 + let val name = Path.implode path in
44.18 timeit (fn () =>
44.19 (priority ("\n**** Starting file " ^ quote name ^ " ****");
44.20 run_file path;
44.21 @@ -280,8 +280,8 @@
44.22 end
44.23 else run_file path) ();
44.24
44.25 -val use = load_file false o Path.unpack;
44.26 -val time_use = load_file true o Path.unpack;
44.27 +val use = load_file false o Path.explode;
44.28 +val time_use = load_file true o Path.explode;
44.29
44.30 end;
44.31
44.32 @@ -303,7 +303,7 @@
44.33 else #1 (ThyLoad.deps_thy dir name ml);
44.34
44.35 val files = get_files name;
44.36 - val missing_files = map_filter (fn (path, NONE) => SOME (Path.pack path) | _ => NONE) files;
44.37 + val missing_files = map_filter (fn (path, NONE) => SOME (Path.implode path) | _ => NONE) files;
44.38 in
44.39 if null missing_files then ()
44.40 else warning (loader_msg "unresolved dependencies of theory" [name] ^
44.41 @@ -315,7 +315,7 @@
44.42
44.43 (* require_thy *)
44.44
44.45 -fun base_of_path s = Path.pack (Path.base (Path.unpack s));
44.46 +fun base_of_path s = Path.implode (Path.base (Path.explode s));
44.47
44.48 local
44.49
44.50 @@ -333,7 +333,7 @@
44.51 | SOME deps =>
44.52 let
44.53 fun get_name s = (case opt_path'' (lookup_deps s) of NONE => s
44.54 - | SOME p => Path.pack (Path.append p (Path.basic s)));
44.55 + | SOME p => Path.implode (Path.append p (Path.basic s)));
44.56 val same_deps = (NONE, map get_name (thy_graph Graph.imm_preds name))
44.57 in
44.58 (case deps of
44.59 @@ -349,8 +349,8 @@
44.60
44.61 fun require_thy really ml time strict keep_strict initiators prfx (visited, str) =
44.62 let
44.63 - val path = Path.expand (Path.unpack str);
44.64 - val name = Path.pack (Path.base path);
44.65 + val path = Path.expand (Path.explode str);
44.66 + val name = Path.implode (Path.base path);
44.67 in
44.68 if member (op =) initiators name then error (cycle_msg initiators) else ();
44.69 if known_thy name andalso is_finished name orelse member (op =) visited name then
44.70 @@ -422,7 +422,7 @@
44.71 let val illegal = map (fn ext => Path.ext ext (Path.basic name)) ThyLoad.ml_exts in
44.72 (case find_first (member (op =) illegal o Path.base o Path.expand o #1) uses of
44.73 NONE => ()
44.74 - | SOME (path, _) => error ("Illegal use of theory ML file: " ^ quote (Path.pack path)))
44.75 + | SOME (path, _) => error ("Illegal use of theory ML file: " ^ quote (Path.implode path)))
44.76 end;
44.77
44.78 fun begin_theory present name parents uses int =
45.1 --- a/src/Pure/Thy/thy_load.ML Thu Dec 14 22:19:39 2006 +0100
45.2 +++ b/src/Pure/Thy/thy_load.ML Fri Dec 15 00:08:06 2006 +0100
45.3 @@ -49,12 +49,12 @@
45.4 val load_path = ref [Path.current];
45.5 fun change_path f = load_path := f (! load_path);
45.6
45.7 -fun show_path () = map Path.pack (! load_path);
45.8 -fun del_path s = change_path (filter_out (equal (Path.unpack s)));
45.9 -fun add_path s = (del_path s; change_path (cons (Path.unpack s)));
45.10 -fun path_add s = (del_path s; change_path (fn path => path @ [Path.unpack s]));
45.11 +fun show_path () = map Path.implode (! load_path);
45.12 +fun del_path s = change_path (filter_out (equal (Path.explode s)));
45.13 +fun add_path s = (del_path s; change_path (cons (Path.explode s)));
45.14 +fun path_add s = (del_path s; change_path (fn path => path @ [Path.explode s]));
45.15 fun reset_path () = load_path := [Path.current];
45.16 -fun with_paths ss f x = Library.setmp load_path (! load_path @ map Path.unpack ss) f x;
45.17 +fun with_paths ss f x = Library.setmp load_path (! load_path @ map Path.explode ss) f x;
45.18 fun with_path s f x = with_paths [s] f x;
45.19
45.20 fun cond_add_path path f x =
45.21 @@ -95,7 +95,7 @@
45.22
45.23 fun load_file current raw_path =
45.24 (case check_file current raw_path of
45.25 - NONE => error ("Could not find ML file " ^ quote (Path.pack raw_path))
45.26 + NONE => error ("Could not find ML file " ^ quote (Path.implode raw_path))
45.27 | SOME (path, info) => (File.use path; (path, info)));
45.28
45.29
45.30 @@ -113,7 +113,7 @@
45.31 fun check_thy_aux (name, ml) =
45.32 let val thy_file = thy_path name in
45.33 case check_file NONE thy_file of
45.34 - NONE => error ("Could not find theory file " ^ quote (Path.pack thy_file) ^
45.35 + NONE => error ("Could not find theory file " ^ quote (Path.implode thy_file) ^
45.36 " in dir(s) " ^ commas_quote (show_path ()))
45.37 | SOME thy_info => (thy_info, if ml then check_file NONE (ml_path name) else NONE)
45.38 end;
46.1 --- a/src/Pure/Tools/codegen_names.ML Thu Dec 14 22:19:39 2006 +0100
46.2 +++ b/src/Pure/Tools/codegen_names.ML Fri Dec 15 00:08:06 2006 +0100
46.3 @@ -176,12 +176,12 @@
46.4 let
46.5 fun is_valid s = Symbol.is_ascii_letter s orelse Symbol.is_ascii_digit s orelse s = "'";
46.6 val is_junk = not o is_valid andf Symbol.not_eof;
46.7 - val junk = Scan.any is_junk;
46.8 + val junk = Scan.many is_junk;
46.9 val scan_valids = Symbol.scanner "Malformed input"
46.10 ((junk |--
46.11 - (Scan.optional (Scan.one Symbol.is_ascii_letter) "x" ^^ (Scan.any is_valid >> implode)
46.12 + (Scan.optional (Scan.one Symbol.is_ascii_letter) "x" ^^ (Scan.many is_valid >> implode)
46.13 --| junk))
46.14 - -- Scan.repeat ((Scan.any1 is_valid >> implode) --| junk) >> op ::);
46.15 + -- Scan.repeat ((Scan.many1 is_valid >> implode) --| junk) >> op ::);
46.16 in explode #> scan_valids #> space_implode "_" end;
46.17
46.18 fun purify_op "0" = "zero"
46.19 @@ -212,11 +212,11 @@
46.20
46.21 fun check_modulename mn =
46.22 let
46.23 - val mns = NameSpace.unpack mn;
46.24 + val mns = NameSpace.explode mn;
46.25 val mns' = map purify_upper mns;
46.26 in
46.27 if mns' = mns then mn else error ("Invalid module name: " ^ quote mn ^ "\n"
46.28 - ^ "perhaps try " ^ quote (NameSpace.pack mns'))
46.29 + ^ "perhaps try " ^ quote (NameSpace.implode mns'))
46.30 end
46.31
46.32 fun purify_var "" = "x"
46.33 @@ -234,9 +234,9 @@
46.34
46.35 fun policy thy get_basename get_thyname name =
46.36 let
46.37 - val prefix = (purify_prefix o NameSpace.unpack o get_thyname thy) name;
46.38 + val prefix = (purify_prefix o NameSpace.explode o get_thyname thy) name;
46.39 val base = (purify_base o get_basename) name;
46.40 - in NameSpace.pack (prefix @ [base]) end;
46.41 + in NameSpace.implode (prefix @ [base]) end;
46.42
46.43 fun class_policy thy = policy thy NameSpace.base thyname_of_class;
46.44 fun tyco_policy thy = policy thy NameSpace.base thyname_of_tyco;
46.45 @@ -258,10 +258,10 @@
46.46 case force_thyname thy (c, tys)
46.47 of NONE => policy thy NameSpace.base thyname_of_const c
46.48 | SOME thyname => let
46.49 - val prefix = (purify_prefix o NameSpace.unpack) thyname;
46.50 + val prefix = (purify_prefix o NameSpace.explode) thyname;
46.51 val tycos = map_filter (fn Type (tyco, _) => SOME tyco | _ => NONE) tys;
46.52 val base = map (purify_base o NameSpace.base) (c :: tycos);
46.53 - in NameSpace.pack (prefix @ [space_implode "_" base]) end;
46.54 + in NameSpace.implode (prefix @ [space_implode "_" base]) end;
46.55
46.56
46.57 (* shallow name spaces *)
46.58 @@ -274,20 +274,20 @@
46.59
46.60 fun add_nsp shallow name =
46.61 name
46.62 - |> NameSpace.unpack
46.63 + |> NameSpace.explode
46.64 |> split_last
46.65 |> apsnd (single #> cons shallow)
46.66 |> (op @)
46.67 - |> NameSpace.pack;
46.68 + |> NameSpace.implode;
46.69
46.70 fun dest_nsp nsp nspname =
46.71 let
46.72 - val xs = NameSpace.unpack nspname;
46.73 + val xs = NameSpace.explode nspname;
46.74 val (ys, base) = split_last xs;
46.75 val (module, shallow) = split_last ys;
46.76 in
46.77 if nsp = shallow
46.78 - then (SOME o NameSpace.pack) (module @ [base])
46.79 + then (SOME o NameSpace.implode) (module @ [base])
46.80 else NONE
46.81 end;
46.82
47.1 --- a/src/Pure/Tools/codegen_serializer.ML Thu Dec 14 22:19:39 2006 +0100
47.2 +++ b/src/Pure/Tools/codegen_serializer.ML Fri Dec 15 00:08:06 2006 +0100
47.3 @@ -235,7 +235,7 @@
47.4
47.5 fun dest_name name =
47.6 let
47.7 - val (names, name_base) = (split_last o NameSpace.unpack) name;
47.8 + val (names, name_base) = (split_last o NameSpace.explode) name;
47.9 val (names_mod, name_shallow) = split_last names;
47.10 in (names_mod, (name_shallow, name_base)) end;
47.11
47.12 @@ -257,7 +257,7 @@
47.13 fun dictvar v =
47.14 first_upper v ^ "_";
47.15 val label = translate_string (fn "." => "__" | c => c)
47.16 - o NameSpace.pack o op @ o apsnd single o apfst (fst o split_last) o split_last o NameSpace.unpack;
47.17 + o NameSpace.implode o op @ o apsnd single o apfst (fst o split_last) o split_last o NameSpace.explode;
47.18 fun pr_tyvar (v, []) =
47.19 str "()"
47.20 | pr_tyvar (v, sort) =
47.21 @@ -584,7 +584,7 @@
47.22 fun dictvar v =
47.23 first_upper v ^ "_";
47.24 val label = translate_string (fn "." => "__" | c => c)
47.25 - o NameSpace.pack o op @ o apsnd single o apfst (fst o split_last) o split_last o NameSpace.unpack;
47.26 + o NameSpace.implode o op @ o apsnd single o apfst (fst o split_last) o split_last o NameSpace.explode;
47.27 fun pr_tyvar (v, []) =
47.28 str "()"
47.29 | pr_tyvar (v, sort) =
47.30 @@ -924,9 +924,9 @@
47.31 val init_vars = CodegenThingol.make_vars (ML_Syntax.reserved_names @ reserved_user);
47.32 fun name_modl modl =
47.33 let
47.34 - val modlname = NameSpace.pack modl
47.35 + val modlname = NameSpace.implode modl
47.36 in case module_alias modlname
47.37 - of SOME modlname' => NameSpace.unpack modlname'
47.38 + of SOME modlname' => NameSpace.explode modlname'
47.39 | NONE => map (fn name => (the_single o fst)
47.40 (Name.variants [name] empty_names)) modl
47.41 end;
47.42 @@ -992,14 +992,14 @@
47.43 val (modl'', defname'') = (apfst name_modl o dest_name) name'';
47.44 in if modl' = modl'' then
47.45 map_node modl'
47.46 - (Graph.add_edge (NameSpace.pack (modl @ [fst defname, snd defname]), name''))
47.47 + (Graph.add_edge (NameSpace.implode (modl @ [fst defname, snd defname]), name''))
47.48 else let
47.49 val (common, (diff1::_, diff2::_)) = chop_prefix (op =) (modl', modl'');
47.50 in
47.51 map_node common
47.52 (fn gr => Graph.add_edge_acyclic (diff1, diff2) gr
47.53 handle Graph.CYCLES _ => error ("Dependency "
47.54 - ^ quote (NameSpace.pack (modl' @ [fst defname, snd defname]))
47.55 + ^ quote (NameSpace.implode (modl' @ [fst defname, snd defname]))
47.56 ^ " -> " ^ quote name'' ^ " would result in module dependency cycle"))
47.57 end end;
47.58 in
47.59 @@ -1039,7 +1039,7 @@
47.60 |> fold (fn m => fn g => case Graph.get_node g m
47.61 of Module (_, (_, g)) => g) modl'
47.62 |> (fn g => case Graph.get_node g name of Def (defname, _) => defname);
47.63 - in NameSpace.pack (remainder @ [defname']) end handle Graph.UNDEF _ =>
47.64 + in NameSpace.implode (remainder @ [defname']) end handle Graph.UNDEF _ =>
47.65 "(raise Fail \"undefined name " ^ name ^ "\")";
47.66 fun the_prolog modlname = case module_prolog modlname
47.67 of NONE => []
47.68 @@ -1049,7 +1049,7 @@
47.69 | pr_node prefix (Def (_, SOME def)) =
47.70 SOME (pr_def tyco_syntax const_syntax init_vars (deresolver prefix) def)
47.71 | pr_node prefix (Module (dmodlname, (_, nodes))) =
47.72 - SOME (pr_modl dmodlname (the_prolog (NameSpace.pack (prefix @ [dmodlname]))
47.73 + SOME (pr_modl dmodlname (the_prolog (NameSpace.implode (prefix @ [dmodlname]))
47.74 @ separate (str "") ((map_filter (pr_node (prefix @ [dmodlname]) o Graph.get_node nodes)
47.75 o rev o flat o Graph.strong_conn) nodes)));
47.76 val p = pr_modl "ROOT" (the_prolog "" @ separate (str "") ((map_filter
47.77 @@ -1058,7 +1058,7 @@
47.78
47.79 val isar_seri_sml =
47.80 let
47.81 - fun output_file file p = File.write (Path.unpack file) (Pretty.output p ^ "\n");
47.82 + fun output_file file p = File.write (Path.explode file) (Pretty.output p ^ "\n");
47.83 fun output_diag p = Pretty.writeln p;
47.84 fun output_internal p = use_text Output.ml_output false (Pretty.output p);
47.85 in
47.86 @@ -1070,7 +1070,7 @@
47.87
47.88 val isar_seri_ocaml =
47.89 let
47.90 - fun output_file file p = File.write (Path.unpack file) (Pretty.output p ^ "\n");
47.91 + fun output_file file p = File.write (Path.explode file) (Pretty.output p ^ "\n");
47.92 fun output_diag p = Pretty.writeln p;
47.93 in
47.94 parse_args ((Args.$$$ "-" >> K output_diag
47.95 @@ -1330,16 +1330,16 @@
47.96 fun seri_haskell module_prefix destination string_classes reserved_user module_alias module_prolog
47.97 class_syntax tyco_syntax const_syntax code =
47.98 let
47.99 - val _ = Option.map File.assert destination;
47.100 + val _ = Option.map File.check destination;
47.101 val empty_names = Name.make_context (reserved_haskell @ reserved_user);
47.102 fun name_modl modl =
47.103 let
47.104 - val modlname = NameSpace.pack modl
47.105 + val modlname = NameSpace.implode modl
47.106 in (modlname, case module_alias modlname
47.107 of SOME modlname' => (case module_prefix
47.108 of NONE => modlname'
47.109 | SOME module_prefix => NameSpace.append module_prefix modlname')
47.110 - | NONE => NameSpace.pack (map_filter I (module_prefix :: map (fn name => (SOME o the_single o fst)
47.111 + | NONE => NameSpace.implode (map_filter I (module_prefix :: map (fn name => (SOME o the_single o fst)
47.112 (Name.variants [name] empty_names)) modl)))
47.113 end;
47.114 fun add_def (name, (def, deps)) =
47.115 @@ -1409,8 +1409,8 @@
47.116 fun write_module (SOME destination) modlname p =
47.117 let
47.118 val filename = case modlname
47.119 - of "" => Path.unpack "Main.hs"
47.120 - | _ => (Path.ext "hs" o Path.unpack o implode o separate "/" o NameSpace.unpack) modlname;
47.121 + of "" => Path.explode "Main.hs"
47.122 + | _ => (Path.ext "hs" o Path.explode o implode o separate "/" o NameSpace.explode) modlname;
47.123 val pathname = Path.append destination filename;
47.124 val _ = File.mkdir (Path.dir pathname);
47.125 in File.write pathname (Pretty.setmp_margin 999999 Pretty.output p ^ "\n") end
47.126 @@ -1435,7 +1435,7 @@
47.127 -- Scan.optional (Args.$$$ "string_classes" >> K true) false
47.128 -- (Args.$$$ "-" >> K NONE || Args.name >> SOME)
47.129 >> (fn ((module_prefix, string_classes), destination) =>
47.130 - seri_haskell module_prefix (Option.map Path.unpack destination) string_classes));
47.131 + seri_haskell module_prefix (Option.map Path.explode destination) string_classes));
47.132
47.133
47.134 (** diagnosis serializer **)
48.1 --- a/src/Pure/codegen.ML Thu Dec 14 22:19:39 2006 +0100
48.2 +++ b/src/Pure/codegen.ML Fri Dec 15 00:08:06 2006 +0100
48.3 @@ -443,7 +443,7 @@
48.4 | (true, "isup") => "" :: check_str zs
48.5 | (ctrl, s') => (if ctrl then "ctrl_" ^ s' else s') :: check_str zs)
48.6 | (ys, zs) => implode ys :: check_str zs);
48.7 - val s' = space_implode "_" (maps (check_str o Symbol.explode) (NameSpace.unpack s))
48.8 + val s' = space_implode "_" (maps (check_str o Symbol.explode) (NameSpace.explode s))
48.9 in
48.10 if Symbol.is_ascii_letter (hd (explode s')) then s' else "id_" ^ s'
48.11 end;
48.12 @@ -453,7 +453,7 @@
48.13 fun find_name [] = sys_error "mk_long_id"
48.14 | find_name (ys :: yss) =
48.15 let
48.16 - val s' = NameSpace.pack ys
48.17 + val s' = NameSpace.implode ys
48.18 val s'' = NameSpace.append module s'
48.19 in case Symtab.lookup used s'' of
48.20 NONE => ((module, s'),
48.21 @@ -462,7 +462,7 @@
48.22 | SOME _ => find_name yss
48.23 end
48.24 in case Symtab.lookup tab s of
48.25 - NONE => find_name (Library.suffixes1 (NameSpace.unpack s))
48.26 + NONE => find_name (Library.suffixes1 (NameSpace.explode s))
48.27 | SOME name => (name, p)
48.28 end;
48.29
48.30 @@ -874,9 +874,9 @@
48.31 fun gen_generate_code prep_term thy modules module =
48.32 setmp print_mode [] (Pretty.setmp_margin (!margin) (fn xs =>
48.33 let
48.34 - val _ = assert (module <> "" orelse
48.35 + val _ = (module <> "" orelse
48.36 member (op =) (!mode) "library" andalso forall (equal "" o fst) xs)
48.37 - "missing module name";
48.38 + orelse error "missing module name";
48.39 val graphs = get_modules thy;
48.40 val defs = mk_deftab thy;
48.41 val gr = new_node ("<Top>", (NONE, module, ""))
48.42 @@ -958,10 +958,10 @@
48.43
48.44 fun test_term thy sz i t =
48.45 let
48.46 - val _ = assert (null (term_tvars t) andalso null (term_tfrees t))
48.47 - "Term to be tested contains type variables";
48.48 - val _ = assert (null (term_vars t))
48.49 - "Term to be tested contains schematic variables";
48.50 + val _ = (null (term_tvars t) andalso null (term_tfrees t)) orelse
48.51 + error "Term to be tested contains type variables";
48.52 + val _ = null (term_vars t) orelse
48.53 + error "Term to be tested contains schematic variables";
48.54 val frees = map dest_Free (term_frees t);
48.55 val frees' = frees ~~
48.56 map (fn i => "arg" ^ string_of_int i) (1 upto length frees);
48.57 @@ -1028,10 +1028,10 @@
48.58
48.59 fun eval_term thy = setmp print_mode [] (fn t =>
48.60 let
48.61 - val _ = assert (null (term_tvars t) andalso null (term_tfrees t))
48.62 - "Term to be evaluated contains type variables";
48.63 - val _ = assert (null (term_vars t) andalso null (term_frees t))
48.64 - "Term to be evaluated contains variables";
48.65 + val _ = (null (term_tvars t) andalso null (term_tfrees t)) orelse
48.66 + error "Term to be evaluated contains type variables";
48.67 + val _ = (null (term_vars t) andalso null (term_frees t)) orelse
48.68 + error "Term to be evaluated contains variables";
48.69 val (code, gr) = setmp mode ["term_of"]
48.70 (generate_code_i thy [] "Generated") [("result", t)];
48.71 val s = "structure EvalTerm =\nstruct\n\n" ^
48.72 @@ -1155,10 +1155,10 @@
48.73 | SOME fname =>
48.74 if lib then
48.75 app (fn (name, s) => File.write
48.76 - (Path.append (Path.unpack fname) (Path.basic (name ^ ".ML"))) s)
48.77 + (Path.append (Path.explode fname) (Path.basic (name ^ ".ML"))) s)
48.78 (("ROOT", implode (map (fn (name, _) =>
48.79 "use \"" ^ name ^ ".ML\";\n") code)) :: code)
48.80 - else File.write (Path.unpack fname) (snd (hd code)));
48.81 + else File.write (Path.explode fname) (snd (hd code)));
48.82 if lib then thy
48.83 else map_modules (Symtab.update (module, gr)) thy)
48.84 end));
49.1 --- a/src/Pure/proof_general.ML Thu Dec 14 22:19:39 2006 +0100
49.2 +++ b/src/Pure/proof_general.ML Fri Dec 15 00:08:06 2006 +0100
49.3 @@ -402,7 +402,7 @@
49.4
49.5 (* prepare theory context *)
49.6
49.7 -val thy_name = Path.pack o #1 o Path.split_ext o Path.base o Path.unpack;
49.8 +val thy_name = Path.implode o #1 o Path.split_ext o Path.base o Path.explode;
49.9
49.10 (* FIXME general treatment of tracing*)
49.11 val update_thy_only = setmp MetaSimplifier.trace_simp false ThyInfo.update_thy_only;
49.12 @@ -413,7 +413,7 @@
49.13 | NONE => "");
49.14
49.15 fun try_update_thy_only file =
49.16 - ThyLoad.cond_add_path (Path.dir (Path.unpack file)) (fn () =>
49.17 + ThyLoad.cond_add_path (Path.dir (Path.explode file)) (fn () =>
49.18 let val name = thy_name file in
49.19 if is_some (ThyLoad.check_file NONE (ThyLoad.thy_path name))
49.20 then update_thy_only name
49.21 @@ -433,13 +433,13 @@
49.22 (ThyInfo.touch_child_thys name;
49.23 ThyInfo.pretend_use_thy_only name handle ERROR msg =>
49.24 (warning msg; warning ("Failed to register theory: " ^ quote name);
49.25 - tell_file_retracted (Path.base (Path.unpack file))))
49.26 + tell_file_retracted (Path.base (Path.explode file))))
49.27 else raise Toplevel.UNDEF
49.28 end;
49.29
49.30 fun vacuous_inform_file_processed file state =
49.31 (warning ("No theory " ^ quote (thy_name file));
49.32 - tell_file_retracted (Path.base (Path.unpack file)));
49.33 + tell_file_retracted (Path.base (Path.explode file)));
49.34
49.35
49.36 (* restart top-level loop (keeps most state information) *)
49.37 @@ -653,7 +653,7 @@
49.38 in
49.39 fun send_pgip_config () =
49.40 let
49.41 - val path = Path.unpack (config_file())
49.42 + val path = Path.explode (config_file())
49.43 val exists = File.exists path
49.44 val proverinfo =
49.45 XML.element "proverinfo"
49.46 @@ -678,7 +678,7 @@
49.47 fun send_informguise (openfile, opentheory, openproofpos) =
49.48 let val guisefile =
49.49 case openfile of SOME f => [XML.element "guisefile"
49.50 - [("url",Url.pack (Url.File (Path.unpack f)))] []]
49.51 + [("url",Url.implode (Url.File (Path.explode f)))] []]
49.52 | _ => []
49.53 val guisetheory =
49.54 case opentheory of SOME t => [XML.element "guisetheory" [("thyname", t)] []]
49.55 @@ -1172,11 +1172,11 @@
49.56
49.57 fun use_thy_or_ml_file file =
49.58 let
49.59 - val (path,extn) = Path.split_ext (Path.unpack file)
49.60 + val (path,extn) = Path.split_ext (Path.explode file)
49.61 in
49.62 case extn of
49.63 - "" => isarcmd ("use_thy " ^ (quote (Path.pack path)))
49.64 - | "thy" => isarcmd ("use_thy " ^ (quote (Path.pack path)))
49.65 + "" => isarcmd ("use_thy " ^ (quote (Path.implode path)))
49.66 + | "thy" => isarcmd ("use_thy " ^ (quote (Path.implode path)))
49.67 | "ML" => isarcmd ("use " ^ quote file)
49.68 | other => error ("Don't know how to read a file with extension " ^ other)
49.69 end
49.70 @@ -1199,7 +1199,7 @@
49.71 val name_attr = xmlattr "name"
49.72
49.73 fun localfile_of_url url = (* only handle file:/// or file://localhost/ *)
49.74 - case Url.unpack url of
49.75 + case Url.explode url of
49.76 (Url.File path) => File.platform_path path
49.77 | _ => error ("Cannot access non-local URL " ^ url)
49.78
49.79 @@ -1515,7 +1515,7 @@
49.80
49.81 fun write_keywords s =
49.82 (init_outer_syntax ();
49.83 - File.write (Path.unpack ("isar-keywords" ^ (if s = "" then "" else "-" ^ s) ^".el"))
49.84 + File.write (Path.explode ("isar-keywords" ^ (if s = "" then "" else "-" ^ s) ^".el"))
49.85 (make_elisp_syntax (OuterSyntax.dest_keywords (), OuterSyntax.dest_parsers ())));
49.86
49.87 end;
50.1 --- a/src/Pure/type.ML Thu Dec 14 22:19:39 2006 +0100
50.2 +++ b/src/Pure/type.ML Fri Dec 15 00:08:06 2006 +0100
50.3 @@ -535,7 +535,8 @@
50.4 fun map_types f = map_tsig (fn (classes, default, types) =>
50.5 let
50.6 val (space', tab') = f types;
50.7 - val _ = assert (NameSpace.intern space' "dummy" = "dummy") "Illegal declaration of dummy type";
50.8 + val _ = NameSpace.intern space' "dummy" = "dummy" orelse
50.9 + error "Illegal declaration of dummy type";
50.10 in (classes, default, (space', tab')) end);
50.11
50.12 fun syntactic types (Type (c, Ts)) =