# HG changeset patch
# User wenzelm
# Date 1309810292 -7200
# Node ID 39fdbd814c7ff2077b4c51998bdeca5ef0684bac
# Parent  bfc0bb115fa189334a3b483e5a57b80c614ea9ce
quasi-static Isabelle_System -- reduced tendency towards "functorial style";

diff -r bfc0bb115fa1 -r 39fdbd814c7f src/Pure/System/gui_setup.scala
--- a/src/Pure/System/gui_setup.scala	Mon Jul 04 20:18:19 2011 +0200
+++ b/src/Pure/System/gui_setup.scala	Mon Jul 04 22:11:32 2011 +0200
@@ -44,14 +44,15 @@
     text.append("JVM name: " + Platform.jvm_name + "\n")
     text.append("JVM platform: " + Platform.jvm_platform + "\n")
     try {
-      val isabelle_system = Isabelle_System.default
-      text.append("ML platform: " + isabelle_system.getenv("ML_PLATFORM") + "\n")
-      text.append("Isabelle platform: " + isabelle_system.getenv("ISABELLE_PLATFORM") + "\n")
-      val platform64 = isabelle_system.getenv("ISABELLE_PLATFORM64")
+      Isabelle_System.init()
+      text.append("ML platform: " + Isabelle_System.getenv("ML_PLATFORM") + "\n")
+      text.append("Isabelle platform: " + Isabelle_System.getenv("ISABELLE_PLATFORM") + "\n")
+      val platform64 = Isabelle_System.getenv("ISABELLE_PLATFORM64")
       if (platform64 != "") text.append("Isabelle platform (64 bit): " + platform64 + "\n")
-      text.append("Isabelle home: " + isabelle_system.getenv("ISABELLE_HOME") + "\n")
-      text.append("Isabelle java: " + isabelle_system.this_java() + "\n")
-    } catch { case ERROR(msg) => text.append(msg + "\n") }
+      text.append("Isabelle home: " + Isabelle_System.getenv("ISABELLE_HOME") + "\n")
+      text.append("Isabelle java: " + Isabelle_System.getenv("THIS_JAVA") + "\n")
+    }
+    catch { case ERROR(msg) => text.append(msg + "\n") }
 
     // reactions
     listenTo(ok)
diff -r bfc0bb115fa1 -r 39fdbd814c7f src/Pure/System/isabelle_process.scala
--- a/src/Pure/System/isabelle_process.scala	Mon Jul 04 20:18:19 2011 +0200
+++ b/src/Pure/System/isabelle_process.scala	Mon Jul 04 22:11:32 2011 +0200
@@ -62,7 +62,7 @@
 }
 
 
-class Isabelle_Process(system: Isabelle_System, timeout: Time, receiver: Actor, args: String*)
+class Isabelle_Process(timeout: Time, receiver: Actor, args: String*)
 {
   import Isabelle_Process._
 
@@ -70,8 +70,7 @@
   /* demo constructor */
 
   def this(args: String*) =
-    this(Isabelle_System.default, Time.seconds(10),
-      actor { loop { react { case res => Console.println(res) } } }, args: _*)
+    this(Time.seconds(10), actor { loop { react { case res => Console.println(res) } } }, args: _*)
 
 
   /* results */
@@ -93,7 +92,7 @@
 
   private def put_result(kind: String, text: String)
   {
-    put_result(kind, Nil, List(XML.Text(system.symbols.decode(text))))
+    put_result(kind, Nil, List(XML.Text(Isabelle_System.symbols.decode(text))))
   }
 
 
@@ -117,15 +116,16 @@
 
   /** process manager **/
 
-  private val in_fifo = system.mk_fifo()
-  private val out_fifo = system.mk_fifo()
-  private def rm_fifos() { system.rm_fifo(in_fifo); system.rm_fifo(out_fifo) }
+  private val in_fifo = Isabelle_System.mk_fifo()
+  private val out_fifo = Isabelle_System.mk_fifo()
+  private def rm_fifos() { Isabelle_System.rm_fifo(in_fifo); Isabelle_System.rm_fifo(out_fifo) }
 
   private val process =
     try {
       val cmdline =
-        List(system.getenv_strict("ISABELLE_PROCESS"), "-W", in_fifo + ":" + out_fifo) ++ args
-      new system.Managed_Process(true, cmdline: _*)
+        List(Isabelle_System.getenv_strict("ISABELLE_PROCESS"), "-W",
+          in_fifo + ":" + out_fifo) ++ args
+      new Isabelle_System.Managed_Process(true, cmdline: _*)
     }
     catch { case e: IOException => rm_fifos(); throw(e) }
 
@@ -168,8 +168,8 @@
     }
     else {
       // rendezvous
-      val command_stream = system.fifo_output_stream(in_fifo)
-      val message_stream = system.fifo_input_stream(out_fifo)
+      val command_stream = Isabelle_System.fifo_output_stream(in_fifo)
+      val message_stream = Isabelle_System.fifo_input_stream(out_fifo)
 
       standard_input = stdin_actor()
       val stdout = stdout_actor()
@@ -341,7 +341,7 @@
 
         if (i != n) throw new Protocol_Error("bad message chunk content")
 
-        YXML.parse_body_failsafe(YXML.decode_chars(system.symbols.decode, buf, 0, n))
+        YXML.parse_body_failsafe(YXML.decode_chars(Isabelle_System.symbols.decode, buf, 0, n))
         //}}}
       }
 
diff -r bfc0bb115fa1 -r 39fdbd814c7f src/Pure/System/isabelle_system.scala
--- a/src/Pure/System/isabelle_system.scala	Mon Jul 04 20:18:19 2011 +0200
+++ b/src/Pure/System/isabelle_system.scala	Mon Jul 04 22:11:32 2011 +0200
@@ -1,7 +1,8 @@
 /*  Title:      Pure/System/isabelle_system.scala
     Author:     Makarius
 
-Isabelle system support (settings environment etc.).
+Fundamental Isabelle system environment: settings, symbols etc.
+Quasi-static module with optional init operation.
 */
 
 package isabelle
@@ -21,15 +22,24 @@
 
 object Isabelle_System
 {
-  lazy val default: Isabelle_System = new Isabelle_System
-}
+  /** implicit state **/
 
-class Isabelle_System(this_isabelle_home: String) extends Standard_System
-{
-  def this() = this(null)
+  private case class State(
+    standard_system: Standard_System,
+    settings: Map[String, String],
+    symbols: Symbol.Interpretation)
 
+  @volatile private var _state: Option[State] = None
 
-  /** Isabelle environment **/
+  private def check_state(): State =
+  {
+    if (_state.isEmpty) init()  // unsynchronized check
+    _state.get
+  }
+
+  def standard_system: Standard_System = check_state().standard_system
+  def settings: Map[String, String] = check_state().settings
+  def symbols: Symbol.Interpretation = check_state().symbols
 
   /*
     isabelle_home precedence:
@@ -37,50 +47,67 @@
       (2) ISABELLE_HOME process environment variable (e.g. inherited from running isabelle tool)
       (3) isabelle.home system property (e.g. via JVM application boot process)
   */
+  def init(this_isabelle_home: String = null) = synchronized {
+    if (_state.isEmpty) {
+      import scala.collection.JavaConversions._
 
-  private val environment: Map[String, String] =
-  {
-    import scala.collection.JavaConversions._
+      val standard_system = new Standard_System
 
-    val env0 = Map(System.getenv.toList: _*) +
-      ("THIS_JAVA" -> this_java())
+      val settings =
+      {
+        val env = Map(System.getenv.toList: _*) +
+          ("THIS_JAVA" -> standard_system.this_java())
 
-    val isabelle_home =
-      if (this_isabelle_home != null) this_isabelle_home
-      else
-        env0.get("ISABELLE_HOME") match {
-          case None | Some("") =>
-            val path = System.getProperty("isabelle.home")
-            if (path == null || path == "") error("Unknown Isabelle home directory")
-            else path
-          case Some(path) => path
-        }
+        val isabelle_home =
+          if (this_isabelle_home != null) this_isabelle_home
+          else
+            env.get("ISABELLE_HOME") match {
+              case None | Some("") =>
+                val path = System.getProperty("isabelle.home")
+                if (path == null || path == "") error("Unknown Isabelle home directory")
+                else path
+              case Some(path) => path
+            }
 
-    Standard_System.with_tmp_file("settings") { dump =>
-        val shell_prefix =
-          if (Platform.is_windows) List(platform_root + "\\bin\\bash", "-l") else Nil
-        val cmdline =
-          shell_prefix ::: List(isabelle_home + "/bin/isabelle", "getenv", "-d", dump.toString)
-        val (output, rc) = Standard_System.raw_exec(null, env0, true, cmdline: _*)
-        if (rc != 0) error(output)
+          Standard_System.with_tmp_file("settings") { dump =>
+              val shell_prefix =
+                if (Platform.is_windows) List(standard_system.platform_root + "\\bin\\bash", "-l")
+                else Nil
+              val cmdline =
+                shell_prefix ::: List(isabelle_home + "/bin/isabelle", "getenv", "-d", dump.toString)
+              val (output, rc) = Standard_System.raw_exec(null, env, true, cmdline: _*)
+              if (rc != 0) error(output)
 
-        val entries =
-          for (entry <- Source.fromFile(dump).mkString split "\0" if entry != "") yield {
-            val i = entry.indexOf('=')
-            if (i <= 0) (entry -> "")
-            else (entry.substring(0, i) -> entry.substring(i + 1))
+              val entries =
+                for (entry <- Source.fromFile(dump).mkString split "\0" if entry != "") yield {
+                  val i = entry.indexOf('=')
+                  if (i <= 0) (entry -> "")
+                  else (entry.substring(0, i) -> entry.substring(i + 1))
+                }
+              Map(entries: _*) +
+                ("HOME" -> System.getenv("HOME")) +
+                ("PATH" -> System.getenv("PATH"))
+            }
           }
-        Map(entries: _*) +
-          ("HOME" -> System.getenv("HOME")) +
-          ("PATH" -> System.getenv("PATH"))
+
+      val symbols =
+      {
+        val isabelle_symbols = settings.getOrElse("ISABELLE_SYMBOLS", "")
+        if (isabelle_symbols == "") error("Undefined environment variable: ISABELLE_SYMBOLS")
+        val files =
+          isabelle_symbols.split(":").toList.map(s => new File(standard_system.jvm_path(s)))
+        new Symbol.Interpretation(Standard_System.try_read(files).split("\n").toList)
       }
+
+      _state = Some(State(standard_system, settings, symbols))
+    }
   }
 
 
   /* getenv */
 
   def getenv(name: String): String =
-    environment.getOrElse(if (name == "HOME") "HOME_JVM" else name, "")
+    settings.getOrElse(if (name == "HOME") "HOME_JVM" else name, "")
 
   def getenv_strict(name: String): String =
   {
@@ -88,9 +115,6 @@
     if (value != "") value else error("Undefined environment variable: " + name)
   }
 
-  override def toString = getenv_strict("ISABELLE_HOME")
-
-
 
   /** file-system operations **/
 
@@ -98,9 +122,11 @@
 
   def standard_path(path: Path): String = path.expand(getenv_strict).implode
 
-  def platform_path(path: Path): String = jvm_path(standard_path(path))
+  def platform_path(path: Path): String = standard_system.jvm_path(standard_path(path))
   def platform_file(path: Path) = new File(platform_path(path))
 
+  def posix_path(jvm_path: String): String = standard_system.posix_path(jvm_path)
+
 
   /* try_read */
 
@@ -142,9 +168,9 @@
   def execute(redirect: Boolean, args: String*): Process =
   {
     val cmdline =
-      if (Platform.is_windows) List(platform_root + "\\bin\\env.exe") ++ args
+      if (Platform.is_windows) List(standard_system.platform_root + "\\bin\\env.exe") ++ args
       else args
-    Standard_System.raw_execute(null, environment, redirect, cmdline: _*)
+    Standard_System.raw_execute(null, settings, redirect, cmdline: _*)
   }
 
 
@@ -271,7 +297,7 @@
   }
 
   def rm_fifo(fifo: String): Boolean =
-    (new File(jvm_path(if (Platform.is_windows) fifo + ".lnk" else fifo))).delete
+    (new File(standard_system.jvm_path(if (Platform.is_windows) fifo + ".lnk" else fifo))).delete
 
   def fifo_input_stream(fifo: String): InputStream =
   {
@@ -328,13 +354,6 @@
   }
 
 
-  /* symbols */
-
-  val symbols = new Symbol.Interpretation(
-    try_read(getenv_strict("ISABELLE_SYMBOLS").split(":").toList.map(Path.explode))
-      .split("\n").toList)
-
-
   /* fonts */
 
   def get_font(family: String = "IsabelleText", size: Int = 1, bold: Boolean = false): Font =
diff -r bfc0bb115fa1 -r 39fdbd814c7f src/Pure/System/session.scala
--- a/src/Pure/System/session.scala	Mon Jul 04 20:18:19 2011 +0200
+++ b/src/Pure/System/session.scala	Mon Jul 04 22:11:32 2011 +0200
@@ -40,7 +40,7 @@
 }
 
 
-class Session(val system: Isabelle_System, val file_store: Session.File_Store)
+class Session(val file_store: Session.File_Store)
 {
   /* real time parameters */  // FIXME properties or settings (!?)
 
@@ -117,7 +117,7 @@
 
   val new_id = new Counter
 
-  @volatile private var syntax = new Outer_Syntax(system.symbols)
+  @volatile private var syntax = new Outer_Syntax(Isabelle_System.symbols)
   def current_syntax(): Outer_Syntax = syntax
 
   @volatile private var reverse_syslog = List[XML.Elem]()
@@ -138,16 +138,14 @@
 
   /* theory files */
 
-  val thy_header = new Thy_Header(system.symbols)
-
   val thy_load = new Thy_Load
   {
     override def check_thy(dir: Path, name: String): (String, Thy_Header.Header) =
     {
-      val file = system.platform_file(dir + Thy_Header.thy_path(name))
+      val file = Isabelle_System.platform_file(dir + Thy_Header.thy_path(name))
       if (!file.exists || !file.isFile) error("No such file: " + quote(file.toString))
       val text = Standard_System.read_file(file)
-      val header = thy_header.read(text)
+      val header = Thy_Header.read(text)
       (text, header)
     }
   }
@@ -202,7 +200,8 @@
                         if (global_state.peek().lookup_command(command.id).isEmpty) {
                           global_state.change(_.define_command(command))
                           prover.get.
-                            define_command(command.id, system.symbols.encode(command.source))
+                            define_command(command.id,
+                              Isabelle_System.symbols.encode(command.source))
                         }
                         Some(command.id)
                     }
@@ -311,8 +310,7 @@
         case Start(timeout, args) if prover.isEmpty =>
           if (phase == Session.Inactive || phase == Session.Failed) {
             phase = Session.Startup
-            prover =
-              Some(new Isabelle_Process(system, timeout, this_actor, args:_*) with Isar_Document)
+            prover = Some(new Isabelle_Process(timeout, this_actor, args:_*) with Isar_Document)
           }
 
         case Stop =>
diff -r bfc0bb115fa1 -r 39fdbd814c7f src/Pure/System/session_manager.scala
--- a/src/Pure/System/session_manager.scala	Mon Jul 04 20:18:19 2011 +0200
+++ b/src/Pure/System/session_manager.scala	Mon Jul 04 22:11:32 2011 +0200
@@ -10,7 +10,7 @@
 import java.io.{File, FileFilter}
 
 
-class Session_Manager(system: Isabelle_System)
+class Session_Manager
 {
   val ROOT_NAME = "session.root"
 
@@ -42,7 +42,8 @@
   def component_sessions(): List[List[String]] =
   {
     val toplevel_sessions =
-      system.components().map(s => system.platform_file(Path.explode(s))).filter(is_session_dir)
+      Isabelle_System.components().map(s =>
+        Isabelle_System.platform_file(Path.explode(s))).filter(is_session_dir)
     ((Nil: List[List[String]]) /: toplevel_sessions)(find_sessions(Nil, _, _)).reverse
   }
 }
diff -r bfc0bb115fa1 -r 39fdbd814c7f src/Pure/System/standard_system.scala
--- a/src/Pure/System/standard_system.scala	Mon Jul 04 20:18:19 2011 +0200
+++ b/src/Pure/System/standard_system.scala	Mon Jul 04 22:11:32 2011 +0200
@@ -96,6 +96,16 @@
 
   def read_file(file: File): String = slurp(new FileInputStream(file))
 
+  def try_read(files: Seq[File]): String =
+  {
+    val buf = new StringBuilder
+    for {
+      file <- files if file.isFile
+      c <- (Source.fromFile(file) ++ Iterator.single('\n'))
+    } buf.append(c)
+    buf.toString
+  }
+
   def write_file(file: File, text: CharSequence)
   {
     val writer =
diff -r bfc0bb115fa1 -r 39fdbd814c7f src/Pure/Thy/html.scala
--- a/src/Pure/Thy/html.scala	Mon Jul 04 20:18:19 2011 +0200
+++ b/src/Pure/Thy/html.scala	Mon Jul 04 22:11:32 2011 +0200
@@ -55,9 +55,10 @@
   def sup(txt: String): XML.Elem = XML.elem("sup", List(XML.Text(txt)))
   def bold(txt: String): XML.Elem = span("bold", List(XML.Text(txt)))
 
-  def spans(symbols: Symbol.Interpretation,
-    input: XML.Tree, original_data: Boolean = false): XML.Body =
+  def spans(input: XML.Tree, original_data: Boolean = false): XML.Body =
   {
+    val symbols = Isabelle_System.symbols
+
     def html_spans(tree: XML.Tree): XML.Body =
       tree match {
         case XML.Elem(m @ Markup(name, props), ts) =>
diff -r bfc0bb115fa1 -r 39fdbd814c7f src/Pure/Thy/thy_header.scala
--- a/src/Pure/Thy/thy_header.scala	Mon Jul 04 20:18:19 2011 +0200
+++ b/src/Pure/Thy/thy_header.scala	Mon Jul 04 22:11:32 2011 +0200
@@ -15,7 +15,7 @@
 import java.io.File
 
 
-object Thy_Header
+object Thy_Header extends Parse.Parser
 {
   val HEADER = "header"
   val THEORY = "theory"
@@ -47,12 +47,6 @@
       case Thy_Path2(dir, name) => Some((dir, name))
       case _ => None
     }
-}
-
-
-class Thy_Header(symbols: Symbol.Interpretation) extends Parse.Parser
-{
-  import Thy_Header._
 
 
   /* header */
@@ -81,7 +75,7 @@
 
   def read(reader: Reader[Char]): Header =
   {
-    val token = lexicon.token(symbols, _ => false)
+    val token = lexicon.token(Isabelle_System.symbols, _ => false)
     val toks = new mutable.ListBuffer[Token]
 
     @tailrec def scan_to_begin(in: Reader[Char])
@@ -119,6 +113,6 @@
     val header = read(source)
     val name1 = header.name
     if (name == name1) header
-    else error("Bad file name " + Thy_Header.thy_path(name) + " for theory " + quote(name1))
+    else error("Bad file name " + thy_path(name) + " for theory " + quote(name1))
   }
 }
diff -r bfc0bb115fa1 -r 39fdbd814c7f src/Tools/jEdit/src/document_model.scala
--- a/src/Tools/jEdit/src/document_model.scala	Mon Jul 04 20:18:19 2011 +0200
+++ b/src/Tools/jEdit/src/document_model.scala	Mon Jul 04 22:11:32 2011 +0200
@@ -63,7 +63,7 @@
 
   private def capture_header(): Exn.Result[Thy_Header.Header] =
     Exn.capture {
-      session.thy_header.check(thy_name, buffer.getSegment(0, buffer.getLength))
+      Thy_Header.check(thy_name, buffer.getSegment(0, buffer.getLength))
     }
 
   private object pending_edits  // owned by Swing thread
diff -r bfc0bb115fa1 -r 39fdbd814c7f src/Tools/jEdit/src/document_view.scala
--- a/src/Tools/jEdit/src/document_view.scala	Mon Jul 04 20:18:19 2011 +0200
+++ b/src/Tools/jEdit/src/document_view.scala	Mon Jul 04 22:11:32 2011 +0200
@@ -143,7 +143,7 @@
   private def exit_popup() { html_popup.map(_.hide) }
 
   private val html_panel =
-    new HTML_Panel(Isabelle.system, Isabelle.font_family(), scala.math.round(Isabelle.font_size()))
+    new HTML_Panel(Isabelle.font_family(), scala.math.round(Isabelle.font_size()))
   html_panel.setBorder(BorderFactory.createLineBorder(Color.black))
 
   private def html_panel_resize()
diff -r bfc0bb115fa1 -r 39fdbd814c7f src/Tools/jEdit/src/html_panel.scala
--- a/src/Tools/jEdit/src/html_panel.scala	Mon Jul 04 20:18:19 2011 +0200
+++ b/src/Tools/jEdit/src/html_panel.scala	Mon Jul 04 22:11:32 2011 +0200
@@ -37,11 +37,7 @@
 }
 
 
-class HTML_Panel(
-    system: Isabelle_System,
-    initial_font_family: String,
-    initial_font_size: Int)
-  extends HtmlPanel
+class HTML_Panel(initial_font_family: String, initial_font_size: Int) extends HtmlPanel
 {
   /** Lobo setup **/
 
@@ -96,7 +92,8 @@
 <head>
 <style media="all" type="text/css">
 """ +
-  system.try_read(system.getenv_strict("JEDIT_STYLE_SHEETS").split(":").map(Path.explode))
+  Isabelle_System.try_read(
+    Isabelle_System.getenv_strict("JEDIT_STYLE_SHEETS").split(":").map(Path.explode))
 
   private val template_tail =
 """
@@ -168,8 +165,7 @@
         current_body.flatMap(div =>
           Pretty.formatted(List(div), current_margin, Pretty.font_metric(current_font_metrics))
             .map(t =>
-              XML.Elem(Markup(HTML.PRE, List((HTML.CLASS, Markup.MESSAGE))),
-                HTML.spans(system.symbols, t, true))))
+              XML.Elem(Markup(HTML.PRE, List((HTML.CLASS, Markup.MESSAGE))), HTML.spans(t, true))))
       val doc =
         builder.parse(
           new InputSourceImpl(
diff -r bfc0bb115fa1 -r 39fdbd814c7f src/Tools/jEdit/src/isabelle_encoding.scala
--- a/src/Tools/jEdit/src/isabelle_encoding.scala	Mon Jul 04 20:18:19 2011 +0200
+++ b/src/Tools/jEdit/src/isabelle_encoding.scala	Mon Jul 04 22:11:32 2011 +0200
@@ -34,7 +34,7 @@
   private def text_reader(in: InputStream, codec: Codec): Reader =
   {
     val source = new BufferedSource(in)(codec)
-    new CharArrayReader(Isabelle.system.symbols.decode(source.mkString).toArray)
+    new CharArrayReader(Isabelle_System.symbols.decode(source.mkString).toArray)
   }
 
   override def getTextReader(in: InputStream): Reader =
@@ -53,7 +53,7 @@
     val buffer = new ByteArrayOutputStream(BUFSIZE) {
       override def flush()
       {
-        val text = Isabelle.system.symbols.encode(toString(Standard_System.charset_name))
+        val text = Isabelle_System.symbols.encode(toString(Standard_System.charset_name))
         out.write(text.getBytes(Standard_System.charset))
         out.flush()
       }
diff -r bfc0bb115fa1 -r 39fdbd814c7f src/Tools/jEdit/src/isabelle_hyperlinks.scala
--- a/src/Tools/jEdit/src/isabelle_hyperlinks.scala	Mon Jul 04 20:18:19 2011 +0200
+++ b/src/Tools/jEdit/src/isabelle_hyperlinks.scala	Mon Jul 04 22:11:32 2011 +0200
@@ -28,7 +28,7 @@
   extends AbstractHyperlink(start, end, line, "")
 {
   override def click(view: View) = {
-    Isabelle.system.source_file(Path.explode(def_file)) match {
+    Isabelle_System.source_file(Path.explode(def_file)) match {
       case None =>
         Library.error_dialog(view, "File not found", "Could not find source file " + def_file)
       case Some(file) =>
diff -r bfc0bb115fa1 -r 39fdbd814c7f src/Tools/jEdit/src/isabelle_sidekick.scala
--- a/src/Tools/jEdit/src/isabelle_sidekick.scala	Mon Jul 04 20:18:19 2011 +0200
+++ b/src/Tools/jEdit/src/isabelle_sidekick.scala	Mon Jul 04 22:11:32 2011 +0200
@@ -96,7 +96,7 @@
             case Some((word, cs)) =>
               val ds =
                 (if (Isabelle_Encoding.is_active(buffer))
-                  cs.map(Isabelle.system.symbols.decode(_)).sortWith(_ < _)
+                  cs.map(Isabelle_System.symbols.decode(_)).sortWith(_ < _)
                  else cs).filter(_ != word)
               if (ds.isEmpty) null
               else new SideKickCompletion(
diff -r bfc0bb115fa1 -r 39fdbd814c7f src/Tools/jEdit/src/output_dockable.scala
--- a/src/Tools/jEdit/src/output_dockable.scala	Mon Jul 04 20:18:19 2011 +0200
+++ b/src/Tools/jEdit/src/output_dockable.scala	Mon Jul 04 22:11:32 2011 +0200
@@ -26,7 +26,7 @@
   Swing_Thread.require()
 
   private val html_panel =
-    new HTML_Panel(Isabelle.system, Isabelle.font_family(), scala.math.round(Isabelle.font_size()))
+    new HTML_Panel(Isabelle.font_family(), scala.math.round(Isabelle.font_size()))
   {
     override val handler: PartialFunction[HTML_Panel.Event, Unit] = {
       case HTML_Panel.Mouse_Click(elem, event) if elem.getClassName() == "sendback" =>
diff -r bfc0bb115fa1 -r 39fdbd814c7f src/Tools/jEdit/src/plugin.scala
--- a/src/Tools/jEdit/src/plugin.scala	Mon Jul 04 20:18:19 2011 +0200
+++ b/src/Tools/jEdit/src/plugin.scala	Mon Jul 04 22:11:32 2011 +0200
@@ -36,7 +36,6 @@
   /* plugin instance */
 
   var plugin: Plugin = null
-  var system: Isabelle_System = null
   var session: Session = null
 
 
@@ -200,7 +199,7 @@
           case Some(model) => Some(model)
           case None =>
             // FIXME strip protocol prefix of URL
-            Thy_Header.split_thy_path(system.posix_path(buffer.getPath)) match {
+            Thy_Header.split_thy_path(Isabelle_System.posix_path(buffer.getPath)) match {
               case Some((master_dir, thy_name)) =>
                 Some(Document_Model.init(session, buffer, master_dir, thy_name))
               case None => None
@@ -274,9 +273,9 @@
 
   def default_logic(): String =
   {
-    val logic = system.getenv("JEDIT_LOGIC")
+    val logic = Isabelle_System.getenv("JEDIT_LOGIC")
     if (logic != "") logic
-    else system.getenv_strict("ISABELLE_LOGIC")
+    else Isabelle_System.getenv_strict("ISABELLE_LOGIC")
   }
 
   class Logic_Entry(val name: String, val description: String)
@@ -288,7 +287,7 @@
   {
     val entries =
       new Logic_Entry("", "default (" + default_logic() + ")") ::
-        system.find_logics().map(name => new Logic_Entry(name, name))
+        Isabelle_System.find_logics().map(name => new Logic_Entry(name, name))
     val component = new ComboBox(entries)
     entries.find(_.name == logic) match {
       case None =>
@@ -301,7 +300,7 @@
   def start_session()
   {
     val timeout = Time_Property("startup-timeout", Time.seconds(10)) max Time.seconds(5)
-    val modes = system.getenv("JEDIT_PRINT_MODE").split(",").toList.map("-m" + _)
+    val modes = Isabelle_System.getenv("JEDIT_PRINT_MODE").split(",").toList.map("-m" + _)
     val logic = {
       val logic = Property("logic")
       if (logic != null && logic != "") logic
@@ -320,7 +319,7 @@
   {
     def read(path: Path): String =
     {
-      val platform_path = Isabelle.system.platform_path(path)
+      val platform_path = Isabelle_System.platform_path(path)
       val canonical_path = MiscUtilities.resolveSymlinks(platform_path)
 
       Isabelle.jedit_buffers().find(buffer =>
@@ -405,10 +404,10 @@
   {
     Isabelle.plugin = this
     Isabelle.setup_tooltips()
-    Isabelle.system = new Isabelle_System
-    Isabelle.system.install_fonts()
-    Isabelle.session = new Session(Isabelle.system, file_store)
-    SyntaxUtilities.setStyleExtender(new Token_Markup.Style_Extender(Isabelle.system.symbols))
+    Isabelle_System.init()
+    Isabelle_System.install_fonts()
+    Isabelle.session = new Session(file_store)
+    SyntaxUtilities.setStyleExtender(new Token_Markup.Style_Extender)
     if (ModeProvider.instance.isInstanceOf[ModeProvider])
       ModeProvider.instance = new Token_Markup.Mode_Provider(ModeProvider.instance)
     Isabelle.session.phase_changed += session_manager
diff -r bfc0bb115fa1 -r 39fdbd814c7f src/Tools/jEdit/src/scala_console.scala
--- a/src/Tools/jEdit/src/scala_console.scala	Mon Jul 04 20:18:19 2011 +0200
+++ b/src/Tools/jEdit/src/scala_console.scala	Mon Jul 04 22:11:32 2011 +0200
@@ -127,7 +127,7 @@
      "The following special toplevel bindings are provided:\n" +
      "  view      -- current jEdit/Swing view (e.g. view.getBuffer, view.getTextArea)\n" +
      "  console   -- jEdit Console plugin instance\n" +
-     "  Isabelle  -- Isabelle plugin instance (e.g. Isabelle.system, Isabelle.session)\n")
+     "  Isabelle  -- Isabelle plugin instance (e.g. Isabelle.session)\n")
   }
 
   override def printPrompt(console: Console, out: Output)
diff -r bfc0bb115fa1 -r 39fdbd814c7f src/Tools/jEdit/src/session_dockable.scala
--- a/src/Tools/jEdit/src/session_dockable.scala	Mon Jul 04 20:18:19 2011 +0200
+++ b/src/Tools/jEdit/src/session_dockable.scala	Mon Jul 04 22:11:32 2011 +0200
@@ -24,8 +24,8 @@
 {
   /* main tabs */
 
-  private val readme = new HTML_Panel(Isabelle.system, "SansSerif", 14)
-  readme.render_document(Isabelle.system.try_read(List(Path.explode("$JEDIT_HOME/README.html"))))
+  private val readme = new HTML_Panel("SansSerif", 14)
+  readme.render_document(Isabelle_System.try_read(List(Path.explode("$JEDIT_HOME/README.html"))))
 
   private val syslog = new TextArea(Isabelle.session.syslog())
   syslog.editable = false
diff -r bfc0bb115fa1 -r 39fdbd814c7f src/Tools/jEdit/src/token_markup.scala
--- a/src/Tools/jEdit/src/token_markup.scala	Mon Jul 04 20:18:19 2011 +0200
+++ b/src/Tools/jEdit/src/token_markup.scala	Mon Jul 04 22:11:32 2011 +0200
@@ -79,8 +79,9 @@
   private def bold_style(style: SyntaxStyle): SyntaxStyle =
     font_style(style, _.deriveFont(Font.BOLD))
 
-  class Style_Extender(symbols: Symbol.Interpretation) extends SyntaxUtilities.StyleExtender
+  class Style_Extender extends SyntaxUtilities.StyleExtender
   {
+    val symbols = Isabelle_System.symbols
     if (symbols.font_names.length > 2)
       error("Too many user symbol fonts (max 2 permitted): " + symbols.font_names.mkString(", "))
 
@@ -105,9 +106,10 @@
     }
   }
 
-  def extended_styles(symbols: Symbol.Interpretation, text: CharSequence)
-    : Map[Text.Offset, Byte => Byte] =
+  def extended_styles(text: CharSequence): Map[Text.Offset, Byte => Byte] =
   {
+    val symbols = Isabelle_System.symbols
+
     // FIXME symbols.bsub_decoded etc.
     def ctrl_style(sym: String): Option[Byte => Byte] =
       if (symbols.is_subscript_decoded(sym)) Some(subscript(_))
@@ -163,7 +165,6 @@
     {
       val context1 =
         if (Isabelle.session.is_ready) {
-          val symbols = Isabelle.system.symbols
           val syntax = Isabelle.session.current_syntax()
     
           val ctxt =
@@ -174,7 +175,7 @@
           val (tokens, ctxt1) = syntax.scan_context(line, ctxt)
           val context1 = new Line_Context(ctxt1)
     
-          val extended = extended_styles(symbols, line)
+          val extended = extended_styles(line)
     
           var offset = 0
           for (token <- tokens) {