clarified modules, like ML version;
authorwenzelm
Thu Aug 20 21:08:47 2015 +0200 (2015-08-20)
changeset 6099289effcb342df
parent 60991 2fc5a44346b5
child 60993 531a48ae1425
clarified modules, like ML version;
src/Pure/General/file.scala
src/Pure/PIDE/protocol.scala
src/Pure/System/isabelle_system.scala
src/Pure/Tools/build.scala
src/Pure/Tools/build_doc.scala
src/Pure/Tools/main.scala
src/Tools/jEdit/src/active.scala
src/Tools/jEdit/src/isabelle_logic.scala
src/Tools/jEdit/src/jedit_lib.scala
     1.1 --- a/src/Pure/General/file.scala	Thu Aug 20 20:36:06 2015 +0200
     1.2 +++ b/src/Pure/General/file.scala	Thu Aug 20 21:08:47 2015 +0200
     1.3 @@ -10,21 +10,85 @@
     1.4  import java.io.{BufferedWriter, OutputStreamWriter, FileOutputStream, BufferedOutputStream,
     1.5    OutputStream, InputStream, FileInputStream, BufferedInputStream, BufferedReader,
     1.6    InputStreamReader, File => JFile, IOException}
     1.7 +import java.net.{URL, URLDecoder, MalformedURLException}
     1.8  import java.util.zip.{GZIPInputStream, GZIPOutputStream}
     1.9 +import java.util.regex.Pattern
    1.10  
    1.11  import scala.collection.mutable
    1.12 +import scala.util.matching.Regex
    1.13  
    1.14  
    1.15  object File
    1.16  {
    1.17 -  /* system path representations */
    1.18 +  /* standard path (Cygwin or Posix) */
    1.19  
    1.20    def standard_path(path: Path): String = path.expand.implode
    1.21  
    1.22 -  def platform_path(path: Path): String = Isabelle_System.jvm_path(standard_path(path))
    1.23 +  def standard_path(platform_path: String): String =
    1.24 +    if (Platform.is_windows) {
    1.25 +      val Platform_Root = new Regex("(?i)" +
    1.26 +        Pattern.quote(Isabelle_System.get_cygwin_root()) + """(?:\\+|\z)(.*)""")
    1.27 +      val Drive = new Regex("""([a-zA-Z]):\\*(.*)""")
    1.28 +
    1.29 +      platform_path.replace('/', '\\') match {
    1.30 +        case Platform_Root(rest) => "/" + rest.replace('\\', '/')
    1.31 +        case Drive(letter, rest) =>
    1.32 +          "/cygdrive/" + Word.lowercase(letter) +
    1.33 +            (if (rest == "") "" else "/" + rest.replace('\\', '/'))
    1.34 +        case path => path.replace('\\', '/')
    1.35 +      }
    1.36 +    }
    1.37 +    else platform_path
    1.38 +
    1.39 +  def standard_path(file: JFile): String = standard_path(file.getPath)
    1.40 +
    1.41 +  def standard_url(name: String): String =
    1.42 +    try {
    1.43 +      val url = new URL(name)
    1.44 +      if (url.getProtocol == "file")
    1.45 +        standard_path(URLDecoder.decode(url.getPath, UTF8.charset_name))
    1.46 +      else name
    1.47 +    }
    1.48 +    catch { case _: MalformedURLException => standard_path(name) }
    1.49 +
    1.50 +
    1.51 +  /* platform path (Windows or Posix) */
    1.52 +
    1.53 +  private val Cygdrive = new Regex("/cygdrive/([a-zA-Z])($|/.*)")
    1.54 +  private val Named_Root = new Regex("//+([^/]*)(.*)")
    1.55 +
    1.56 +  def platform_path(standard_path: String): String =
    1.57 +    if (Platform.is_windows) {
    1.58 +      val result_path = new StringBuilder
    1.59 +      val rest =
    1.60 +        standard_path match {
    1.61 +          case Cygdrive(drive, rest) =>
    1.62 +            result_path ++= (Word.uppercase(drive) + ":" + JFile.separator)
    1.63 +            rest
    1.64 +          case Named_Root(root, rest) =>
    1.65 +            result_path ++= JFile.separator
    1.66 +            result_path ++= JFile.separator
    1.67 +            result_path ++= root
    1.68 +            rest
    1.69 +          case path if path.startsWith("/") =>
    1.70 +            result_path ++= Isabelle_System.get_cygwin_root()
    1.71 +            path
    1.72 +          case path => path
    1.73 +        }
    1.74 +      for (p <- space_explode('/', rest) if p != "") {
    1.75 +        val len = result_path.length
    1.76 +        if (len > 0 && result_path(len - 1) != JFile.separatorChar)
    1.77 +          result_path += JFile.separatorChar
    1.78 +        result_path ++= p
    1.79 +      }
    1.80 +      result_path.toString
    1.81 +    }
    1.82 +    else standard_path
    1.83 +
    1.84 +  def platform_path(path: Path): String = platform_path(standard_path(path))
    1.85    def platform_file(path: Path): JFile = new JFile(platform_path(path))
    1.86  
    1.87 -  def platform_file_url(raw_path: Path): String =
    1.88 +  def platform_url(raw_path: Path): String =
    1.89    {
    1.90      val path = raw_path.expand
    1.91      require(path.is_absolute)
    1.92 @@ -34,8 +98,11 @@
    1.93      else "file:///" + s.replace('\\', '/')
    1.94    }
    1.95  
    1.96 +
    1.97 +  /* shell path (bash) */
    1.98 +
    1.99    def shell_path(path: Path): String = "'" + standard_path(path) + "'"
   1.100 -  def shell_path(file: JFile): String = "'" + Isabelle_System.posix_path(file) + "'"
   1.101 +  def shell_path(file: JFile): String = "'" + standard_path(file) + "'"
   1.102  
   1.103  
   1.104    /* directory content */
   1.105 @@ -172,4 +239,3 @@
   1.106  
   1.107    def copy(path1: Path, path2: Path): Unit = copy(path1.file, path2.file)
   1.108  }
   1.109 -
     2.1 --- a/src/Pure/PIDE/protocol.scala	Thu Aug 20 20:36:06 2015 +0200
     2.2 +++ b/src/Pure/PIDE/protocol.scala	Thu Aug 20 21:08:47 2015 +0200
     2.3 @@ -368,7 +368,7 @@
     2.4          variant(List(
     2.5            { case Document.Node.Edits(a) => (Nil, list(pair(option(id), option(id)))(a)) },
     2.6            { case Document.Node.Deps(header) =>
     2.7 -              val master_dir = Isabelle_System.posix_path_url(name.master_dir)
     2.8 +              val master_dir = File.standard_url(name.master_dir)
     2.9                val theory = Long_Name.base_name(name.theory)
    2.10                val imports = header.imports.map({ case (a, _) => a.node })
    2.11                val keywords = header.keywords.map({ case (a, b, _) => (a, b) })
     3.1 --- a/src/Pure/System/isabelle_system.scala	Thu Aug 20 20:36:06 2015 +0200
     3.2 +++ b/src/Pure/System/isabelle_system.scala	Thu Aug 20 21:08:47 2015 +0200
     3.3 @@ -8,13 +8,9 @@
     3.4  package isabelle
     3.5  
     3.6  
     3.7 -import java.util.regex.Pattern
     3.8  import java.io.{File => JFile, IOException}
     3.9  import java.nio.file.{Path => JPath, Files, SimpleFileVisitor, FileVisitResult}
    3.10  import java.nio.file.attribute.BasicFileAttributes
    3.11 -import java.net.{URL, URLDecoder, MalformedURLException}
    3.12 -
    3.13 -import scala.util.matching.Regex
    3.14  
    3.15  
    3.16  object Isabelle_System
    3.17 @@ -91,7 +87,7 @@
    3.18  
    3.19          default(
    3.20            default(
    3.21 -            default(sys.env + ("ISABELLE_JDK_HOME" -> posix_path(jdk_home())),
    3.22 +            default(sys.env + ("ISABELLE_JDK_HOME" -> File.standard_path(jdk_home())),
    3.23                "TEMP_WINDOWS" -> temp_windows),
    3.24              "HOME" -> user_home),
    3.25            "ISABELLE_APP" -> "true")
    3.26 @@ -154,70 +150,6 @@
    3.27  
    3.28    /** file-system operations **/
    3.29  
    3.30 -  /* jvm_path */
    3.31 -
    3.32 -  private val Cygdrive = new Regex("/cygdrive/([a-zA-Z])($|/.*)")
    3.33 -  private val Named_Root = new Regex("//+([^/]*)(.*)")
    3.34 -
    3.35 -  def jvm_path(posix_path: String): String =
    3.36 -    if (Platform.is_windows) {
    3.37 -      val result_path = new StringBuilder
    3.38 -      val rest =
    3.39 -        posix_path match {
    3.40 -          case Cygdrive(drive, rest) =>
    3.41 -            result_path ++= (Word.uppercase(drive) + ":" + JFile.separator)
    3.42 -            rest
    3.43 -          case Named_Root(root, rest) =>
    3.44 -            result_path ++= JFile.separator
    3.45 -            result_path ++= JFile.separator
    3.46 -            result_path ++= root
    3.47 -            rest
    3.48 -          case path if path.startsWith("/") =>
    3.49 -            result_path ++= get_cygwin_root()
    3.50 -            path
    3.51 -          case path => path
    3.52 -        }
    3.53 -      for (p <- space_explode('/', rest) if p != "") {
    3.54 -        val len = result_path.length
    3.55 -        if (len > 0 && result_path(len - 1) != JFile.separatorChar)
    3.56 -          result_path += JFile.separatorChar
    3.57 -        result_path ++= p
    3.58 -      }
    3.59 -      result_path.toString
    3.60 -    }
    3.61 -    else posix_path
    3.62 -
    3.63 -
    3.64 -  /* posix_path */
    3.65 -
    3.66 -  def posix_path(jvm_path: String): String =
    3.67 -    if (Platform.is_windows) {
    3.68 -      val Platform_Root = new Regex("(?i)" +
    3.69 -        Pattern.quote(get_cygwin_root()) + """(?:\\+|\z)(.*)""")
    3.70 -      val Drive = new Regex("""([a-zA-Z]):\\*(.*)""")
    3.71 -
    3.72 -      jvm_path.replace('/', '\\') match {
    3.73 -        case Platform_Root(rest) => "/" + rest.replace('\\', '/')
    3.74 -        case Drive(letter, rest) =>
    3.75 -          "/cygdrive/" + Word.lowercase(letter) +
    3.76 -            (if (rest == "") "" else "/" + rest.replace('\\', '/'))
    3.77 -        case path => path.replace('\\', '/')
    3.78 -      }
    3.79 -    }
    3.80 -    else jvm_path
    3.81 -
    3.82 -  def posix_path(file: JFile): String = posix_path(file.getPath)
    3.83 -
    3.84 -  def posix_path_url(name: String): String =
    3.85 -    try {
    3.86 -      val url = new URL(name)
    3.87 -      if (url.getProtocol == "file")
    3.88 -        posix_path(URLDecoder.decode(url.getPath, UTF8.charset_name))
    3.89 -      else name
    3.90 -    }
    3.91 -    catch { case _: MalformedURLException => posix_path(name) }
    3.92 -
    3.93 -
    3.94    /* source files of Isabelle/ML bootstrap */
    3.95  
    3.96    def source_file(path: Path): Option[Path] =
    3.97 @@ -381,7 +313,7 @@
    3.98    {
    3.99      with_tmp_file("isabelle_script") { script_file =>
   3.100        File.write(script_file, script)
   3.101 -      val proc = Bash.process(cwd, env, false, "bash", posix_path(script_file))
   3.102 +      val proc = Bash.process(cwd, env, false, "bash", File.standard_path(script_file))
   3.103        proc.stdin.close
   3.104  
   3.105        val limited = new Limited_Progress(proc, progress_limit)
     4.1 --- a/src/Pure/Tools/build.scala	Thu Aug 20 20:36:06 2015 +0200
     4.2 +++ b/src/Pure/Tools/build.scala	Thu Aug 20 21:08:47 2015 +0200
     4.3 @@ -586,14 +586,14 @@
     4.4                  pair(list(pair(Path.encode, Path.encode)), pair(string, pair(string,
     4.5                  pair(string, pair(string, list(pair(Options.encode, list(Path.encode)))))))))))))(
     4.6                (command_timings, (do_output, (info.options, (verbose, (browser_info,
     4.7 -                (info.document_files, (Isabelle_System.posix_path(graph_file), (parent,
     4.8 +                (info.document_files, (File.standard_path(graph_file), (parent,
     4.9                  (info.chapter, (name, theories)))))))))))
    4.10          }))
    4.11  
    4.12      private val env =
    4.13        Map("INPUT" -> parent, "TARGET" -> name, "OUTPUT" -> File.standard_path(output),
    4.14          (if (is_pure(name)) "ISABELLE_PROCESS_OPTIONS" else "ARGS_FILE") ->
    4.15 -          Isabelle_System.posix_path(args_file))
    4.16 +          File.standard_path(args_file))
    4.17  
    4.18      private val script =
    4.19        if (is_pure(name)) {
     5.1 --- a/src/Pure/Tools/build_doc.scala	Thu Aug 20 20:36:06 2015 +0200
     5.2 +++ b/src/Pure/Tools/build_doc.scala	Thu Aug 20 21:08:47 2015 +0200
     5.3 @@ -50,7 +50,7 @@
     5.4              Build.build(
     5.5                options.bool.update("browser_info", false).
     5.6                  string.update("document", "pdf").
     5.7 -                string.update("document_output", Isabelle_System.posix_path(output)),
     5.8 +                string.update("document_output", File.standard_path(output)),
     5.9                progress, clean_build = true, max_jobs = max_jobs, system_mode = system_mode,
    5.10                sessions = sessions)
    5.11            if (rc2 == 0) {
     6.1 --- a/src/Pure/Tools/main.scala	Thu Aug 20 20:36:06 2015 +0200
     6.2 +++ b/src/Pure/Tools/main.scala	Thu Aug 20 21:08:47 2015 +0200
     6.3 @@ -228,8 +228,8 @@
     6.4        val upd =
     6.5          if (Platform.is_windows)
     6.6            List(
     6.7 -            "ISABELLE_HOME" -> Isabelle_System.jvm_path(isabelle_home),
     6.8 -            "ISABELLE_HOME_USER" -> Isabelle_System.jvm_path(isabelle_home_user),
     6.9 +            "ISABELLE_HOME" -> File.platform_path(isabelle_home),
    6.10 +            "ISABELLE_HOME_USER" -> File.platform_path(isabelle_home_user),
    6.11              "INI_DIR" -> "")
    6.12          else
    6.13            List(
     7.1 --- a/src/Tools/jEdit/src/active.scala	Thu Aug 20 20:36:06 2015 +0200
     7.2 +++ b/src/Tools/jEdit/src/active.scala	Thu Aug 20 21:08:47 2015 +0200
     7.3 @@ -34,7 +34,7 @@
     7.4                    val graph_file = Isabelle_System.tmp_file("graph")
     7.5                    File.write(graph_file, XML.content(body))
     7.6                    Isabelle_System.bash_env(null,
     7.7 -                    Map("GRAPH_FILE" -> Isabelle_System.posix_path(graph_file)),
     7.8 +                    Map("GRAPH_FILE" -> File.standard_path(graph_file)),
     7.9                      "\"$ISABELLE_TOOL\" browser -c \"$GRAPH_FILE\" &")
    7.10                  }
    7.11  
     8.1 --- a/src/Tools/jEdit/src/isabelle_logic.scala	Thu Aug 20 20:36:06 2015 +0200
     8.2 +++ b/src/Tools/jEdit/src/isabelle_logic.scala	Thu Aug 20 21:08:47 2015 +0200
     8.3 @@ -83,7 +83,7 @@
     8.4      val name = session_args().last
     8.5      val content = Build.session_content(PIDE.options.value, inlined_files, dirs, name)
     8.6      content.copy(known_theories =
     8.7 -      content.known_theories.mapValues(name => name.map(Isabelle_System.jvm_path(_))))
     8.8 +      content.known_theories.mapValues(name => name.map(File.platform_path(_))))
     8.9    }
    8.10  }
    8.11  
     9.1 --- a/src/Tools/jEdit/src/jedit_lib.scala	Thu Aug 20 20:36:06 2015 +0200
     9.2 +++ b/src/Tools/jEdit/src/jedit_lib.scala	Thu Aug 20 21:08:47 2015 +0200
     9.3 @@ -308,7 +308,7 @@
     9.4    {
     9.5      val name1 =
     9.6        if (name.startsWith("idea-icons/")) {
     9.7 -        val file = File.platform_file_url(Path.explode("$JEDIT_HOME/dist/jars/idea-icons.jar"))
     9.8 +        val file = File.platform_url(Path.explode("$JEDIT_HOME/dist/jars/idea-icons.jar"))
     9.9          "jar:" + file + "!/" + name
    9.10        }
    9.11        else name