rendering information and style sheets via settings;
generalized Isabelle_System.try_read;
prefer getenv_strict in most situations;
--- 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 =
"""