--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/General/file.scala Fri Jul 20 23:38:15 2012 +0200
@@ -0,0 +1,107 @@
+/* Title: Pure/General/file.scala
+ Author: Makarius
+
+File system operations.
+*/
+
+package isabelle
+
+
+import java.io.{BufferedWriter, OutputStreamWriter, FileOutputStream, BufferedOutputStream,
+ InputStream, FileInputStream, BufferedReader, InputStreamReader, File => JFile, FileFilter}
+import java.util.zip.GZIPOutputStream
+
+import scala.collection.mutable
+
+
+object File
+{
+ /* read */
+
+ def read(reader: BufferedReader): String =
+ {
+ val output = new StringBuilder(100)
+ var c = -1
+ while ({ c = reader.read; c != -1 }) output += c.toChar
+ reader.close
+ output.toString
+ }
+
+ def read(stream: InputStream): String =
+ read(new BufferedReader(new InputStreamReader(stream, Standard_System.charset)))
+
+ def read(file: JFile): String = read(new FileInputStream(file))
+
+ def read(path: Path): String = read(path.file)
+
+
+ /* write */
+
+ private def write_file(file: JFile, text: CharSequence, zip: Boolean)
+ {
+ val stream1 = new FileOutputStream(file)
+ val stream2 = if (zip) new GZIPOutputStream(new BufferedOutputStream(stream1)) else stream1
+ val writer = new BufferedWriter(new OutputStreamWriter(stream2, Standard_System.charset))
+ try { writer.append(text) }
+ finally { writer.close }
+ }
+
+ def write(file: JFile, text: CharSequence): Unit = write_file(file, text, false)
+ def write(path: Path, text: CharSequence): Unit = write(path.file, text)
+
+ def write_zip(file: JFile, text: CharSequence): Unit = write_file(file, text, true)
+ def write_zip(path: Path, text: CharSequence): Unit = write_zip(path.file, text)
+
+
+ /* copy */
+
+ def eq(file1: JFile, file2: JFile): Boolean =
+ file1.getCanonicalPath == file2.getCanonicalPath // FIXME prefer java.nio.file.Files.isSameFile of Java 1.7
+
+ def copy(src: JFile, dst: JFile)
+ {
+ if (!eq(src, dst)) {
+ val in = new FileInputStream(src)
+ try {
+ val out = new FileOutputStream(dst)
+ try {
+ val buf = new Array[Byte](65536)
+ var m = 0
+ do {
+ m = in.read(buf, 0, buf.length)
+ if (m != -1) out.write(buf, 0, m)
+ } while (m != -1)
+ }
+ finally { out.close }
+ }
+ finally { in.close }
+ }
+ }
+
+ def copy(path1: Path, path2: Path): Unit = copy(path1.file, path2.file)
+
+
+ /* misc */
+
+ def with_tmp_file[A](prefix: String)(body: JFile => A): A =
+ {
+ val file = JFile.createTempFile(prefix, null)
+ file.deleteOnExit
+ try { body(file) } finally { file.delete }
+ }
+
+ // FIXME handle (potentially cyclic) directory graph
+ def find_files(start: JFile, ok: JFile => Boolean): List[JFile] =
+ {
+ val files = new mutable.ListBuffer[JFile]
+ val filter = new FileFilter { def accept(entry: JFile) = entry.isDirectory || ok(entry) }
+ def find_entry(entry: JFile)
+ {
+ if (ok(entry)) files += entry
+ if (entry.isDirectory) entry.listFiles(filter).foreach(find_entry)
+ }
+ find_entry(start)
+ files.toList
+ }
+}
+
--- a/src/Pure/General/path.scala Fri Jul 20 22:43:51 2012 +0200
+++ b/src/Pure/General/path.scala Fri Jul 20 23:38:15 2012 +0200
@@ -8,7 +8,7 @@
package isabelle
-import java.io.File
+import java.io.{File => JFile}
import scala.util.matching.Regex
@@ -168,5 +168,5 @@
/* platform file */
- def file: File = Isabelle_System.platform_file(this)
+ def file: JFile = Isabelle_System.platform_file(this)
}
--- a/src/Pure/General/position.scala Fri Jul 20 22:43:51 2012 +0200
+++ b/src/Pure/General/position.scala Fri Jul 20 23:38:15 2012 +0200
@@ -7,6 +7,9 @@
package isabelle
+import java.io.{File => JFile}
+
+
object Position
{
type T = Properties.T
@@ -17,8 +20,8 @@
val File = new Properties.String(Isabelle_Markup.FILE)
val Id = new Properties.Long(Isabelle_Markup.ID)
- def file(f: java.io.File): T = File(Isabelle_System.posix_path(f.toString))
- def line_file(i: Int, f: java.io.File): T = Line(i) ::: file(f)
+ def file(f: JFile): T = File(Isabelle_System.posix_path(f.toString))
+ def line_file(i: Int, f: JFile): T = Line(i) ::: file(f)
object Range
{
--- a/src/Pure/General/scan.scala Fri Jul 20 22:43:51 2012 +0200
+++ b/src/Pure/General/scan.scala Fri Jul 20 23:38:15 2012 +0200
@@ -12,7 +12,7 @@
import scala.util.parsing.input.{OffsetPosition, Position => InputPosition, Reader}
import scala.util.parsing.combinator.RegexParsers
-import java.io.{File, BufferedInputStream, FileInputStream}
+import java.io.{File => JFile, BufferedInputStream, FileInputStream}
object Scan
@@ -422,7 +422,7 @@
abstract class Byte_Reader extends Reader[Char] { def close: Unit }
- def byte_reader(file: File): Byte_Reader =
+ def byte_reader(file: JFile): Byte_Reader =
{
val stream = new BufferedInputStream(new FileInputStream(file))
val seq = new PagedSeq(
--- a/src/Pure/General/sha1.scala Fri Jul 20 22:43:51 2012 +0200
+++ b/src/Pure/General/sha1.scala Fri Jul 20 23:38:15 2012 +0200
@@ -8,7 +8,7 @@
package isabelle
-import java.io.{File, FileInputStream}
+import java.io.{File => JFile, FileInputStream}
import java.security.MessageDigest
@@ -30,7 +30,7 @@
Digest(result.toString)
}
- def digest(file: File): Digest =
+ def digest(file: JFile): Digest =
{
val stream = new FileInputStream(file)
val digest = MessageDigest.getInstance("SHA")
--- a/src/Pure/System/build.scala Fri Jul 20 22:43:51 2012 +0200
+++ b/src/Pure/System/build.scala Fri Jul 20 23:38:15 2012 +0200
@@ -7,7 +7,7 @@
package isabelle
-import java.io.File
+import java.io.{File => JFile}
import scala.collection.mutable
import scala.annotation.tailrec
@@ -140,9 +140,9 @@
{ case a ~ b ~ c ~ d ~ e ~ f ~ g ~ h ~ i => Session_Entry(a, b, c, d, e, f, g, h, i) }
}
- def parse_entries(root: File): List[Session_Entry] =
+ def parse_entries(root: JFile): List[Session_Entry] =
{
- val toks = syntax.scan(Standard_System.read_file(root))
+ val toks = syntax.scan(File.read(root))
parse_all(rep(session_entry), Token.reader(toks, root.toString)) match {
case Success(result, _) => result
case bad => error(bad.toString)
@@ -158,7 +158,7 @@
private def is_pure(name: String): Boolean = name == "RAW" || name == "Pure"
- private def sessions_root(dir: Path, root: File, queue: Session.Queue): Session.Queue =
+ private def sessions_root(dir: Path, root: JFile, queue: Session.Queue): Session.Queue =
{
(queue /: Parser.parse_entries(root))((queue1, entry) =>
try {
@@ -204,11 +204,10 @@
else queue
}
- private def sessions_catalog(dir: Path, catalog: File, queue: Session.Queue): Session.Queue =
+ private def sessions_catalog(dir: Path, catalog: JFile, queue: Session.Queue): Session.Queue =
{
val dirs =
- split_lines(Standard_System.read_file(catalog)).
- filterNot(line => line == "" || line.startsWith("#"))
+ split_lines(File.read(catalog)).filterNot(line => line == "" || line.startsWith("#"))
(queue /: dirs)((queue1, dir1) =>
try {
val dir2 = dir + Path.explode(dir1)
@@ -275,15 +274,12 @@
!Path.explode("$ISABELLE_BROWSER_INFO/index.html").file.isFile)
{
Path.explode("$ISABELLE_BROWSER_INFO").file.mkdirs()
- Standard_System.copy_file(Path.explode("$ISABELLE_HOME/lib/logo/isabelle.gif").file,
- Path.explode("$ISABELLE_BROWSER_INFO/isabelle.gif").file)
- Standard_System.write_file(Path.explode("$ISABELLE_BROWSER_INFO/index.html").file,
- Standard_System.read_file(
- Path.explode("$ISABELLE_HOME/lib/html/library_index_header.template").file) +
- Standard_System.read_file(
- Path.explode("$ISABELLE_HOME/lib/html/library_index_content.template").file) +
- Standard_System.read_file(
- Path.explode("$ISABELLE_HOME/lib/html/library_index_footer.template").file))
+ File.copy(Path.explode("$ISABELLE_HOME/lib/logo/isabelle.gif"),
+ Path.explode("$ISABELLE_BROWSER_INFO/isabelle.gif"))
+ File.write(Path.explode("$ISABELLE_BROWSER_INFO/index.html"),
+ File.read(Path.explode("$ISABELLE_HOME/lib/html/library_index_header.template")) +
+ File.read(Path.explode("$ISABELLE_HOME/lib/html/library_index_content.template")) +
+ File.read(Path.explode("$ISABELLE_HOME/lib/html/library_index_footer.template")))
}
// prepare log dir
@@ -304,10 +300,10 @@
val log = log_dir + Path.basic(key.name)
if (rc == 0) {
- Standard_System.write_file(log.ext("gz").file, out, true)
+ File.write_zip(log.ext("gz"), out)
}
else {
- Standard_System.write_file(log.file, out)
+ File.write(log, out)
echo(key.name + " FAILED")
echo("(see also " + log.file + ")")
val lines = split_lines(out)
--- a/src/Pure/System/isabelle_system.scala Fri Jul 20 22:43:51 2012 +0200
+++ b/src/Pure/System/isabelle_system.scala Fri Jul 20 23:38:15 2012 +0200
@@ -10,7 +10,7 @@
import java.lang.System
import java.util.regex.Pattern
import java.util.Locale
-import java.io.{InputStream, OutputStream, File, BufferedReader, InputStreamReader,
+import java.io.{InputStream, OutputStream, File => JFile, BufferedReader, InputStreamReader,
BufferedWriter, OutputStreamWriter, IOException}
import java.awt.{GraphicsEnvironment, Font}
import java.awt.font.TextAttribute
@@ -68,7 +68,7 @@
case Some(path) => path
}
- Standard_System.with_tmp_file("settings") { dump =>
+ File.with_tmp_file("settings") { dump =>
val shell_prefix =
if (Platform.is_windows) List(standard_system.platform_root + "\\bin\\bash", "-l")
else Nil
@@ -78,7 +78,7 @@
if (rc != 0) error(output)
val entries =
- (for (entry <- Standard_System.read_file(dump) split "\0" if entry != "") yield {
+ (for (entry <- File.read(dump) split "\0" if entry != "") yield {
val i = entry.indexOf('=')
if (i <= 0) (entry -> "")
else (entry.substring(0, i) -> entry.substring(i + 1))
@@ -109,7 +109,7 @@
def standard_path(path: Path): String = path.expand.implode
def platform_path(path: Path): String = standard_system.jvm_path(standard_path(path))
- def platform_file(path: Path): File = new File(platform_path(path))
+ def platform_file(path: Path): JFile = new JFile(platform_path(path))
def platform_file_url(raw_path: Path): String =
{
@@ -132,16 +132,16 @@
for {
path <- paths
file = platform_file(path) if file.isFile
- } { buf.append(Standard_System.read_file(file)); buf.append('\n') }
+ } { buf.append(File.read(file)); buf.append('\n') }
buf.toString
}
/* source files */
- private def try_file(file: File) = if (file.isFile) Some(file) else None
+ private def try_file(file: JFile) = if (file.isFile) Some(file) else None
- def source_file(path: Path): Option[File] =
+ def source_file(path: Path): Option[JFile] =
{
if (path.is_absolute || path.is_current)
try_file(platform_file(path))
@@ -159,7 +159,7 @@
/* plain execute */
- def execute_env(cwd: File, env: Map[String, String], redirect: Boolean, args: String*): Process =
+ def execute_env(cwd: JFile, env: Map[String, String], redirect: Boolean, args: String*): Process =
{
val cmdline =
if (Platform.is_windows) List(standard_system.platform_root + "\\bin\\env.exe") ++ args
@@ -174,7 +174,7 @@
/* managed process */
- class Managed_Process(cwd: File, env: Map[String, String], redirect: Boolean, args: String*)
+ 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")
@@ -241,15 +241,15 @@
/* bash */
- def bash_env(cwd: File, env: Map[String, String], script: String): (String, String, Int) =
+ def bash_env(cwd: JFile, env: Map[String, String], script: String): (String, String, Int) =
{
- Standard_System.with_tmp_file("isabelle_script") { script_file =>
- Standard_System.write_file(script_file, script)
+ File.with_tmp_file("isabelle_script") { script_file =>
+ File.write(script_file, script)
val proc = new Managed_Process(cwd, env, false, "bash", posix_path(script_file.getPath))
proc.stdin.close
- val (_, stdout) = Simple_Thread.future("bash_stdout") { Standard_System.slurp(proc.stdout) }
- val (_, stderr) = Simple_Thread.future("bash_stderr") { Standard_System.slurp(proc.stderr) }
+ val (_, stdout) = Simple_Thread.future("bash_stdout") { File.read(proc.stdout) }
+ val (_, stderr) = Simple_Thread.future("bash_stderr") { File.read(proc.stderr) }
val rc =
try { proc.join }
@@ -260,7 +260,7 @@
def bash(script: String): (String, String, Int) = bash_env(null, null, script)
- class Bash_Job(cwd: File, env: Map[String, String], script: String)
+ class Bash_Job(cwd: JFile, env: Map[String, String], script: String)
{
private val (thread, result) = Simple_Thread.future("bash_job") { bash_env(cwd, env, script) }
--- a/src/Pure/System/options.scala Fri Jul 20 22:43:51 2012 +0200
+++ b/src/Pure/System/options.scala Fri Jul 20 23:38:15 2012 +0200
@@ -7,7 +7,7 @@
package isabelle
-import java.io.File
+import java.io.{File => JFile}
object Options
@@ -49,10 +49,9 @@
{ case _ ~ (a ~ _ ~ b) => (options: Options) => options.define(a, b) }
}
- def parse_entries(file: File): List[Options => Options] =
+ def parse_entries(file: JFile): List[Options => Options] =
{
- val toks = syntax.scan(Standard_System.read_file(file))
- parse_all(rep(entry), Token.reader(toks, file.toString)) match {
+ parse_all(rep(entry), Token.reader(syntax.scan(File.read(file)), file.toString)) match {
case Success(result, _) => result
case bad => error(bad.toString)
}
--- a/src/Pure/System/session_manager.scala Fri Jul 20 22:43:51 2012 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,48 +0,0 @@
-/* Title: Pure/System/isabelle_manager.scala
- Author: Makarius
-
-Isabelle session manager.
-*/
-
-package isabelle
-
-
-import java.io.{File, FileFilter}
-
-
-class Session_Manager
-{
- val ROOT_NAME = "session.root"
-
- def is_session_file(file: File): Boolean =
- file.isFile && file.getName == ROOT_NAME
-
- def is_session_dir(dir: File): Boolean =
- dir.isDirectory && (new File(dir, ROOT_NAME)).isFile
-
-
- // FIXME handle (potentially cyclic) directory graph
- private def find_sessions(reverse_prefix: List[String], reverse_sessions: List[List[String]],
- dir: File): List[List[String]] =
- {
- val (reverse_prefix1, reverse_sessions1) =
- if (is_session_dir(dir)) {
- val name = dir.getName // FIXME from root file
- val reverse_prefix1 = name :: reverse_prefix
- val reverse_sessions1 = reverse_prefix1.reverse :: reverse_sessions
- (reverse_prefix1, reverse_sessions1)
- }
- else (reverse_prefix, reverse_sessions)
-
- val subdirs =
- dir.listFiles(new FileFilter { def accept(entry: File) = entry.isDirectory })
- (reverse_sessions1 /: subdirs)(find_sessions(reverse_prefix1, _, _))
- }
-
- def component_sessions(): List[List[String]] =
- {
- val toplevel_sessions =
- Isabelle_System.components().map(Isabelle_System.platform_file).filter(is_session_dir)
- ((Nil: List[List[String]]) /: toplevel_sessions)(find_sessions(Nil, _, _)).reverse
- }
-}
--- a/src/Pure/System/standard_system.scala Fri Jul 20 22:43:51 2012 +0200
+++ b/src/Pure/System/standard_system.scala Fri Jul 20 23:38:15 2012 +0200
@@ -11,15 +11,11 @@
import java.util.regex.Pattern
import java.util.Locale
import java.net.URL
-import java.io.{BufferedWriter, OutputStreamWriter, FileOutputStream, BufferedOutputStream,
- BufferedInputStream, InputStream, FileInputStream, BufferedReader, InputStreamReader,
- File, FileFilter, IOException}
+import java.io.{File => JFile}
import java.nio.charset.Charset
-import java.util.zip.GZIPOutputStream
import scala.io.Codec
import scala.util.matching.Regex
-import scala.collection.mutable
object Standard_System
@@ -100,77 +96,9 @@
}
- /* basic file operations */
-
- def slurp(reader: BufferedReader): String =
- {
- val output = new StringBuilder(100)
- var c = -1
- while ({ c = reader.read; c != -1 }) output += c.toChar
- reader.close
- output.toString
- }
-
- def slurp(stream: InputStream): String =
- slurp(new BufferedReader(new InputStreamReader(stream, charset)))
-
- def read_file(file: File): String = slurp(new FileInputStream(file))
-
- def write_file(file: File, text: CharSequence, zip: Boolean = false)
- {
- val stream1 = new FileOutputStream(file)
- val stream2 = if (zip) new GZIPOutputStream(new BufferedOutputStream(stream1)) else stream1
- val writer = new BufferedWriter(new OutputStreamWriter(stream2, charset))
- try { writer.append(text) }
- finally { writer.close }
- }
-
- def eq_file(file1: File, file2: File): Boolean =
- file1.getCanonicalPath == file2.getCanonicalPath // FIXME prefer java.nio.file.Files.isSameFile of Java 1.7
-
- def copy_file(src: File, dst: File) =
- if (!eq_file(src, dst)) {
- val in = new FileInputStream(src)
- try {
- val out = new FileOutputStream(dst)
- try {
- val buf = new Array[Byte](65536)
- var m = 0
- do {
- m = in.read(buf, 0, buf.length)
- if (m != -1) out.write(buf, 0, m)
- } while (m != -1)
- }
- finally { out.close }
- }
- finally { in.close }
- }
-
- def with_tmp_file[A](prefix: String)(body: File => A): A =
- {
- val file = File.createTempFile(prefix, null)
- file.deleteOnExit
- try { body(file) } finally { file.delete }
- }
-
- // FIXME handle (potentially cyclic) directory graph
- def find_files(start: File, ok: File => Boolean): List[File] =
- {
- val files = new mutable.ListBuffer[File]
- val filter = new FileFilter { def accept(entry: File) = entry.isDirectory || ok(entry) }
- def find_entry(entry: File)
- {
- if (ok(entry)) files += entry
- if (entry.isDirectory) entry.listFiles(filter).foreach(find_entry)
- }
- find_entry(start)
- files.toList
- }
-
-
/* shell processes */
- def raw_execute(cwd: File, env: Map[String, String], redirect: Boolean, args: String*): Process =
+ def raw_execute(cwd: JFile, env: Map[String, String], redirect: Boolean, args: String*): Process =
{
val cmdline = new java.util.LinkedList[String]
for (s <- args) cmdline.add(s)
@@ -188,7 +116,7 @@
def process_output(proc: Process): (String, Int) =
{
proc.getOutputStream.close
- val output = slurp(proc.getInputStream)
+ val output = File.read(proc.getInputStream)
val rc =
try { proc.waitFor }
finally {
@@ -200,7 +128,7 @@
(output, rc)
}
- def raw_exec(cwd: File, env: Map[String, String], redirect: Boolean, args: String*)
+ def raw_exec(cwd: JFile, env: Map[String, String], redirect: Boolean, args: String*)
: (String, Int) = process_output(raw_execute(cwd, env, redirect, args: _*))
@@ -215,10 +143,10 @@
else if (cygwin_root2 != null && cygwin_root2 != "") cygwin_root2
else error("Bad Cygwin installation: unknown root")
- val root_file = new File(root)
- if (!new File(root_file, "bin\\bash.exe").isFile ||
- !new File(root_file, "bin\\env.exe").isFile ||
- !new File(root_file, "bin\\tar.exe").isFile)
+ val root_file = new JFile(root)
+ if (!new JFile(root_file, "bin\\bash.exe").isFile ||
+ !new JFile(root_file, "bin\\env.exe").isFile ||
+ !new JFile(root_file, "bin\\tar.exe").isFile)
error("Bad Cygwin installation: " + quote(root))
root
@@ -244,11 +172,11 @@
val rest =
posix_path match {
case Cygdrive(drive, rest) =>
- result_path ++= (drive.toUpperCase(Locale.ENGLISH) + ":" + File.separator)
+ result_path ++= (drive.toUpperCase(Locale.ENGLISH) + ":" + JFile.separator)
rest
case Named_Root(root, rest) =>
- result_path ++= File.separator
- result_path ++= File.separator
+ result_path ++= JFile.separator
+ result_path ++= JFile.separator
result_path ++= root
rest
case path if path.startsWith("/") =>
@@ -258,8 +186,8 @@
}
for (p <- space_explode('/', rest) if p != "") {
val len = result_path.length
- if (len > 0 && result_path(len - 1) != File.separatorChar)
- result_path += File.separatorChar
+ if (len > 0 && result_path(len - 1) != JFile.separatorChar)
+ result_path += JFile.separatorChar
result_path ++= p
}
result_path.toString
@@ -292,11 +220,11 @@
def this_jdk_home(): String =
{
val java_home = System.getProperty("java.home")
- val home = new File(java_home)
+ val home = new JFile(java_home)
val parent = home.getParent
val jdk_home =
if (home.getName == "jre" && parent != null &&
- (new File(new File(parent, "bin"), "javac")).exists) parent
+ (new JFile(new JFile(parent, "bin"), "javac")).exists) parent
else java_home
posix_path(jdk_home)
}
--- a/src/Pure/System/system_channel.scala Fri Jul 20 22:43:51 2012 +0200
+++ b/src/Pure/System/system_channel.scala Fri Jul 20 23:38:15 2012 +0200
@@ -8,7 +8,8 @@
package isabelle
-import java.io.{InputStream, OutputStream, File, FileInputStream, FileOutputStream, IOException}
+import java.io.{InputStream, OutputStream, File => JFile, FileInputStream,
+ FileOutputStream, IOException}
import java.net.{ServerSocket, InetAddress}
--- a/src/Pure/Thy/thy_header.scala Fri Jul 20 22:43:51 2012 +0200
+++ b/src/Pure/Thy/thy_header.scala Fri Jul 20 23:38:15 2012 +0200
@@ -12,7 +12,7 @@
import scala.util.parsing.input.{Reader, CharSequenceReader}
import scala.util.matching.Regex
-import java.io.File
+import java.io.{File => JFile}
object Thy_Header extends Parse.Parser
@@ -102,7 +102,7 @@
def read(source: CharSequence): Thy_Header =
read(new CharSequenceReader(source))
- def read(file: File): Thy_Header =
+ def read(file: JFile): Thy_Header =
{
val reader = Scan.byte_reader(file)
try { read(reader).map(Standard_System.decode_permissive_utf8) }
--- a/src/Pure/Thy/thy_load.scala Fri Jul 20 22:43:51 2012 +0200
+++ b/src/Pure/Thy/thy_load.scala Fri Jul 20 23:38:15 2012 +0200
@@ -7,7 +7,7 @@
package isabelle
-import java.io.File
+import java.io.{File => JFile}
@@ -31,7 +31,7 @@
def read_header(name: Document.Node.Name): Thy_Header =
{
- val file = new File(name.node)
+ val file = new JFile(name.node)
if (!file.exists || !file.isFile) error("No such file: " + quote(file.toString))
Thy_Header.read(file)
}
--- a/src/Pure/build-jars Fri Jul 20 22:43:51 2012 +0200
+++ b/src/Pure/build-jars Fri Jul 20 23:38:15 2012 +0200
@@ -14,6 +14,7 @@
Concurrent/simple_thread.scala
Concurrent/volatile.scala
General/exn.scala
+ General/file.scala
General/graph.scala
General/linear_set.scala
General/path.scala
@@ -51,7 +52,6 @@
System/options.scala
System/platform.scala
System/session.scala
- System/session_manager.scala
System/standard_system.scala
System/swing_thread.scala
System/system_channel.scala
--- a/src/Tools/jEdit/src/isabelle_hyperlinks.scala Fri Jul 20 22:43:51 2012 +0200
+++ b/src/Tools/jEdit/src/isabelle_hyperlinks.scala Fri Jul 20 23:38:15 2012 +0200
@@ -9,7 +9,7 @@
import isabelle._
-import java.io.File
+import java.io.{File => JFile}
import gatchan.jedit.hyperlinks.{Hyperlink, HyperlinkSource, AbstractHyperlink}
--- a/src/Tools/jEdit/src/jedit_thy_load.scala Fri Jul 20 22:43:51 2012 +0200
+++ b/src/Tools/jEdit/src/jedit_thy_load.scala Fri Jul 20 23:38:15 2012 +0200
@@ -9,7 +9,7 @@
import isabelle._
-import java.io.{File, IOException}
+import java.io.{File => JFile, IOException}
import javax.swing.text.Segment
import org.gjt.sp.jedit.io.{VFS, FileVFS, VFSFile, VFSManager}
@@ -65,7 +65,7 @@
case None => None
}
} getOrElse {
- val file = new File(name.node) // FIXME load URL via jEdit VFS (!?)
+ val file = new JFile(name.node) // FIXME load URL via jEdit VFS (!?)
if (!file.exists || !file.isFile) error("No such file: " + quote(file.toString))
Thy_Header.read(file)
}
--- a/src/Tools/jEdit/src/scala_console.scala Fri Jul 20 22:43:51 2012 +0200
+++ b/src/Tools/jEdit/src/scala_console.scala Fri Jul 20 23:38:15 2012 +0200
@@ -15,7 +15,7 @@
import org.gjt.sp.jedit.MiscUtilities
import java.lang.System
-import java.io.{File, OutputStream, Writer, PrintWriter}
+import java.io.{File => JFile, OutputStream, Writer, PrintWriter}
import scala.tools.nsc.{GenericRunnerSettings, NewLinePrintWriter, ConsoleWriter}
import scala.tools.nsc.interpreter.IMain
@@ -30,11 +30,11 @@
{
def find_jars(start: String): List[String] =
if (start != null)
- Standard_System.find_files(new File(start),
+ File.find_files(new JFile(start),
entry => entry.isFile && entry.getName.endsWith(".jar")).map(_.getAbsolutePath)
else Nil
val path = find_jars(jEdit.getSettingsDirectory) ::: find_jars(jEdit.getJEditHome)
- path.mkString(File.pathSeparator)
+ path.mkString(JFile.pathSeparator)
}