# HG changeset patch # User wenzelm # Date 1274348190 -7200 # Node ID ccb8da7f76e6d3ce63130306fbb95cfa5a91e690 # Parent 449628c148cfc571eef0765ed9c6b49a1681c43f general Isabelle_System.try_read; diff -r 449628c148cf -r ccb8da7f76e6 src/Pure/System/isabelle_system.scala --- a/src/Pure/System/isabelle_system.scala Thu May 20 10:43:46 2010 +0200 +++ b/src/Pure/System/isabelle_system.scala Thu May 20 11:36:30 2010 +0200 @@ -150,6 +150,15 @@ def platform_file(path: String) = new File(platform_path(path)) + /* try_read */ + + def try_read(path: String): String = + { + val file = platform_file(path) + if (file.isFile) Source.fromFile(file).mkString else "" + } + + /* source files */ private def try_file(file: File) = if (file.isFile) Some(file) else None @@ -304,11 +313,8 @@ /* symbols */ private def read_symbols(path: String): List[String] = - { - val file = platform_file(path) - if (file.isFile) Source.fromFile(file).getLines("\n").toList - else Nil - } + Library.chunks(try_read(path)).map(_.toString).toList + val symbols = new Symbol.Interpretation( read_symbols("$ISABELLE_HOME/etc/symbols") ::: read_symbols("$ISABELLE_HOME_USER/etc/symbols")) diff -r 449628c148cf -r ccb8da7f76e6 src/Tools/jEdit/src/jedit/html_panel.scala --- a/src/Tools/jEdit/src/jedit/html_panel.scala Thu May 20 10:43:46 2010 +0200 +++ b/src/Tools/jEdit/src/jedit/html_panel.scala Thu May 20 11:36:30 2010 +0200 @@ -59,12 +59,6 @@ /* document template */ - private def try_file(name: String): String = - { - val file = sys.platform_file(name) - if (file.isFile) Source.fromFile(file).mkString else "" - } - private def template(font_size: Int): String = { """ @@ -74,8 +68,8 @@