rendering information and style sheets via settings;
authorwenzelm
Sat, 22 May 2010 19:42:20 +0200
changeset 37058 c47653f3ec14
parent 37057 e70f9230c608
child 37059 d1840e304ed0
rendering information and style sheets via settings; generalized Isabelle_System.try_read; prefer getenv_strict in most situations;
etc/settings
src/Pure/System/isabelle_system.scala
src/Tools/jEdit/dist-template/etc/settings
src/Tools/jEdit/src/jedit/html_panel.scala
--- a/etc/settings	Fri May 21 23:48:48 2010 +0200
+++ b/etc/settings	Sat May 22 19:42:20 2010 +0200
@@ -192,6 +192,14 @@
 
 
 ###
+### Rendering information
+###
+
+ISABELLE_FONT_FAMILY="IsabelleText"
+ISABELLE_SYMBOLS="$ISABELLE_HOME/etc/symbols:$ISABELLE_HOME_USER/etc/symbols"
+
+
+###
 ### External reasoning tools
 ###
 
--- a/src/Pure/System/isabelle_system.scala	Fri May 21 23:48:48 2010 +0200
+++ b/src/Pure/System/isabelle_system.scala	Sat May 22 19:42:20 2010 +0200
@@ -93,7 +93,7 @@
     if (value != "") value else error("Undefined environment variable: " + name)
   }
 
-  override def toString = getenv("ISABELLE_HOME")
+  override def toString = getenv_strict("ISABELLE_HOME")
 
 
 
@@ -164,10 +164,15 @@
 
   /* try_read */
 
-  def try_read(path: String): String =
+  def try_read(paths: Seq[String]): String =
   {
-    val file = platform_file(path)
-    if (file.isFile) Source.fromFile(file).mkString else ""
+    val buf = new StringBuilder
+    for {
+      path <- paths
+      file = platform_file(path) if file.isFile
+      c <- (Source.fromFile(file) ++ Iterator.single('\n'))
+    } buf.append(c)
+    buf.toString
   }
 
 
@@ -303,7 +308,7 @@
   /* components */
 
   def components(): List[String] =
-    getenv("ISABELLE_COMPONENTS").split(":").toList
+    getenv_strict("ISABELLE_COMPONENTS").split(":").toList
 
 
   /* find logics */
@@ -324,17 +329,13 @@
 
   /* symbols */
 
-  private def read_symbols(path: String): List[String] =
-    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"))
+    try_read(getenv_strict("ISABELLE_SYMBOLS").split(":").toList).split("\n").toList)
 
 
   /* fonts */
 
-  val font_family = "IsabelleText"
+  val font_family = getenv_strict("ISABELLE_FONT_FAMILY")
 
   def get_font(size: Int = 1, bold: Boolean = false): Font =
     new Font(font_family, if (bold) Font.BOLD else Font.PLAIN, size)
@@ -357,6 +358,7 @@
       val ge = GraphicsEnvironment.getLocalGraphicsEnvironment()
       ge.registerFont(font)
       // workaround strange problem with Apple's Java 1.6 font manager
+      // FIXME does not quite work!?
       if (bold_font.getFamily == font_family) ge.registerFont(bold_font)
       if (!check_font()) error("Failed to install IsabelleText fonts")
     }
--- a/src/Tools/jEdit/dist-template/etc/settings	Fri May 21 23:48:48 2010 +0200
+++ b/src/Tools/jEdit/dist-template/etc/settings	Sat May 22 19:42:20 2010 +0200
@@ -6,6 +6,9 @@
 #JEDIT_JAVA_OPTIONS="-server -Xms128m -Xmx1024m -Xss4m $JEDIT_APPLE_PROPERTIES"
 JEDIT_OPTIONS="-reuseview -noserver -nobackground"
 
+JEDIT_STYLE_SHEETS="$ISABELLE_HOME/lib/html/isabelle.css:$JEDIT_HOME/etc/isabelle-jedit.css:$ISABELLE_HOME_USER/etc/isabelle.css:$ISABELLE_HOME_USER/etc/isabelle-jedit.css"
+
 ISABELLE_JEDIT_OPTIONS="-m xsymbols -m no_brackets -m no_type_brackets"
 
 ISABELLE_TOOLS="$ISABELLE_TOOLS:$JEDIT_HOME/lib/Tools"
+
--- a/src/Tools/jEdit/src/jedit/html_panel.scala	Fri May 21 23:48:48 2010 +0200
+++ b/src/Tools/jEdit/src/jedit/html_panel.scala	Sat May 22 19:42:20 2010 +0200
@@ -92,10 +92,7 @@
 <head>
 <style media="all" type="text/css">
 """ +
-  system.try_read("$ISABELLE_HOME/lib/html/isabelle.css") + "\n" +
-  system.try_read("$JEDIT_HOME/etc/isabelle-jedit.css") + "\n" +
-  system.try_read("$ISABELLE_HOME_USER/etc/isabelle.css") + "\n" +
-  system.try_read("$ISABELLE_HOME_USER/etc/isabelle-jedit.css") + "\n"
+  system.try_read(system.getenv_strict("JEDIT_STYLE_SHEETS").split(":"))
 
   private val template_tail =
 """