1.1 --- a/src/Pure/System/isabelle_system.scala Thu May 20 10:43:46 2010 +0200
1.2 +++ b/src/Pure/System/isabelle_system.scala Thu May 20 11:36:30 2010 +0200
1.3 @@ -150,6 +150,15 @@
1.4 def platform_file(path: String) = new File(platform_path(path))
1.5
1.6
1.7 + /* try_read */
1.8 +
1.9 + def try_read(path: String): String =
1.10 + {
1.11 + val file = platform_file(path)
1.12 + if (file.isFile) Source.fromFile(file).mkString else ""
1.13 + }
1.14 +
1.15 +
1.16 /* source files */
1.17
1.18 private def try_file(file: File) = if (file.isFile) Some(file) else None
1.19 @@ -304,11 +313,8 @@
1.20 /* symbols */
1.21
1.22 private def read_symbols(path: String): List[String] =
1.23 - {
1.24 - val file = platform_file(path)
1.25 - if (file.isFile) Source.fromFile(file).getLines("\n").toList
1.26 - else Nil
1.27 - }
1.28 + Library.chunks(try_read(path)).map(_.toString).toList
1.29 +
1.30 val symbols = new Symbol.Interpretation(
1.31 read_symbols("$ISABELLE_HOME/etc/symbols") :::
1.32 read_symbols("$ISABELLE_HOME_USER/etc/symbols"))
2.1 --- a/src/Tools/jEdit/src/jedit/html_panel.scala Thu May 20 10:43:46 2010 +0200
2.2 +++ b/src/Tools/jEdit/src/jedit/html_panel.scala Thu May 20 11:36:30 2010 +0200
2.3 @@ -59,12 +59,6 @@
2.4
2.5 /* document template */
2.6
2.7 - private def try_file(name: String): String =
2.8 - {
2.9 - val file = sys.platform_file(name)
2.10 - if (file.isFile) Source.fromFile(file).mkString else ""
2.11 - }
2.12 -
2.13 private def template(font_size: Int): String =
2.14 {
2.15 """<?xml version="1.0" encoding="utf-8"?>
2.16 @@ -74,8 +68,8 @@
2.17 <head>
2.18 <style media="all" type="text/css">
2.19 """ +
2.20 - try_file("$ISABELLE_HOME/lib/html/isabelle.css") + "\n" +
2.21 - try_file("$ISABELLE_HOME_USER/etc/isabelle.css") + "\n" +
2.22 + sys.try_read("$ISABELLE_HOME/lib/html/isabelle.css") + "\n" +
2.23 + sys.try_read("$ISABELLE_HOME_USER/etc/isabelle.css") + "\n" +
2.24 "body { font-family: " + sys.font_family + "; font-size: " + raw_px(font_size) + "px }" +
2.25 """
2.26 </style>