tuned signature, according to ML version;

--- a/src/Pure/General/file.scala	Thu Aug 20 17:41:50 2015 +0100
+++ b/src/Pure/General/file.scala	Thu Aug 20 19:15:17 2015 +0200
@@ -17,6 +17,27 @@
 
 object File
 {
+  /* system path representations */
+
+  def standard_path(path: Path): String = path.expand.implode
+
+  def platform_path(path: Path): String = Isabelle_System.jvm_path(standard_path(path))
+  def platform_file(path: Path): JFile = new JFile(platform_path(path))
+
+  def platform_file_url(raw_path: Path): String =
+  {
+    val path = raw_path.expand
+    require(path.is_absolute)
+    val s = platform_path(path).replaceAll(" ", "%20")
+    if (!Platform.is_windows) "file://" + s
+    else if (s.startsWith("\\\\")) "file:" + s.replace('\\', '/')
+    else "file:///" + s.replace('\\', '/')
+  }
+
+  def shell_path(path: Path): String = "'" + standard_path(path) + "'"
+  def shell_path(file: JFile): String = "'" + Isabelle_System.posix_path(file) + "'"
+
+
   /* directory content */
 
   def read_dir(dir: Path): List[String] =

--- a/src/Pure/General/path.scala	Thu Aug 20 17:41:50 2015 +0100
+++ b/src/Pure/General/path.scala	Thu Aug 20 19:15:17 2015 +0200
@@ -205,7 +205,7 @@
 
   /* platform file */
 
-  def file: JFile = Isabelle_System.platform_file(this)
+  def file: JFile = File.platform_file(this)
   def is_file: Boolean = file.isFile
   def is_dir: Boolean = file.isDirectory
 }

--- a/src/Pure/System/isabelle_system.scala	Thu Aug 20 17:41:50 2015 +0100
+++ b/src/Pure/System/isabelle_system.scala	Thu Aug 20 19:15:17 2015 +0200
@@ -219,27 +219,6 @@
     catch { case _: MalformedURLException => posix_path(name) }
 
 
-  /* misc path specifications */
-
-  def standard_path(path: Path): String = path.expand.implode
-
-  def platform_path(path: Path): String = jvm_path(standard_path(path))
-  def platform_file(path: Path): JFile = new JFile(platform_path(path))
-
-  def platform_file_url(raw_path: Path): String =
-  {
-    val path = raw_path.expand
-    require(path.is_absolute)
-    val s = platform_path(path).replaceAll(" ", "%20")
-    if (!Platform.is_windows) "file://" + s
-    else if (s.startsWith("\\\\")) "file:" + s.replace('\\', '/')
-    else "file:///" + s.replace('\\', '/')
-  }
-
-  def shell_path(path: Path): String = "'" + standard_path(path) + "'"
-  def shell_path(file: JFile): String = "'" + posix_path(file) + "'"
-
-
   /* source files of Isabelle/ML bootstrap */
 
   def source_file(path: Path): Option[Path] =
@@ -259,8 +238,8 @@
 
   def mkdirs(path: Path): Unit =
     if (!path.is_dir) {
-      bash("perl -e \"use File::Path make_path; make_path(" + shell_path(path) + ");\"")
-      if (!path.is_dir) error("Failed to create directory: " + quote(platform_path(path)))
+      bash("perl -e \"use File::Path make_path; make_path(" + File.shell_path(path) + ");\"")
+      if (!path.is_dir) error("Failed to create directory: " + quote(File.platform_path(path)))
     }
 
 
@@ -320,7 +299,7 @@
   class Managed_Process(cwd: JFile, env: Map[String, String], redirect: Boolean, args: String*)
   {
     private val params =
-      List(standard_path(Path.explode("~~/lib/scripts/process")), "group", "-", "no_script")
+      List(File.standard_path(Path.explode("~~/lib/scripts/process")), "group", "-", "no_script")
     private val proc = execute_env(cwd, env, redirect, (params ::: args.toList):_*)
 
 
@@ -390,7 +369,7 @@
   {
     val path = Path.explode("$ISABELLE_TMP_PREFIX")
     path.file.mkdirs  // low-level mkdirs
-    platform_file(path)
+    File.platform_file(path)
   }
 
   def tmp_file[A](name: String, ext: String = ""): JFile =
@@ -523,7 +502,7 @@
       catch { case _: SecurityException => false }
     } match {
       case Some(dir) =>
-        val file = standard_path(dir + Path.basic(name))
+        val file = File.standard_path(dir + Path.basic(name))
         process_output(execute(true, (List(file) ::: args.toList): _*))
       case None => ("Unknown Isabelle tool: " + name, 2)
     }
@@ -533,10 +512,10 @@
     bash("exec \"$ISABELLE_OPEN\" '" + arg + "' >/dev/null 2>/dev/null &")
 
   def pdf_viewer(arg: Path): Unit =
-    bash("exec \"$PDF_VIEWER\" '" + standard_path(arg) + "' >/dev/null 2>/dev/null &")
+    bash("exec \"$PDF_VIEWER\" '" + File.standard_path(arg) + "' >/dev/null 2>/dev/null &")
 
   def hg(cmd_line: String, cwd: Path = Path.current): Bash_Result =
-    bash("cd " + shell_path(cwd) + " && \"${HG:-hg}\" " + cmd_line)
+    bash("cd " + File.shell_path(cwd) + " && \"${HG:-hg}\" " + cmd_line)
 
 
   /** Isabelle resources **/

--- a/src/Pure/Tools/build.scala	Thu Aug 20 17:41:50 2015 +0100
+++ b/src/Pure/Tools/build.scala	Thu Aug 20 19:15:17 2015 +0200
@@ -591,7 +591,7 @@
         }))
 
     private val env =
-      Map("INPUT" -> parent, "TARGET" -> name, "OUTPUT" -> Isabelle_System.standard_path(output),
+      Map("INPUT" -> parent, "TARGET" -> name, "OUTPUT" -> File.standard_path(output),
         (if (is_pure(name)) "ISABELLE_PROCESS_OPTIONS" else "ARGS_FILE") ->
           Isabelle_System.posix_path(args_file))
 

--- a/src/Pure/Tools/check_source.scala	Thu Aug 20 17:41:50 2015 +0100
+++ b/src/Pure/Tools/check_source.scala	Thu Aug 20 19:15:17 2015 +0200
@@ -41,7 +41,7 @@
   def check_hg(root: Path)
   {
     Output.writeln("Checking " + root + " ...")
-    Isabelle_System.hg("--repository " + Isabelle_System.shell_path(root) + " root").check_error
+    Isabelle_System.hg("--repository " + File.shell_path(root) + " root").check_error
     for {
       file <- Isabelle_System.hg("manifest", root).check_error.out_lines
       if file.endsWith(".thy") || file.endsWith(".ML")

--- a/src/Pure/Tools/main.scala	Thu Aug 20 17:41:50 2015 +0100
+++ b/src/Pure/Tools/main.scala	Thu Aug 20 19:15:17 2015 +0200
@@ -102,11 +102,11 @@
             Isabelle_System.getenv_strict("JEDIT_OPTIONS").split(" +")
 
           val jedit_settings =
-            Array("-settings=" + Isabelle_System.platform_path(Path.explode("$JEDIT_SETTINGS")))
+            Array("-settings=" + File.platform_path(Path.explode("$JEDIT_SETTINGS")))
 
           val more_args =
             if (args.isEmpty)
-              Array(Isabelle_System.platform_path(Path.explode("$USER_HOME/Scratch.thy")))
+              Array(File.platform_path(Path.explode("$USER_HOME/Scratch.thy")))
             else args
 
 
@@ -114,11 +114,8 @@
 
           update_environment()
 
-          System.setProperty("jedit.home",
-            Isabelle_System.platform_path(Path.explode("$JEDIT_HOME/dist")))
-
-          System.setProperty("scala.home",
-            Isabelle_System.platform_path(Path.explode("$SCALA_HOME")))
+          System.setProperty("jedit.home", File.platform_path(Path.explode("$JEDIT_HOME/dist")))
+          System.setProperty("scala.home", File.platform_path(Path.explode("$SCALA_HOME")))
 
           val jedit =
             Class.forName("org.gjt.sp.jedit.jEdit", true, ClassLoader.getSystemClassLoader)

--- a/src/Tools/jEdit/src/documentation_dockable.scala	Thu Aug 20 17:41:50 2015 +0100
+++ b/src/Tools/jEdit/src/documentation_dockable.scala	Thu Aug 20 19:15:17 2015 +0200
@@ -54,10 +54,10 @@
   {
     node.getUserObject match {
       case Text_File(_, path) =>
-        PIDE.editor.goto_file(true, view, Isabelle_System.platform_path(path))
+        PIDE.editor.goto_file(true, view, File.platform_path(path))
       case Documentation(_, _, path) =>
         if (path.is_file)
-          PIDE.editor.goto_file(true, view, Isabelle_System.platform_path(path))
+          PIDE.editor.goto_file(true, view, File.platform_path(path))
         else {
           Future.fork {
             try { Doc.view(path) }

--- a/src/Tools/jEdit/src/jedit_editor.scala	Thu Aug 20 17:41:50 2015 +0100
+++ b/src/Tools/jEdit/src/jedit_editor.scala	Thu Aug 20 19:15:17 2015 +0200
@@ -225,7 +225,7 @@
       if (Path.is_wellformed(source_name)) {
         if (Path.is_valid(source_name)) {
           val path = Path.explode(source_name)
-          Some(Isabelle_System.platform_path(Isabelle_System.source_file(path) getOrElse path))
+          Some(File.platform_path(Isabelle_System.source_file(path) getOrElse path))
         }
         else None
       }

--- a/src/Tools/jEdit/src/jedit_lib.scala	Thu Aug 20 17:41:50 2015 +0100
+++ b/src/Tools/jEdit/src/jedit_lib.scala	Thu Aug 20 19:15:17 2015 +0200
@@ -308,8 +308,7 @@
   {
     val name1 =
       if (name.startsWith("idea-icons/")) {
-        val file =
-          Isabelle_System.platform_file_url(Path.explode("$JEDIT_HOME/dist/jars/idea-icons.jar"))
+        val file = File.platform_file_url(Path.explode("$JEDIT_HOME/dist/jars/idea-icons.jar"))
         "jar:" + file + "!/" + name
       }
       else name

--- a/src/Tools/jEdit/src/jedit_resources.scala	Thu Aug 20 17:41:50 2015 +0100
+++ b/src/Tools/jEdit/src/jedit_resources.scala	Thu Aug 20 19:15:17 2015 +0200
@@ -56,14 +56,14 @@
   {
     val path = source_path.expand
     if (dir == "" || path.is_absolute)
-      MiscUtilities.resolveSymlinks(Isabelle_System.platform_path(path))
+      MiscUtilities.resolveSymlinks(File.platform_path(path))
     else if (path.is_current) dir
     else {
       val vfs = VFSManager.getVFSForPath(dir)
       if (vfs.isInstanceOf[FileVFS])
         MiscUtilities.resolveSymlinks(
-          vfs.constructPath(dir, Isabelle_System.platform_path(path)))
-      else vfs.constructPath(dir, Isabelle_System.standard_path(path))
+          vfs.constructPath(dir, File.platform_path(path)))
+      else vfs.constructPath(dir, File.standard_path(path))
     }
   }