--- a/src/HOL/Matrix/Compute_Oracle/am_ghc.ML Thu Jun 30 11:15:36 2011 +0200
+++ b/src/HOL/Matrix/Compute_Oracle/am_ghc.ML Thu Jun 30 13:21:41 2011 +0200
@@ -210,7 +210,7 @@
string_of_int (Time.toMicroseconds (Time.now ())) ^ string_of_int c
end
-fun tmp_file s = Path.implode (Path.expand (File.tmp_path (Path.make [s])));
+fun tmp_file s = Path.implode (Path.expand (File.tmp_path (Path.basic s)));
fun wrap s = "\""^s^"\""
fun writeTextFile name s = File.write (Path.explode name) s
--- a/src/HOL/Matrix/Cplex_tools.ML Thu Jun 30 11:15:36 2011 +0200
+++ b/src/HOL/Matrix/Cplex_tools.ML Thu Jun 30 13:21:41 2011 +0200
@@ -1129,7 +1129,7 @@
exception Execute of string;
-fun tmp_file s = Path.implode (Path.expand (File.tmp_path (Path.make [s])));
+fun tmp_file s = Path.implode (Path.expand (File.tmp_path (Path.basic s)));
fun wrap s = "\""^s^"\"";
fun solve_glpk prog =
--- a/src/HOL/Tools/ATP/atp_proof.ML Thu Jun 30 11:15:36 2011 +0200
+++ b/src/HOL/Tools/ATP/atp_proof.ML Thu Jun 30 13:21:41 2011 +0200
@@ -142,9 +142,7 @@
\TPTP syntax. To install it, download and extract the package \
\\"http://isabelle.in.tum.de/dist/contrib/spass-3.7.tar.gz\" and add the \
\\"spass-3.7\" directory's absolute path to " ^
- Path.print (Path.expand (Path.appends
- (Path.variable "ISABELLE_HOME_USER" ::
- map Path.basic ["etc", "components"]))) ^
+ Path.print (Path.expand (Path.explode "$ISABELLE_HOME_USER/etc/components")) ^
" on a line of its own."
| string_for_failure VampireTooOld =
"Isabelle requires a more recent version of Vampire. To install it, follow \
--- a/src/HOL/Tools/Nitpick/nitpick.ML Thu Jun 30 11:15:36 2011 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick.ML Thu Jun 30 13:21:41 2011 +0200
@@ -183,9 +183,8 @@
"Nitpick requires the external Java program Kodkodi. To install it, download \
\the package from Isabelle's web page and add the \"kodkodi-x.y.z\" \
\directory's full path to " ^
- Path.print (Path.expand (Path.appends
- (Path.variable "ISABELLE_HOME_USER" ::
- map Path.basic ["etc", "components"]))) ^ " on a line of its own."
+ Path.print (Path.expand (Path.explode "$ISABELLE_HOME_USER/etc/components")) ^
+ " on a line of its own."
val max_unsound_delay_ms = 200
val max_unsound_delay_percent = 2
--- a/src/HOL/Tools/Quickcheck/narrowing_generators.ML Thu Jun 30 11:15:36 2011 +0200
+++ b/src/HOL/Tools/Quickcheck/narrowing_generators.ML Thu Jun 30 13:21:41 2011 +0200
@@ -206,7 +206,8 @@
fun with_overlord_dir name f =
let
- val path = Path.append (Path.explode "~/.isabelle") (Path.basic (name ^ serial_string ()))
+ val path =
+ Path.append (Path.explode "$ISABELLE_HOME_USER") (Path.basic (name ^ serial_string ()))
val _ = Isabelle_System.mkdirs path;
in Exn.release (Exn.capture f path) end;
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Thu Jun 30 11:15:36 2011 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Thu Jun 30 13:21:41 2011 +0200
@@ -703,7 +703,7 @@
|> fold maybe_run_slice actual_slices
end
else
- error ("Bad executable: " ^ Path.print command ^ ".")
+ error ("Bad executable: " ^ Path.print command)
(* If the problem file has not been exported, remove it; otherwise, export
the proof file too. *)
--- a/src/HOL/ex/atp_export.ML Thu Jun 30 11:15:36 2011 +0200
+++ b/src/HOL/ex/atp_export.ML Thu Jun 30 13:21:41 2011 +0200
@@ -112,7 +112,7 @@
fun run_some_atp ctxt problem =
let
val thy = Proof_Context.theory_of ctxt
- val prob_file = Path.explode "/tmp/prob.tptp"
+ val prob_file = Path.explode "/tmp/prob.tptp" (* FIXME File.tmp_path (?) *)
val {exec, arguments, proof_delims, known_failures, ...} =
get_atp thy spassN
val _ = problem |> tptp_lines_for_atp_problem FOF
--- a/src/Tools/WWW_Find/unicode_symbols.ML Thu Jun 30 11:15:36 2011 +0200
+++ b/src/Tools/WWW_Find/unicode_symbols.ML Thu Jun 30 13:21:41 2011 +0200
@@ -135,11 +135,6 @@
val line = (symbol -- unicode --| font -- abbr) >> Parse.triple1;
-val symbols_path =
- [getenv "ISABELLE_HOME", "etc", "symbols"]
- |> map Path.explode
- |> Path.appends;
-
end;
local (* build tables *)
@@ -164,8 +159,7 @@
fun read_symbols path =
let
val parsed_lines =
- File.read path
- |> (fn x => Symbol_Pos.explode (x, Position.file (Path.implode path)))
+ Symbol_Pos.explode (File.read path, Path.position path)
|> tokenize
|> filter is_proper
|> Scan.finite stopper (Scan.repeat line)
@@ -179,7 +173,7 @@
end;
local
-val (fromsym, fromabbr, tosym, toabbr) = read_symbols symbols_path;
+val (fromsym, fromabbr, tosym, toabbr) = read_symbols (Path.explode "~~/etc/symbols");
in
val symbol_to_unicode = Symtab.lookup fromsym;
val abbrev_to_unicode = Symtab.lookup fromabbr;