--- 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"))
--- 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 =
{
"""<?xml version="1.0" encoding="utf-8"?>
@@ -74,8 +68,8 @@
<head>
<style media="all" type="text/css">
""" +
- try_file("$ISABELLE_HOME/lib/html/isabelle.css") + "\n" +
- try_file("$ISABELLE_HOME_USER/etc/isabelle.css") + "\n" +
+ sys.try_read("$ISABELLE_HOME/lib/html/isabelle.css") + "\n" +
+ sys.try_read("$ISABELLE_HOME_USER/etc/isabelle.css") + "\n" +
"body { font-family: " + sys.font_family + "; font-size: " + raw_px(font_size) + "px }" +
"""
</style>