--- 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)
--- 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)
{
--- 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
--- 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 @@
<head>
<style media="all" type="text/css">
""" +
- Isabelle_System.try_read(Path.split(Isabelle_System.getenv_strict("JEDIT_STYLE_SHEETS")))
+ File.try_read(Path.split(Isabelle_System.getenv_strict("JEDIT_STYLE_SHEETS")))
private val template_tail =
"""
--- a/src/Tools/jEdit/src/readme_dockable.scala Fri Jul 27 14:15:04 2012 +0200
+++ b/src/Tools/jEdit/src/readme_dockable.scala Fri Jul 27 14:22:32 2012 +0200
@@ -17,8 +17,7 @@
private val readme = new HTML_Panel("SansSerif", 14)
private val readme_path = Path.explode("$JEDIT_HOME/README.html")
readme.render_document(
- Isabelle_System.platform_file_url(readme_path),
- Isabelle_System.try_read(List(readme_path)))
+ Isabelle_System.platform_file_url(readme_path), File.try_read(List(readme_path)))
set_content(readme)
}