# HG changeset patch # User wenzelm # Date 1343391752 -7200 # Node ID 97592027a2a8e96cea8df229a7de647c8b484bec # Parent cc7990d6eb38e85f79ef0faf04fb252d655158ae tuned signature; diff -r cc7990d6eb38 -r 97592027a2a8 src/Pure/General/file.scala --- a/src/Pure/General/file.scala Fri Jul 27 14:15:04 2012 +0200 +++ b/src/Pure/General/file.scala Fri Jul 27 14:22:32 2012 +0200 @@ -35,6 +35,19 @@ def read(path: Path): String = read(path.file) + /* try_read */ + + def try_read(paths: Seq[Path]): String = + { + val buf = new StringBuilder + for (path <- paths if path.is_file) { + buf.append(read(path)) + buf.append('\n') + } + buf.toString + } + + /* write */ private def write_file(file: JFile, text: CharSequence, gzip: Boolean) diff -r cc7990d6eb38 -r 97592027a2a8 src/Pure/General/symbol.scala --- a/src/Pure/General/symbol.scala Fri Jul 27 14:15:04 2012 +0200 +++ b/src/Pure/General/symbol.scala Fri Jul 27 14:22:32 2012 +0200 @@ -210,8 +210,7 @@ /** symbol interpretation **/ private lazy val symbols = - new Interpretation( - Isabelle_System.try_read(Path.split(Isabelle_System.getenv_strict("ISABELLE_SYMBOLS")))) + new Interpretation(File.try_read(Path.split(Isabelle_System.getenv_strict("ISABELLE_SYMBOLS")))) private class Interpretation(symbols_spec: String) { diff -r cc7990d6eb38 -r 97592027a2a8 src/Pure/System/isabelle_system.scala --- a/src/Pure/System/isabelle_system.scala Fri Jul 27 14:15:04 2012 +0200 +++ b/src/Pure/System/isabelle_system.scala Fri Jul 27 14:22:32 2012 +0200 @@ -124,19 +124,6 @@ def posix_path(jvm_path: String): String = standard_system.posix_path(jvm_path) - /* try_read */ - - def try_read(paths: Seq[Path]): String = - { - val buf = new StringBuilder - for (path <- paths if path.is_file) { - buf.append(File.read(path)) - buf.append('\n') - } - buf.toString - } - - /* source files */ private def try_file(file: JFile) = if (file.isFile) Some(file) else None diff -r cc7990d6eb38 -r 97592027a2a8 src/Tools/jEdit/src/html_panel.scala --- a/src/Tools/jEdit/src/html_panel.scala Fri Jul 27 14:15:04 2012 +0200 +++ b/src/Tools/jEdit/src/html_panel.scala Fri Jul 27 14:22:32 2012 +0200 @@ -92,7 +92,7 @@