# HG changeset patch
# User wenzelm
# Date 1476524283 -7200
# Node ID e7cbf81ec4b7fc5bafc8380daf07f304252c7b5a
# Parent  c1af670cbe7eaf05d177e9dbdfba69cffb7131bd
prefer Isabelle standard Path;

diff -r c1af670cbe7e -r e7cbf81ec4b7 src/Pure/Admin/build_doc.scala
--- a/src/Pure/Admin/build_doc.scala	Sat Oct 15 11:26:31 2016 +0200
+++ b/src/Pure/Admin/build_doc.scala	Sat Oct 15 11:38:03 2016 +0200
@@ -50,14 +50,14 @@
             Build.build(
               options.bool.update("browser_info", false).
                 string.update("document", "pdf").
-                string.update("document_output", File.standard_path(output)),
+                string.update("document_output", output.implode),
               progress, clean_build = true, max_jobs = max_jobs, system_mode = system_mode,
               sessions = sessions)
           if (res2.ok) {
-            val doc_dir = Path.explode("$ISABELLE_HOME/doc").file
+            val doc_dir = Path.explode("$ISABELLE_HOME/doc")
             for (doc <- selected_docs) {
-              val name = doc + ".pdf"
-              File.copy(new JFile(output, name), new JFile(doc_dir, name))
+              val name = Path.explode(doc + ".pdf")
+              File.copy(output + name, doc_dir + name)
             }
           }
           res2.rc
diff -r c1af670cbe7e -r e7cbf81ec4b7 src/Pure/Admin/build_stats.scala
--- a/src/Pure/Admin/build_stats.scala	Sat Oct 15 11:26:31 2016 +0200
+++ b/src/Pure/Admin/build_stats.scala	Sat Oct 15 11:38:03 2016 +0200
@@ -85,7 +85,6 @@
               case Some(true) => plots2
             }
 
-          val data_file_name = File.standard_path(data_file.getAbsolutePath)
           File.write(plot_file, """
 set terminal png size """ + size._1 + "," + size._2 + """
 set output """ + quote(File.standard_path(dir + Path.basic(session + ".png"))) + """
@@ -94,7 +93,7 @@
 set format x "%d-%b"
 set xlabel """ + quote(session) + """ noenhanced
 set key left top
-plot [] [0:] """ + plots.map(s => quote(data_file_name) + " " + s).mkString(", ") + "\n")
+plot [] [0:] """ + plots.map(s => quote(data_file.implode) + " " + s).mkString(", ") + "\n")
           val result = Isabelle_System.bash("\"$ISABELLE_GNUPLOT\" " + File.bash_path(plot_file))
           if (result.rc != 0) {
             Output.error_message("Session " + session + ": gnuplot error")
diff -r c1af670cbe7e -r e7cbf81ec4b7 src/Pure/Admin/isabelle_cronjob.scala
--- a/src/Pure/Admin/isabelle_cronjob.scala	Sat Oct 15 11:26:31 2016 +0200
+++ b/src/Pure/Admin/isabelle_cronjob.scala	Sat Oct 15 11:38:03 2016 +0200
@@ -66,10 +66,8 @@
 
   private val build_release =
     Logger_Task("build_release", logger =>
-      Isabelle_System.with_tmp_dir("isadist")(tmp_dir =>
+      Isabelle_System.with_tmp_dir("isadist")(base_dir =>
         {
-          val base_dir = File.path(tmp_dir)
-
           val new_snapshot = release_snapshot.ext("new")
           val old_snapshot = release_snapshot.ext("old")
 
diff -r c1af670cbe7e -r e7cbf81ec4b7 src/Pure/General/file.scala
--- a/src/Pure/General/file.scala	Sat Oct 15 11:26:31 2016 +0200
+++ b/src/Pure/General/file.scala	Sat Oct 15 11:38:03 2016 +0200
@@ -47,6 +47,8 @@
 
   def standard_path(file: JFile): String = standard_path(file.getPath)
 
+  def path(file: JFile): Path = Path.explode(standard_path(file))
+
   def standard_url(name: String): String =
     try {
       val url = new URL(name)
@@ -56,8 +58,6 @@
     }
     catch { case _: MalformedURLException => standard_path(name) }
 
-  def path(file: JFile): Path = Path.explode(standard_path(file.getAbsolutePath))
-
 
   /* platform path (Windows or Posix) */
 
diff -r c1af670cbe7e -r e7cbf81ec4b7 src/Pure/System/isabelle_system.scala
--- a/src/Pure/System/isabelle_system.scala	Sat Oct 15 11:26:31 2016 +0200
+++ b/src/Pure/System/isabelle_system.scala	Sat Oct 15 11:38:03 2016 +0200
@@ -202,10 +202,10 @@
     file
   }
 
-  def with_tmp_file[A](name: String, ext: String = "")(body: JFile => A): A =
+  def with_tmp_file[A](name: String, ext: String = "")(body: Path => A): A =
   {
     val file = tmp_file(name, ext)
-    try { body(file) } finally { file.delete }
+    try { body(File.path(file)) } finally { file.delete }
   }
 
 
@@ -245,10 +245,10 @@
     dir
   }
 
-  def with_tmp_dir[A](name: String)(body: JFile => A): A =
+  def with_tmp_dir[A](name: String)(body: Path => A): A =
   {
     val dir = tmp_dir(name)
-    try { body(dir) } finally { rm_tree(dir) }
+    try { body(File.path(dir)) } finally { rm_tree(dir) }
   }