--- a/src/Pure/General/file.scala Thu Aug 20 20:36:06 2015 +0200
+++ b/src/Pure/General/file.scala Thu Aug 20 21:08:47 2015 +0200
@@ -10,21 +10,85 @@
import java.io.{BufferedWriter, OutputStreamWriter, FileOutputStream, BufferedOutputStream,
OutputStream, InputStream, FileInputStream, BufferedInputStream, BufferedReader,
InputStreamReader, File => JFile, IOException}
+import java.net.{URL, URLDecoder, MalformedURLException}
import java.util.zip.{GZIPInputStream, GZIPOutputStream}
+import java.util.regex.Pattern
import scala.collection.mutable
+import scala.util.matching.Regex
object File
{
- /* system path representations */
+ /* standard path (Cygwin or Posix) */
def standard_path(path: Path): String = path.expand.implode
- def platform_path(path: Path): String = Isabelle_System.jvm_path(standard_path(path))
+ def standard_path(platform_path: String): String =
+ if (Platform.is_windows) {
+ val Platform_Root = new Regex("(?i)" +
+ Pattern.quote(Isabelle_System.get_cygwin_root()) + """(?:\\+|\z)(.*)""")
+ val Drive = new Regex("""([a-zA-Z]):\\*(.*)""")
+
+ platform_path.replace('/', '\\') match {
+ case Platform_Root(rest) => "/" + rest.replace('\\', '/')
+ case Drive(letter, rest) =>
+ "/cygdrive/" + Word.lowercase(letter) +
+ (if (rest == "") "" else "/" + rest.replace('\\', '/'))
+ case path => path.replace('\\', '/')
+ }
+ }
+ else platform_path
+
+ def standard_path(file: JFile): String = standard_path(file.getPath)
+
+ def standard_url(name: String): String =
+ try {
+ val url = new URL(name)
+ if (url.getProtocol == "file")
+ standard_path(URLDecoder.decode(url.getPath, UTF8.charset_name))
+ else name
+ }
+ catch { case _: MalformedURLException => standard_path(name) }
+
+
+ /* platform path (Windows or Posix) */
+
+ private val Cygdrive = new Regex("/cygdrive/([a-zA-Z])($|/.*)")
+ private val Named_Root = new Regex("//+([^/]*)(.*)")
+
+ def platform_path(standard_path: String): String =
+ if (Platform.is_windows) {
+ val result_path = new StringBuilder
+ val rest =
+ standard_path match {
+ case Cygdrive(drive, rest) =>
+ result_path ++= (Word.uppercase(drive) + ":" + JFile.separator)
+ rest
+ case Named_Root(root, rest) =>
+ result_path ++= JFile.separator
+ result_path ++= JFile.separator
+ result_path ++= root
+ rest
+ case path if path.startsWith("/") =>
+ result_path ++= Isabelle_System.get_cygwin_root()
+ path
+ case path => path
+ }
+ for (p <- space_explode('/', rest) if p != "") {
+ val len = result_path.length
+ if (len > 0 && result_path(len - 1) != JFile.separatorChar)
+ result_path += JFile.separatorChar
+ result_path ++= p
+ }
+ result_path.toString
+ }
+ else standard_path
+
+ def platform_path(path: Path): String = platform_path(standard_path(path))
def platform_file(path: Path): JFile = new JFile(platform_path(path))
- def platform_file_url(raw_path: Path): String =
+ def platform_url(raw_path: Path): String =
{
val path = raw_path.expand
require(path.is_absolute)
@@ -34,8 +98,11 @@
else "file:///" + s.replace('\\', '/')
}
+
+ /* shell path (bash) */
+
def shell_path(path: Path): String = "'" + standard_path(path) + "'"
- def shell_path(file: JFile): String = "'" + Isabelle_System.posix_path(file) + "'"
+ def shell_path(file: JFile): String = "'" + standard_path(file) + "'"
/* directory content */
@@ -172,4 +239,3 @@
def copy(path1: Path, path2: Path): Unit = copy(path1.file, path2.file)
}
-
--- a/src/Pure/PIDE/protocol.scala Thu Aug 20 20:36:06 2015 +0200
+++ b/src/Pure/PIDE/protocol.scala Thu Aug 20 21:08:47 2015 +0200
@@ -368,7 +368,7 @@
variant(List(
{ case Document.Node.Edits(a) => (Nil, list(pair(option(id), option(id)))(a)) },
{ case Document.Node.Deps(header) =>
- val master_dir = Isabelle_System.posix_path_url(name.master_dir)
+ val master_dir = File.standard_url(name.master_dir)
val theory = Long_Name.base_name(name.theory)
val imports = header.imports.map({ case (a, _) => a.node })
val keywords = header.keywords.map({ case (a, b, _) => (a, b) })
--- a/src/Pure/System/isabelle_system.scala Thu Aug 20 20:36:06 2015 +0200
+++ b/src/Pure/System/isabelle_system.scala Thu Aug 20 21:08:47 2015 +0200
@@ -8,13 +8,9 @@
package isabelle
-import java.util.regex.Pattern
import java.io.{File => JFile, IOException}
import java.nio.file.{Path => JPath, Files, SimpleFileVisitor, FileVisitResult}
import java.nio.file.attribute.BasicFileAttributes
-import java.net.{URL, URLDecoder, MalformedURLException}
-
-import scala.util.matching.Regex
object Isabelle_System
@@ -91,7 +87,7 @@
default(
default(
- default(sys.env + ("ISABELLE_JDK_HOME" -> posix_path(jdk_home())),
+ default(sys.env + ("ISABELLE_JDK_HOME" -> File.standard_path(jdk_home())),
"TEMP_WINDOWS" -> temp_windows),
"HOME" -> user_home),
"ISABELLE_APP" -> "true")
@@ -154,70 +150,6 @@
/** file-system operations **/
- /* jvm_path */
-
- private val Cygdrive = new Regex("/cygdrive/([a-zA-Z])($|/.*)")
- private val Named_Root = new Regex("//+([^/]*)(.*)")
-
- def jvm_path(posix_path: String): String =
- if (Platform.is_windows) {
- val result_path = new StringBuilder
- val rest =
- posix_path match {
- case Cygdrive(drive, rest) =>
- result_path ++= (Word.uppercase(drive) + ":" + JFile.separator)
- rest
- case Named_Root(root, rest) =>
- result_path ++= JFile.separator
- result_path ++= JFile.separator
- result_path ++= root
- rest
- case path if path.startsWith("/") =>
- result_path ++= get_cygwin_root()
- path
- case path => path
- }
- for (p <- space_explode('/', rest) if p != "") {
- val len = result_path.length
- if (len > 0 && result_path(len - 1) != JFile.separatorChar)
- result_path += JFile.separatorChar
- result_path ++= p
- }
- result_path.toString
- }
- else posix_path
-
-
- /* posix_path */
-
- def posix_path(jvm_path: String): String =
- if (Platform.is_windows) {
- val Platform_Root = new Regex("(?i)" +
- Pattern.quote(get_cygwin_root()) + """(?:\\+|\z)(.*)""")
- val Drive = new Regex("""([a-zA-Z]):\\*(.*)""")
-
- jvm_path.replace('/', '\\') match {
- case Platform_Root(rest) => "/" + rest.replace('\\', '/')
- case Drive(letter, rest) =>
- "/cygdrive/" + Word.lowercase(letter) +
- (if (rest == "") "" else "/" + rest.replace('\\', '/'))
- case path => path.replace('\\', '/')
- }
- }
- else jvm_path
-
- def posix_path(file: JFile): String = posix_path(file.getPath)
-
- def posix_path_url(name: String): String =
- try {
- val url = new URL(name)
- if (url.getProtocol == "file")
- posix_path(URLDecoder.decode(url.getPath, UTF8.charset_name))
- else name
- }
- catch { case _: MalformedURLException => posix_path(name) }
-
-
/* source files of Isabelle/ML bootstrap */
def source_file(path: Path): Option[Path] =
@@ -381,7 +313,7 @@
{
with_tmp_file("isabelle_script") { script_file =>
File.write(script_file, script)
- val proc = Bash.process(cwd, env, false, "bash", posix_path(script_file))
+ val proc = Bash.process(cwd, env, false, "bash", File.standard_path(script_file))
proc.stdin.close
val limited = new Limited_Progress(proc, progress_limit)
--- a/src/Pure/Tools/build.scala Thu Aug 20 20:36:06 2015 +0200
+++ b/src/Pure/Tools/build.scala Thu Aug 20 21:08:47 2015 +0200
@@ -586,14 +586,14 @@
pair(list(pair(Path.encode, Path.encode)), pair(string, pair(string,
pair(string, pair(string, list(pair(Options.encode, list(Path.encode)))))))))))))(
(command_timings, (do_output, (info.options, (verbose, (browser_info,
- (info.document_files, (Isabelle_System.posix_path(graph_file), (parent,
+ (info.document_files, (File.standard_path(graph_file), (parent,
(info.chapter, (name, theories)))))))))))
}))
private val env =
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))
+ File.standard_path(args_file))
private val script =
if (is_pure(name)) {
--- a/src/Pure/Tools/build_doc.scala Thu Aug 20 20:36:06 2015 +0200
+++ b/src/Pure/Tools/build_doc.scala Thu Aug 20 21:08:47 2015 +0200
@@ -50,7 +50,7 @@
Build.build(
options.bool.update("browser_info", false).
string.update("document", "pdf").
- string.update("document_output", Isabelle_System.posix_path(output)),
+ string.update("document_output", File.standard_path(output)),
progress, clean_build = true, max_jobs = max_jobs, system_mode = system_mode,
sessions = sessions)
if (rc2 == 0) {
--- a/src/Pure/Tools/main.scala Thu Aug 20 20:36:06 2015 +0200
+++ b/src/Pure/Tools/main.scala Thu Aug 20 21:08:47 2015 +0200
@@ -228,8 +228,8 @@
val upd =
if (Platform.is_windows)
List(
- "ISABELLE_HOME" -> Isabelle_System.jvm_path(isabelle_home),
- "ISABELLE_HOME_USER" -> Isabelle_System.jvm_path(isabelle_home_user),
+ "ISABELLE_HOME" -> File.platform_path(isabelle_home),
+ "ISABELLE_HOME_USER" -> File.platform_path(isabelle_home_user),
"INI_DIR" -> "")
else
List(
--- a/src/Tools/jEdit/src/active.scala Thu Aug 20 20:36:06 2015 +0200
+++ b/src/Tools/jEdit/src/active.scala Thu Aug 20 21:08:47 2015 +0200
@@ -34,7 +34,7 @@
val graph_file = Isabelle_System.tmp_file("graph")
File.write(graph_file, XML.content(body))
Isabelle_System.bash_env(null,
- Map("GRAPH_FILE" -> Isabelle_System.posix_path(graph_file)),
+ Map("GRAPH_FILE" -> File.standard_path(graph_file)),
"\"$ISABELLE_TOOL\" browser -c \"$GRAPH_FILE\" &")
}
--- a/src/Tools/jEdit/src/isabelle_logic.scala Thu Aug 20 20:36:06 2015 +0200
+++ b/src/Tools/jEdit/src/isabelle_logic.scala Thu Aug 20 21:08:47 2015 +0200
@@ -83,7 +83,7 @@
val name = session_args().last
val content = Build.session_content(PIDE.options.value, inlined_files, dirs, name)
content.copy(known_theories =
- content.known_theories.mapValues(name => name.map(Isabelle_System.jvm_path(_))))
+ content.known_theories.mapValues(name => name.map(File.platform_path(_))))
}
}
--- a/src/Tools/jEdit/src/jedit_lib.scala Thu Aug 20 20:36:06 2015 +0200
+++ b/src/Tools/jEdit/src/jedit_lib.scala Thu Aug 20 21:08:47 2015 +0200
@@ -308,7 +308,7 @@
{
val name1 =
if (name.startsWith("idea-icons/")) {
- val file = File.platform_file_url(Path.explode("$JEDIT_HOME/dist/jars/idea-icons.jar"))
+ val file = File.platform_url(Path.explode("$JEDIT_HOME/dist/jars/idea-icons.jar"))
"jar:" + file + "!/" + name
}
else name