tuned signature, according to ML version;
authorwenzelm
Thu Aug 20 19:15:17 2015 +0200 (2015-08-20 ago)
changeset 609881d7a7e33fd67
parent 60987 ea00d17eba3b
child 60989 c967d423953a
tuned signature, according to ML version;
src/Pure/General/file.scala
src/Pure/General/path.scala
src/Pure/System/isabelle_system.scala
src/Pure/Tools/build.scala
src/Pure/Tools/check_source.scala
src/Pure/Tools/main.scala
src/Tools/jEdit/src/documentation_dockable.scala
src/Tools/jEdit/src/jedit_editor.scala
src/Tools/jEdit/src/jedit_lib.scala
src/Tools/jEdit/src/jedit_resources.scala
     1.1 --- a/src/Pure/General/file.scala	Thu Aug 20 17:41:50 2015 +0100
     1.2 +++ b/src/Pure/General/file.scala	Thu Aug 20 19:15:17 2015 +0200
     1.3 @@ -17,6 +17,27 @@
     1.4  
     1.5  object File
     1.6  {
     1.7 +  /* system path representations */
     1.8 +
     1.9 +  def standard_path(path: Path): String = path.expand.implode
    1.10 +
    1.11 +  def platform_path(path: Path): String = Isabelle_System.jvm_path(standard_path(path))
    1.12 +  def platform_file(path: Path): JFile = new JFile(platform_path(path))
    1.13 +
    1.14 +  def platform_file_url(raw_path: Path): String =
    1.15 +  {
    1.16 +    val path = raw_path.expand
    1.17 +    require(path.is_absolute)
    1.18 +    val s = platform_path(path).replaceAll(" ", "%20")
    1.19 +    if (!Platform.is_windows) "file://" + s
    1.20 +    else if (s.startsWith("\\\\")) "file:" + s.replace('\\', '/')
    1.21 +    else "file:///" + s.replace('\\', '/')
    1.22 +  }
    1.23 +
    1.24 +  def shell_path(path: Path): String = "'" + standard_path(path) + "'"
    1.25 +  def shell_path(file: JFile): String = "'" + Isabelle_System.posix_path(file) + "'"
    1.26 +
    1.27 +
    1.28    /* directory content */
    1.29  
    1.30    def read_dir(dir: Path): List[String] =
     2.1 --- a/src/Pure/General/path.scala	Thu Aug 20 17:41:50 2015 +0100
     2.2 +++ b/src/Pure/General/path.scala	Thu Aug 20 19:15:17 2015 +0200
     2.3 @@ -205,7 +205,7 @@
     2.4  
     2.5    /* platform file */
     2.6  
     2.7 -  def file: JFile = Isabelle_System.platform_file(this)
     2.8 +  def file: JFile = File.platform_file(this)
     2.9    def is_file: Boolean = file.isFile
    2.10    def is_dir: Boolean = file.isDirectory
    2.11  }
     3.1 --- a/src/Pure/System/isabelle_system.scala	Thu Aug 20 17:41:50 2015 +0100
     3.2 +++ b/src/Pure/System/isabelle_system.scala	Thu Aug 20 19:15:17 2015 +0200
     3.3 @@ -219,27 +219,6 @@
     3.4      catch { case _: MalformedURLException => posix_path(name) }
     3.5  
     3.6  
     3.7 -  /* misc path specifications */
     3.8 -
     3.9 -  def standard_path(path: Path): String = path.expand.implode
    3.10 -
    3.11 -  def platform_path(path: Path): String = jvm_path(standard_path(path))
    3.12 -  def platform_file(path: Path): JFile = new JFile(platform_path(path))
    3.13 -
    3.14 -  def platform_file_url(raw_path: Path): String =
    3.15 -  {
    3.16 -    val path = raw_path.expand
    3.17 -    require(path.is_absolute)
    3.18 -    val s = platform_path(path).replaceAll(" ", "%20")
    3.19 -    if (!Platform.is_windows) "file://" + s
    3.20 -    else if (s.startsWith("\\\\")) "file:" + s.replace('\\', '/')
    3.21 -    else "file:///" + s.replace('\\', '/')
    3.22 -  }
    3.23 -
    3.24 -  def shell_path(path: Path): String = "'" + standard_path(path) + "'"
    3.25 -  def shell_path(file: JFile): String = "'" + posix_path(file) + "'"
    3.26 -
    3.27 -
    3.28    /* source files of Isabelle/ML bootstrap */
    3.29  
    3.30    def source_file(path: Path): Option[Path] =
    3.31 @@ -259,8 +238,8 @@
    3.32  
    3.33    def mkdirs(path: Path): Unit =
    3.34      if (!path.is_dir) {
    3.35 -      bash("perl -e \"use File::Path make_path; make_path(" + shell_path(path) + ");\"")
    3.36 -      if (!path.is_dir) error("Failed to create directory: " + quote(platform_path(path)))
    3.37 +      bash("perl -e \"use File::Path make_path; make_path(" + File.shell_path(path) + ");\"")
    3.38 +      if (!path.is_dir) error("Failed to create directory: " + quote(File.platform_path(path)))
    3.39      }
    3.40  
    3.41  
    3.42 @@ -320,7 +299,7 @@
    3.43    class Managed_Process(cwd: JFile, env: Map[String, String], redirect: Boolean, args: String*)
    3.44    {
    3.45      private val params =
    3.46 -      List(standard_path(Path.explode("~~/lib/scripts/process")), "group", "-", "no_script")
    3.47 +      List(File.standard_path(Path.explode("~~/lib/scripts/process")), "group", "-", "no_script")
    3.48      private val proc = execute_env(cwd, env, redirect, (params ::: args.toList):_*)
    3.49  
    3.50  
    3.51 @@ -390,7 +369,7 @@
    3.52    {
    3.53      val path = Path.explode("$ISABELLE_TMP_PREFIX")
    3.54      path.file.mkdirs  // low-level mkdirs
    3.55 -    platform_file(path)
    3.56 +    File.platform_file(path)
    3.57    }
    3.58  
    3.59    def tmp_file[A](name: String, ext: String = ""): JFile =
    3.60 @@ -523,7 +502,7 @@
    3.61        catch { case _: SecurityException => false }
    3.62      } match {
    3.63        case Some(dir) =>
    3.64 -        val file = standard_path(dir + Path.basic(name))
    3.65 +        val file = File.standard_path(dir + Path.basic(name))
    3.66          process_output(execute(true, (List(file) ::: args.toList): _*))
    3.67        case None => ("Unknown Isabelle tool: " + name, 2)
    3.68      }
    3.69 @@ -533,10 +512,10 @@
    3.70      bash("exec \"$ISABELLE_OPEN\" '" + arg + "' >/dev/null 2>/dev/null &")
    3.71  
    3.72    def pdf_viewer(arg: Path): Unit =
    3.73 -    bash("exec \"$PDF_VIEWER\" '" + standard_path(arg) + "' >/dev/null 2>/dev/null &")
    3.74 +    bash("exec \"$PDF_VIEWER\" '" + File.standard_path(arg) + "' >/dev/null 2>/dev/null &")
    3.75  
    3.76    def hg(cmd_line: String, cwd: Path = Path.current): Bash_Result =
    3.77 -    bash("cd " + shell_path(cwd) + " && \"${HG:-hg}\" " + cmd_line)
    3.78 +    bash("cd " + File.shell_path(cwd) + " && \"${HG:-hg}\" " + cmd_line)
    3.79  
    3.80  
    3.81    /** Isabelle resources **/
     4.1 --- a/src/Pure/Tools/build.scala	Thu Aug 20 17:41:50 2015 +0100
     4.2 +++ b/src/Pure/Tools/build.scala	Thu Aug 20 19:15:17 2015 +0200
     4.3 @@ -591,7 +591,7 @@
     4.4          }))
     4.5  
     4.6      private val env =
     4.7 -      Map("INPUT" -> parent, "TARGET" -> name, "OUTPUT" -> Isabelle_System.standard_path(output),
     4.8 +      Map("INPUT" -> parent, "TARGET" -> name, "OUTPUT" -> File.standard_path(output),
     4.9          (if (is_pure(name)) "ISABELLE_PROCESS_OPTIONS" else "ARGS_FILE") ->
    4.10            Isabelle_System.posix_path(args_file))
    4.11  
     5.1 --- a/src/Pure/Tools/check_source.scala	Thu Aug 20 17:41:50 2015 +0100
     5.2 +++ b/src/Pure/Tools/check_source.scala	Thu Aug 20 19:15:17 2015 +0200
     5.3 @@ -41,7 +41,7 @@
     5.4    def check_hg(root: Path)
     5.5    {
     5.6      Output.writeln("Checking " + root + " ...")
     5.7 -    Isabelle_System.hg("--repository " + Isabelle_System.shell_path(root) + " root").check_error
     5.8 +    Isabelle_System.hg("--repository " + File.shell_path(root) + " root").check_error
     5.9      for {
    5.10        file <- Isabelle_System.hg("manifest", root).check_error.out_lines
    5.11        if file.endsWith(".thy") || file.endsWith(".ML")
     6.1 --- a/src/Pure/Tools/main.scala	Thu Aug 20 17:41:50 2015 +0100
     6.2 +++ b/src/Pure/Tools/main.scala	Thu Aug 20 19:15:17 2015 +0200
     6.3 @@ -102,11 +102,11 @@
     6.4              Isabelle_System.getenv_strict("JEDIT_OPTIONS").split(" +")
     6.5  
     6.6            val jedit_settings =
     6.7 -            Array("-settings=" + Isabelle_System.platform_path(Path.explode("$JEDIT_SETTINGS")))
     6.8 +            Array("-settings=" + File.platform_path(Path.explode("$JEDIT_SETTINGS")))
     6.9  
    6.10            val more_args =
    6.11              if (args.isEmpty)
    6.12 -              Array(Isabelle_System.platform_path(Path.explode("$USER_HOME/Scratch.thy")))
    6.13 +              Array(File.platform_path(Path.explode("$USER_HOME/Scratch.thy")))
    6.14              else args
    6.15  
    6.16  
    6.17 @@ -114,11 +114,8 @@
    6.18  
    6.19            update_environment()
    6.20  
    6.21 -          System.setProperty("jedit.home",
    6.22 -            Isabelle_System.platform_path(Path.explode("$JEDIT_HOME/dist")))
    6.23 -
    6.24 -          System.setProperty("scala.home",
    6.25 -            Isabelle_System.platform_path(Path.explode("$SCALA_HOME")))
    6.26 +          System.setProperty("jedit.home", File.platform_path(Path.explode("$JEDIT_HOME/dist")))
    6.27 +          System.setProperty("scala.home", File.platform_path(Path.explode("$SCALA_HOME")))
    6.28  
    6.29            val jedit =
    6.30              Class.forName("org.gjt.sp.jedit.jEdit", true, ClassLoader.getSystemClassLoader)
     7.1 --- a/src/Tools/jEdit/src/documentation_dockable.scala	Thu Aug 20 17:41:50 2015 +0100
     7.2 +++ b/src/Tools/jEdit/src/documentation_dockable.scala	Thu Aug 20 19:15:17 2015 +0200
     7.3 @@ -54,10 +54,10 @@
     7.4    {
     7.5      node.getUserObject match {
     7.6        case Text_File(_, path) =>
     7.7 -        PIDE.editor.goto_file(true, view, Isabelle_System.platform_path(path))
     7.8 +        PIDE.editor.goto_file(true, view, File.platform_path(path))
     7.9        case Documentation(_, _, path) =>
    7.10          if (path.is_file)
    7.11 -          PIDE.editor.goto_file(true, view, Isabelle_System.platform_path(path))
    7.12 +          PIDE.editor.goto_file(true, view, File.platform_path(path))
    7.13          else {
    7.14            Future.fork {
    7.15              try { Doc.view(path) }
     8.1 --- a/src/Tools/jEdit/src/jedit_editor.scala	Thu Aug 20 17:41:50 2015 +0100
     8.2 +++ b/src/Tools/jEdit/src/jedit_editor.scala	Thu Aug 20 19:15:17 2015 +0200
     8.3 @@ -225,7 +225,7 @@
     8.4        if (Path.is_wellformed(source_name)) {
     8.5          if (Path.is_valid(source_name)) {
     8.6            val path = Path.explode(source_name)
     8.7 -          Some(Isabelle_System.platform_path(Isabelle_System.source_file(path) getOrElse path))
     8.8 +          Some(File.platform_path(Isabelle_System.source_file(path) getOrElse path))
     8.9          }
    8.10          else None
    8.11        }
     9.1 --- a/src/Tools/jEdit/src/jedit_lib.scala	Thu Aug 20 17:41:50 2015 +0100
     9.2 +++ b/src/Tools/jEdit/src/jedit_lib.scala	Thu Aug 20 19:15:17 2015 +0200
     9.3 @@ -308,8 +308,7 @@
     9.4    {
     9.5      val name1 =
     9.6        if (name.startsWith("idea-icons/")) {
     9.7 -        val file =
     9.8 -          Isabelle_System.platform_file_url(Path.explode("$JEDIT_HOME/dist/jars/idea-icons.jar"))
     9.9 +        val file = File.platform_file_url(Path.explode("$JEDIT_HOME/dist/jars/idea-icons.jar"))
    9.10          "jar:" + file + "!/" + name
    9.11        }
    9.12        else name
    10.1 --- a/src/Tools/jEdit/src/jedit_resources.scala	Thu Aug 20 17:41:50 2015 +0100
    10.2 +++ b/src/Tools/jEdit/src/jedit_resources.scala	Thu Aug 20 19:15:17 2015 +0200
    10.3 @@ -56,14 +56,14 @@
    10.4    {
    10.5      val path = source_path.expand
    10.6      if (dir == "" || path.is_absolute)
    10.7 -      MiscUtilities.resolveSymlinks(Isabelle_System.platform_path(path))
    10.8 +      MiscUtilities.resolveSymlinks(File.platform_path(path))
    10.9      else if (path.is_current) dir
   10.10      else {
   10.11        val vfs = VFSManager.getVFSForPath(dir)
   10.12        if (vfs.isInstanceOf[FileVFS])
   10.13          MiscUtilities.resolveSymlinks(
   10.14 -          vfs.constructPath(dir, Isabelle_System.platform_path(path)))
   10.15 -      else vfs.constructPath(dir, Isabelle_System.standard_path(path))
   10.16 +          vfs.constructPath(dir, File.platform_path(path)))
   10.17 +      else vfs.constructPath(dir, File.standard_path(path))
   10.18      }
   10.19    }
   10.20