# HG changeset patch
# User wenzelm
# Date 1309432901 -7200
# Node ID 8c89a1fb30f230079aa584c35f02cb1f96bda164
# Parent  fd650d6592756065d0568d9aeadc5abae36f57ef
standardized use of Path operations;

diff -r fd650d659275 -r 8c89a1fb30f2 src/HOL/Matrix/Compute_Oracle/am_ghc.ML
--- 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
diff -r fd650d659275 -r 8c89a1fb30f2 src/HOL/Matrix/Cplex_tools.ML
--- 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 =
diff -r fd650d659275 -r 8c89a1fb30f2 src/HOL/Tools/ATP/atp_proof.ML
--- 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 \
diff -r fd650d659275 -r 8c89a1fb30f2 src/HOL/Tools/Nitpick/nitpick.ML
--- 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
diff -r fd650d659275 -r 8c89a1fb30f2 src/HOL/Tools/Quickcheck/narrowing_generators.ML
--- 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;
 
diff -r fd650d659275 -r 8c89a1fb30f2 src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML
--- 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. *)
diff -r fd650d659275 -r 8c89a1fb30f2 src/HOL/ex/atp_export.ML
--- 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
diff -r fd650d659275 -r 8c89a1fb30f2 src/Tools/WWW_Find/unicode_symbols.ML
--- 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;