quasi-static Isabelle_System -- reduced tendency towards "functorial style";
authorwenzelm
Mon Jul 04 22:11:32 2011 +0200 (2011-07-04)
changeset 4366139fdbd814c7f
parent 43660 bfc0bb115fa1
child 43662 e3175ec00311
quasi-static Isabelle_System -- reduced tendency towards "functorial style";
src/Pure/System/gui_setup.scala
src/Pure/System/isabelle_process.scala
src/Pure/System/isabelle_system.scala
src/Pure/System/session.scala
src/Pure/System/session_manager.scala
src/Pure/System/standard_system.scala
src/Pure/Thy/html.scala
src/Pure/Thy/thy_header.scala
src/Tools/jEdit/src/document_model.scala
src/Tools/jEdit/src/document_view.scala
src/Tools/jEdit/src/html_panel.scala
src/Tools/jEdit/src/isabelle_encoding.scala
src/Tools/jEdit/src/isabelle_hyperlinks.scala
src/Tools/jEdit/src/isabelle_sidekick.scala
src/Tools/jEdit/src/output_dockable.scala
src/Tools/jEdit/src/plugin.scala
src/Tools/jEdit/src/scala_console.scala
src/Tools/jEdit/src/session_dockable.scala
src/Tools/jEdit/src/token_markup.scala
     1.1 --- a/src/Pure/System/gui_setup.scala	Mon Jul 04 20:18:19 2011 +0200
     1.2 +++ b/src/Pure/System/gui_setup.scala	Mon Jul 04 22:11:32 2011 +0200
     1.3 @@ -44,14 +44,15 @@
     1.4      text.append("JVM name: " + Platform.jvm_name + "\n")
     1.5      text.append("JVM platform: " + Platform.jvm_platform + "\n")
     1.6      try {
     1.7 -      val isabelle_system = Isabelle_System.default
     1.8 -      text.append("ML platform: " + isabelle_system.getenv("ML_PLATFORM") + "\n")
     1.9 -      text.append("Isabelle platform: " + isabelle_system.getenv("ISABELLE_PLATFORM") + "\n")
    1.10 -      val platform64 = isabelle_system.getenv("ISABELLE_PLATFORM64")
    1.11 +      Isabelle_System.init()
    1.12 +      text.append("ML platform: " + Isabelle_System.getenv("ML_PLATFORM") + "\n")
    1.13 +      text.append("Isabelle platform: " + Isabelle_System.getenv("ISABELLE_PLATFORM") + "\n")
    1.14 +      val platform64 = Isabelle_System.getenv("ISABELLE_PLATFORM64")
    1.15        if (platform64 != "") text.append("Isabelle platform (64 bit): " + platform64 + "\n")
    1.16 -      text.append("Isabelle home: " + isabelle_system.getenv("ISABELLE_HOME") + "\n")
    1.17 -      text.append("Isabelle java: " + isabelle_system.this_java() + "\n")
    1.18 -    } catch { case ERROR(msg) => text.append(msg + "\n") }
    1.19 +      text.append("Isabelle home: " + Isabelle_System.getenv("ISABELLE_HOME") + "\n")
    1.20 +      text.append("Isabelle java: " + Isabelle_System.getenv("THIS_JAVA") + "\n")
    1.21 +    }
    1.22 +    catch { case ERROR(msg) => text.append(msg + "\n") }
    1.23  
    1.24      // reactions
    1.25      listenTo(ok)
     2.1 --- a/src/Pure/System/isabelle_process.scala	Mon Jul 04 20:18:19 2011 +0200
     2.2 +++ b/src/Pure/System/isabelle_process.scala	Mon Jul 04 22:11:32 2011 +0200
     2.3 @@ -62,7 +62,7 @@
     2.4  }
     2.5  
     2.6  
     2.7 -class Isabelle_Process(system: Isabelle_System, timeout: Time, receiver: Actor, args: String*)
     2.8 +class Isabelle_Process(timeout: Time, receiver: Actor, args: String*)
     2.9  {
    2.10    import Isabelle_Process._
    2.11  
    2.12 @@ -70,8 +70,7 @@
    2.13    /* demo constructor */
    2.14  
    2.15    def this(args: String*) =
    2.16 -    this(Isabelle_System.default, Time.seconds(10),
    2.17 -      actor { loop { react { case res => Console.println(res) } } }, args: _*)
    2.18 +    this(Time.seconds(10), actor { loop { react { case res => Console.println(res) } } }, args: _*)
    2.19  
    2.20  
    2.21    /* results */
    2.22 @@ -93,7 +92,7 @@
    2.23  
    2.24    private def put_result(kind: String, text: String)
    2.25    {
    2.26 -    put_result(kind, Nil, List(XML.Text(system.symbols.decode(text))))
    2.27 +    put_result(kind, Nil, List(XML.Text(Isabelle_System.symbols.decode(text))))
    2.28    }
    2.29  
    2.30  
    2.31 @@ -117,15 +116,16 @@
    2.32  
    2.33    /** process manager **/
    2.34  
    2.35 -  private val in_fifo = system.mk_fifo()
    2.36 -  private val out_fifo = system.mk_fifo()
    2.37 -  private def rm_fifos() { system.rm_fifo(in_fifo); system.rm_fifo(out_fifo) }
    2.38 +  private val in_fifo = Isabelle_System.mk_fifo()
    2.39 +  private val out_fifo = Isabelle_System.mk_fifo()
    2.40 +  private def rm_fifos() { Isabelle_System.rm_fifo(in_fifo); Isabelle_System.rm_fifo(out_fifo) }
    2.41  
    2.42    private val process =
    2.43      try {
    2.44        val cmdline =
    2.45 -        List(system.getenv_strict("ISABELLE_PROCESS"), "-W", in_fifo + ":" + out_fifo) ++ args
    2.46 -      new system.Managed_Process(true, cmdline: _*)
    2.47 +        List(Isabelle_System.getenv_strict("ISABELLE_PROCESS"), "-W",
    2.48 +          in_fifo + ":" + out_fifo) ++ args
    2.49 +      new Isabelle_System.Managed_Process(true, cmdline: _*)
    2.50      }
    2.51      catch { case e: IOException => rm_fifos(); throw(e) }
    2.52  
    2.53 @@ -168,8 +168,8 @@
    2.54      }
    2.55      else {
    2.56        // rendezvous
    2.57 -      val command_stream = system.fifo_output_stream(in_fifo)
    2.58 -      val message_stream = system.fifo_input_stream(out_fifo)
    2.59 +      val command_stream = Isabelle_System.fifo_output_stream(in_fifo)
    2.60 +      val message_stream = Isabelle_System.fifo_input_stream(out_fifo)
    2.61  
    2.62        standard_input = stdin_actor()
    2.63        val stdout = stdout_actor()
    2.64 @@ -341,7 +341,7 @@
    2.65  
    2.66          if (i != n) throw new Protocol_Error("bad message chunk content")
    2.67  
    2.68 -        YXML.parse_body_failsafe(YXML.decode_chars(system.symbols.decode, buf, 0, n))
    2.69 +        YXML.parse_body_failsafe(YXML.decode_chars(Isabelle_System.symbols.decode, buf, 0, n))
    2.70          //}}}
    2.71        }
    2.72  
     3.1 --- a/src/Pure/System/isabelle_system.scala	Mon Jul 04 20:18:19 2011 +0200
     3.2 +++ b/src/Pure/System/isabelle_system.scala	Mon Jul 04 22:11:32 2011 +0200
     3.3 @@ -1,7 +1,8 @@
     3.4  /*  Title:      Pure/System/isabelle_system.scala
     3.5      Author:     Makarius
     3.6  
     3.7 -Isabelle system support (settings environment etc.).
     3.8 +Fundamental Isabelle system environment: settings, symbols etc.
     3.9 +Quasi-static module with optional init operation.
    3.10  */
    3.11  
    3.12  package isabelle
    3.13 @@ -21,15 +22,24 @@
    3.14  
    3.15  object Isabelle_System
    3.16  {
    3.17 -  lazy val default: Isabelle_System = new Isabelle_System
    3.18 -}
    3.19 +  /** implicit state **/
    3.20 +
    3.21 +  private case class State(
    3.22 +    standard_system: Standard_System,
    3.23 +    settings: Map[String, String],
    3.24 +    symbols: Symbol.Interpretation)
    3.25 +
    3.26 +  @volatile private var _state: Option[State] = None
    3.27  
    3.28 -class Isabelle_System(this_isabelle_home: String) extends Standard_System
    3.29 -{
    3.30 -  def this() = this(null)
    3.31 +  private def check_state(): State =
    3.32 +  {
    3.33 +    if (_state.isEmpty) init()  // unsynchronized check
    3.34 +    _state.get
    3.35 +  }
    3.36  
    3.37 -
    3.38 -  /** Isabelle environment **/
    3.39 +  def standard_system: Standard_System = check_state().standard_system
    3.40 +  def settings: Map[String, String] = check_state().settings
    3.41 +  def symbols: Symbol.Interpretation = check_state().symbols
    3.42  
    3.43    /*
    3.44      isabelle_home precedence:
    3.45 @@ -37,50 +47,67 @@
    3.46        (2) ISABELLE_HOME process environment variable (e.g. inherited from running isabelle tool)
    3.47        (3) isabelle.home system property (e.g. via JVM application boot process)
    3.48    */
    3.49 +  def init(this_isabelle_home: String = null) = synchronized {
    3.50 +    if (_state.isEmpty) {
    3.51 +      import scala.collection.JavaConversions._
    3.52  
    3.53 -  private val environment: Map[String, String] =
    3.54 -  {
    3.55 -    import scala.collection.JavaConversions._
    3.56 +      val standard_system = new Standard_System
    3.57  
    3.58 -    val env0 = Map(System.getenv.toList: _*) +
    3.59 -      ("THIS_JAVA" -> this_java())
    3.60 +      val settings =
    3.61 +      {
    3.62 +        val env = Map(System.getenv.toList: _*) +
    3.63 +          ("THIS_JAVA" -> standard_system.this_java())
    3.64  
    3.65 -    val isabelle_home =
    3.66 -      if (this_isabelle_home != null) this_isabelle_home
    3.67 -      else
    3.68 -        env0.get("ISABELLE_HOME") match {
    3.69 -          case None | Some("") =>
    3.70 -            val path = System.getProperty("isabelle.home")
    3.71 -            if (path == null || path == "") error("Unknown Isabelle home directory")
    3.72 -            else path
    3.73 -          case Some(path) => path
    3.74 -        }
    3.75 +        val isabelle_home =
    3.76 +          if (this_isabelle_home != null) this_isabelle_home
    3.77 +          else
    3.78 +            env.get("ISABELLE_HOME") match {
    3.79 +              case None | Some("") =>
    3.80 +                val path = System.getProperty("isabelle.home")
    3.81 +                if (path == null || path == "") error("Unknown Isabelle home directory")
    3.82 +                else path
    3.83 +              case Some(path) => path
    3.84 +            }
    3.85  
    3.86 -    Standard_System.with_tmp_file("settings") { dump =>
    3.87 -        val shell_prefix =
    3.88 -          if (Platform.is_windows) List(platform_root + "\\bin\\bash", "-l") else Nil
    3.89 -        val cmdline =
    3.90 -          shell_prefix ::: List(isabelle_home + "/bin/isabelle", "getenv", "-d", dump.toString)
    3.91 -        val (output, rc) = Standard_System.raw_exec(null, env0, true, cmdline: _*)
    3.92 -        if (rc != 0) error(output)
    3.93 +          Standard_System.with_tmp_file("settings") { dump =>
    3.94 +              val shell_prefix =
    3.95 +                if (Platform.is_windows) List(standard_system.platform_root + "\\bin\\bash", "-l")
    3.96 +                else Nil
    3.97 +              val cmdline =
    3.98 +                shell_prefix ::: List(isabelle_home + "/bin/isabelle", "getenv", "-d", dump.toString)
    3.99 +              val (output, rc) = Standard_System.raw_exec(null, env, true, cmdline: _*)
   3.100 +              if (rc != 0) error(output)
   3.101  
   3.102 -        val entries =
   3.103 -          for (entry <- Source.fromFile(dump).mkString split "\0" if entry != "") yield {
   3.104 -            val i = entry.indexOf('=')
   3.105 -            if (i <= 0) (entry -> "")
   3.106 -            else (entry.substring(0, i) -> entry.substring(i + 1))
   3.107 +              val entries =
   3.108 +                for (entry <- Source.fromFile(dump).mkString split "\0" if entry != "") yield {
   3.109 +                  val i = entry.indexOf('=')
   3.110 +                  if (i <= 0) (entry -> "")
   3.111 +                  else (entry.substring(0, i) -> entry.substring(i + 1))
   3.112 +                }
   3.113 +              Map(entries: _*) +
   3.114 +                ("HOME" -> System.getenv("HOME")) +
   3.115 +                ("PATH" -> System.getenv("PATH"))
   3.116 +            }
   3.117            }
   3.118 -        Map(entries: _*) +
   3.119 -          ("HOME" -> System.getenv("HOME")) +
   3.120 -          ("PATH" -> System.getenv("PATH"))
   3.121 +
   3.122 +      val symbols =
   3.123 +      {
   3.124 +        val isabelle_symbols = settings.getOrElse("ISABELLE_SYMBOLS", "")
   3.125 +        if (isabelle_symbols == "") error("Undefined environment variable: ISABELLE_SYMBOLS")
   3.126 +        val files =
   3.127 +          isabelle_symbols.split(":").toList.map(s => new File(standard_system.jvm_path(s)))
   3.128 +        new Symbol.Interpretation(Standard_System.try_read(files).split("\n").toList)
   3.129        }
   3.130 +
   3.131 +      _state = Some(State(standard_system, settings, symbols))
   3.132 +    }
   3.133    }
   3.134  
   3.135  
   3.136    /* getenv */
   3.137  
   3.138    def getenv(name: String): String =
   3.139 -    environment.getOrElse(if (name == "HOME") "HOME_JVM" else name, "")
   3.140 +    settings.getOrElse(if (name == "HOME") "HOME_JVM" else name, "")
   3.141  
   3.142    def getenv_strict(name: String): String =
   3.143    {
   3.144 @@ -88,9 +115,6 @@
   3.145      if (value != "") value else error("Undefined environment variable: " + name)
   3.146    }
   3.147  
   3.148 -  override def toString = getenv_strict("ISABELLE_HOME")
   3.149 -
   3.150 -
   3.151  
   3.152    /** file-system operations **/
   3.153  
   3.154 @@ -98,9 +122,11 @@
   3.155  
   3.156    def standard_path(path: Path): String = path.expand(getenv_strict).implode
   3.157  
   3.158 -  def platform_path(path: Path): String = jvm_path(standard_path(path))
   3.159 +  def platform_path(path: Path): String = standard_system.jvm_path(standard_path(path))
   3.160    def platform_file(path: Path) = new File(platform_path(path))
   3.161  
   3.162 +  def posix_path(jvm_path: String): String = standard_system.posix_path(jvm_path)
   3.163 +
   3.164  
   3.165    /* try_read */
   3.166  
   3.167 @@ -142,9 +168,9 @@
   3.168    def execute(redirect: Boolean, args: String*): Process =
   3.169    {
   3.170      val cmdline =
   3.171 -      if (Platform.is_windows) List(platform_root + "\\bin\\env.exe") ++ args
   3.172 +      if (Platform.is_windows) List(standard_system.platform_root + "\\bin\\env.exe") ++ args
   3.173        else args
   3.174 -    Standard_System.raw_execute(null, environment, redirect, cmdline: _*)
   3.175 +    Standard_System.raw_execute(null, settings, redirect, cmdline: _*)
   3.176    }
   3.177  
   3.178  
   3.179 @@ -271,7 +297,7 @@
   3.180    }
   3.181  
   3.182    def rm_fifo(fifo: String): Boolean =
   3.183 -    (new File(jvm_path(if (Platform.is_windows) fifo + ".lnk" else fifo))).delete
   3.184 +    (new File(standard_system.jvm_path(if (Platform.is_windows) fifo + ".lnk" else fifo))).delete
   3.185  
   3.186    def fifo_input_stream(fifo: String): InputStream =
   3.187    {
   3.188 @@ -328,13 +354,6 @@
   3.189    }
   3.190  
   3.191  
   3.192 -  /* symbols */
   3.193 -
   3.194 -  val symbols = new Symbol.Interpretation(
   3.195 -    try_read(getenv_strict("ISABELLE_SYMBOLS").split(":").toList.map(Path.explode))
   3.196 -      .split("\n").toList)
   3.197 -
   3.198 -
   3.199    /* fonts */
   3.200  
   3.201    def get_font(family: String = "IsabelleText", size: Int = 1, bold: Boolean = false): Font =
     4.1 --- a/src/Pure/System/session.scala	Mon Jul 04 20:18:19 2011 +0200
     4.2 +++ b/src/Pure/System/session.scala	Mon Jul 04 22:11:32 2011 +0200
     4.3 @@ -40,7 +40,7 @@
     4.4  }
     4.5  
     4.6  
     4.7 -class Session(val system: Isabelle_System, val file_store: Session.File_Store)
     4.8 +class Session(val file_store: Session.File_Store)
     4.9  {
    4.10    /* real time parameters */  // FIXME properties or settings (!?)
    4.11  
    4.12 @@ -117,7 +117,7 @@
    4.13  
    4.14    val new_id = new Counter
    4.15  
    4.16 -  @volatile private var syntax = new Outer_Syntax(system.symbols)
    4.17 +  @volatile private var syntax = new Outer_Syntax(Isabelle_System.symbols)
    4.18    def current_syntax(): Outer_Syntax = syntax
    4.19  
    4.20    @volatile private var reverse_syslog = List[XML.Elem]()
    4.21 @@ -138,16 +138,14 @@
    4.22  
    4.23    /* theory files */
    4.24  
    4.25 -  val thy_header = new Thy_Header(system.symbols)
    4.26 -
    4.27    val thy_load = new Thy_Load
    4.28    {
    4.29      override def check_thy(dir: Path, name: String): (String, Thy_Header.Header) =
    4.30      {
    4.31 -      val file = system.platform_file(dir + Thy_Header.thy_path(name))
    4.32 +      val file = Isabelle_System.platform_file(dir + Thy_Header.thy_path(name))
    4.33        if (!file.exists || !file.isFile) error("No such file: " + quote(file.toString))
    4.34        val text = Standard_System.read_file(file)
    4.35 -      val header = thy_header.read(text)
    4.36 +      val header = Thy_Header.read(text)
    4.37        (text, header)
    4.38      }
    4.39    }
    4.40 @@ -202,7 +200,8 @@
    4.41                          if (global_state.peek().lookup_command(command.id).isEmpty) {
    4.42                            global_state.change(_.define_command(command))
    4.43                            prover.get.
    4.44 -                            define_command(command.id, system.symbols.encode(command.source))
    4.45 +                            define_command(command.id,
    4.46 +                              Isabelle_System.symbols.encode(command.source))
    4.47                          }
    4.48                          Some(command.id)
    4.49                      }
    4.50 @@ -311,8 +310,7 @@
    4.51          case Start(timeout, args) if prover.isEmpty =>
    4.52            if (phase == Session.Inactive || phase == Session.Failed) {
    4.53              phase = Session.Startup
    4.54 -            prover =
    4.55 -              Some(new Isabelle_Process(system, timeout, this_actor, args:_*) with Isar_Document)
    4.56 +            prover = Some(new Isabelle_Process(timeout, this_actor, args:_*) with Isar_Document)
    4.57            }
    4.58  
    4.59          case Stop =>
     5.1 --- a/src/Pure/System/session_manager.scala	Mon Jul 04 20:18:19 2011 +0200
     5.2 +++ b/src/Pure/System/session_manager.scala	Mon Jul 04 22:11:32 2011 +0200
     5.3 @@ -10,7 +10,7 @@
     5.4  import java.io.{File, FileFilter}
     5.5  
     5.6  
     5.7 -class Session_Manager(system: Isabelle_System)
     5.8 +class Session_Manager
     5.9  {
    5.10    val ROOT_NAME = "session.root"
    5.11  
    5.12 @@ -42,7 +42,8 @@
    5.13    def component_sessions(): List[List[String]] =
    5.14    {
    5.15      val toplevel_sessions =
    5.16 -      system.components().map(s => system.platform_file(Path.explode(s))).filter(is_session_dir)
    5.17 +      Isabelle_System.components().map(s =>
    5.18 +        Isabelle_System.platform_file(Path.explode(s))).filter(is_session_dir)
    5.19      ((Nil: List[List[String]]) /: toplevel_sessions)(find_sessions(Nil, _, _)).reverse
    5.20    }
    5.21  }
     6.1 --- a/src/Pure/System/standard_system.scala	Mon Jul 04 20:18:19 2011 +0200
     6.2 +++ b/src/Pure/System/standard_system.scala	Mon Jul 04 22:11:32 2011 +0200
     6.3 @@ -96,6 +96,16 @@
     6.4  
     6.5    def read_file(file: File): String = slurp(new FileInputStream(file))
     6.6  
     6.7 +  def try_read(files: Seq[File]): String =
     6.8 +  {
     6.9 +    val buf = new StringBuilder
    6.10 +    for {
    6.11 +      file <- files if file.isFile
    6.12 +      c <- (Source.fromFile(file) ++ Iterator.single('\n'))
    6.13 +    } buf.append(c)
    6.14 +    buf.toString
    6.15 +  }
    6.16 +
    6.17    def write_file(file: File, text: CharSequence)
    6.18    {
    6.19      val writer =
     7.1 --- a/src/Pure/Thy/html.scala	Mon Jul 04 20:18:19 2011 +0200
     7.2 +++ b/src/Pure/Thy/html.scala	Mon Jul 04 22:11:32 2011 +0200
     7.3 @@ -55,9 +55,10 @@
     7.4    def sup(txt: String): XML.Elem = XML.elem("sup", List(XML.Text(txt)))
     7.5    def bold(txt: String): XML.Elem = span("bold", List(XML.Text(txt)))
     7.6  
     7.7 -  def spans(symbols: Symbol.Interpretation,
     7.8 -    input: XML.Tree, original_data: Boolean = false): XML.Body =
     7.9 +  def spans(input: XML.Tree, original_data: Boolean = false): XML.Body =
    7.10    {
    7.11 +    val symbols = Isabelle_System.symbols
    7.12 +
    7.13      def html_spans(tree: XML.Tree): XML.Body =
    7.14        tree match {
    7.15          case XML.Elem(m @ Markup(name, props), ts) =>
     8.1 --- a/src/Pure/Thy/thy_header.scala	Mon Jul 04 20:18:19 2011 +0200
     8.2 +++ b/src/Pure/Thy/thy_header.scala	Mon Jul 04 22:11:32 2011 +0200
     8.3 @@ -15,7 +15,7 @@
     8.4  import java.io.File
     8.5  
     8.6  
     8.7 -object Thy_Header
     8.8 +object Thy_Header extends Parse.Parser
     8.9  {
    8.10    val HEADER = "header"
    8.11    val THEORY = "theory"
    8.12 @@ -47,12 +47,6 @@
    8.13        case Thy_Path2(dir, name) => Some((dir, name))
    8.14        case _ => None
    8.15      }
    8.16 -}
    8.17 -
    8.18 -
    8.19 -class Thy_Header(symbols: Symbol.Interpretation) extends Parse.Parser
    8.20 -{
    8.21 -  import Thy_Header._
    8.22  
    8.23  
    8.24    /* header */
    8.25 @@ -81,7 +75,7 @@
    8.26  
    8.27    def read(reader: Reader[Char]): Header =
    8.28    {
    8.29 -    val token = lexicon.token(symbols, _ => false)
    8.30 +    val token = lexicon.token(Isabelle_System.symbols, _ => false)
    8.31      val toks = new mutable.ListBuffer[Token]
    8.32  
    8.33      @tailrec def scan_to_begin(in: Reader[Char])
    8.34 @@ -119,6 +113,6 @@
    8.35      val header = read(source)
    8.36      val name1 = header.name
    8.37      if (name == name1) header
    8.38 -    else error("Bad file name " + Thy_Header.thy_path(name) + " for theory " + quote(name1))
    8.39 +    else error("Bad file name " + thy_path(name) + " for theory " + quote(name1))
    8.40    }
    8.41  }
     9.1 --- a/src/Tools/jEdit/src/document_model.scala	Mon Jul 04 20:18:19 2011 +0200
     9.2 +++ b/src/Tools/jEdit/src/document_model.scala	Mon Jul 04 22:11:32 2011 +0200
     9.3 @@ -63,7 +63,7 @@
     9.4  
     9.5    private def capture_header(): Exn.Result[Thy_Header.Header] =
     9.6      Exn.capture {
     9.7 -      session.thy_header.check(thy_name, buffer.getSegment(0, buffer.getLength))
     9.8 +      Thy_Header.check(thy_name, buffer.getSegment(0, buffer.getLength))
     9.9      }
    9.10  
    9.11    private object pending_edits  // owned by Swing thread
    10.1 --- a/src/Tools/jEdit/src/document_view.scala	Mon Jul 04 20:18:19 2011 +0200
    10.2 +++ b/src/Tools/jEdit/src/document_view.scala	Mon Jul 04 22:11:32 2011 +0200
    10.3 @@ -143,7 +143,7 @@
    10.4    private def exit_popup() { html_popup.map(_.hide) }
    10.5  
    10.6    private val html_panel =
    10.7 -    new HTML_Panel(Isabelle.system, Isabelle.font_family(), scala.math.round(Isabelle.font_size()))
    10.8 +    new HTML_Panel(Isabelle.font_family(), scala.math.round(Isabelle.font_size()))
    10.9    html_panel.setBorder(BorderFactory.createLineBorder(Color.black))
   10.10  
   10.11    private def html_panel_resize()
    11.1 --- a/src/Tools/jEdit/src/html_panel.scala	Mon Jul 04 20:18:19 2011 +0200
    11.2 +++ b/src/Tools/jEdit/src/html_panel.scala	Mon Jul 04 22:11:32 2011 +0200
    11.3 @@ -37,11 +37,7 @@
    11.4  }
    11.5  
    11.6  
    11.7 -class HTML_Panel(
    11.8 -    system: Isabelle_System,
    11.9 -    initial_font_family: String,
   11.10 -    initial_font_size: Int)
   11.11 -  extends HtmlPanel
   11.12 +class HTML_Panel(initial_font_family: String, initial_font_size: Int) extends HtmlPanel
   11.13  {
   11.14    /** Lobo setup **/
   11.15  
   11.16 @@ -96,7 +92,8 @@
   11.17  <head>
   11.18  <style media="all" type="text/css">
   11.19  """ +
   11.20 -  system.try_read(system.getenv_strict("JEDIT_STYLE_SHEETS").split(":").map(Path.explode))
   11.21 +  Isabelle_System.try_read(
   11.22 +    Isabelle_System.getenv_strict("JEDIT_STYLE_SHEETS").split(":").map(Path.explode))
   11.23  
   11.24    private val template_tail =
   11.25  """
   11.26 @@ -168,8 +165,7 @@
   11.27          current_body.flatMap(div =>
   11.28            Pretty.formatted(List(div), current_margin, Pretty.font_metric(current_font_metrics))
   11.29              .map(t =>
   11.30 -              XML.Elem(Markup(HTML.PRE, List((HTML.CLASS, Markup.MESSAGE))),
   11.31 -                HTML.spans(system.symbols, t, true))))
   11.32 +              XML.Elem(Markup(HTML.PRE, List((HTML.CLASS, Markup.MESSAGE))), HTML.spans(t, true))))
   11.33        val doc =
   11.34          builder.parse(
   11.35            new InputSourceImpl(
    12.1 --- a/src/Tools/jEdit/src/isabelle_encoding.scala	Mon Jul 04 20:18:19 2011 +0200
    12.2 +++ b/src/Tools/jEdit/src/isabelle_encoding.scala	Mon Jul 04 22:11:32 2011 +0200
    12.3 @@ -34,7 +34,7 @@
    12.4    private def text_reader(in: InputStream, codec: Codec): Reader =
    12.5    {
    12.6      val source = new BufferedSource(in)(codec)
    12.7 -    new CharArrayReader(Isabelle.system.symbols.decode(source.mkString).toArray)
    12.8 +    new CharArrayReader(Isabelle_System.symbols.decode(source.mkString).toArray)
    12.9    }
   12.10  
   12.11    override def getTextReader(in: InputStream): Reader =
   12.12 @@ -53,7 +53,7 @@
   12.13      val buffer = new ByteArrayOutputStream(BUFSIZE) {
   12.14        override def flush()
   12.15        {
   12.16 -        val text = Isabelle.system.symbols.encode(toString(Standard_System.charset_name))
   12.17 +        val text = Isabelle_System.symbols.encode(toString(Standard_System.charset_name))
   12.18          out.write(text.getBytes(Standard_System.charset))
   12.19          out.flush()
   12.20        }
    13.1 --- a/src/Tools/jEdit/src/isabelle_hyperlinks.scala	Mon Jul 04 20:18:19 2011 +0200
    13.2 +++ b/src/Tools/jEdit/src/isabelle_hyperlinks.scala	Mon Jul 04 22:11:32 2011 +0200
    13.3 @@ -28,7 +28,7 @@
    13.4    extends AbstractHyperlink(start, end, line, "")
    13.5  {
    13.6    override def click(view: View) = {
    13.7 -    Isabelle.system.source_file(Path.explode(def_file)) match {
    13.8 +    Isabelle_System.source_file(Path.explode(def_file)) match {
    13.9        case None =>
   13.10          Library.error_dialog(view, "File not found", "Could not find source file " + def_file)
   13.11        case Some(file) =>
    14.1 --- a/src/Tools/jEdit/src/isabelle_sidekick.scala	Mon Jul 04 20:18:19 2011 +0200
    14.2 +++ b/src/Tools/jEdit/src/isabelle_sidekick.scala	Mon Jul 04 22:11:32 2011 +0200
    14.3 @@ -96,7 +96,7 @@
    14.4              case Some((word, cs)) =>
    14.5                val ds =
    14.6                  (if (Isabelle_Encoding.is_active(buffer))
    14.7 -                  cs.map(Isabelle.system.symbols.decode(_)).sortWith(_ < _)
    14.8 +                  cs.map(Isabelle_System.symbols.decode(_)).sortWith(_ < _)
    14.9                   else cs).filter(_ != word)
   14.10                if (ds.isEmpty) null
   14.11                else new SideKickCompletion(
    15.1 --- a/src/Tools/jEdit/src/output_dockable.scala	Mon Jul 04 20:18:19 2011 +0200
    15.2 +++ b/src/Tools/jEdit/src/output_dockable.scala	Mon Jul 04 22:11:32 2011 +0200
    15.3 @@ -26,7 +26,7 @@
    15.4    Swing_Thread.require()
    15.5  
    15.6    private val html_panel =
    15.7 -    new HTML_Panel(Isabelle.system, Isabelle.font_family(), scala.math.round(Isabelle.font_size()))
    15.8 +    new HTML_Panel(Isabelle.font_family(), scala.math.round(Isabelle.font_size()))
    15.9    {
   15.10      override val handler: PartialFunction[HTML_Panel.Event, Unit] = {
   15.11        case HTML_Panel.Mouse_Click(elem, event) if elem.getClassName() == "sendback" =>
    16.1 --- a/src/Tools/jEdit/src/plugin.scala	Mon Jul 04 20:18:19 2011 +0200
    16.2 +++ b/src/Tools/jEdit/src/plugin.scala	Mon Jul 04 22:11:32 2011 +0200
    16.3 @@ -36,7 +36,6 @@
    16.4    /* plugin instance */
    16.5  
    16.6    var plugin: Plugin = null
    16.7 -  var system: Isabelle_System = null
    16.8    var session: Session = null
    16.9  
   16.10  
   16.11 @@ -200,7 +199,7 @@
   16.12            case Some(model) => Some(model)
   16.13            case None =>
   16.14              // FIXME strip protocol prefix of URL
   16.15 -            Thy_Header.split_thy_path(system.posix_path(buffer.getPath)) match {
   16.16 +            Thy_Header.split_thy_path(Isabelle_System.posix_path(buffer.getPath)) match {
   16.17                case Some((master_dir, thy_name)) =>
   16.18                  Some(Document_Model.init(session, buffer, master_dir, thy_name))
   16.19                case None => None
   16.20 @@ -274,9 +273,9 @@
   16.21  
   16.22    def default_logic(): String =
   16.23    {
   16.24 -    val logic = system.getenv("JEDIT_LOGIC")
   16.25 +    val logic = Isabelle_System.getenv("JEDIT_LOGIC")
   16.26      if (logic != "") logic
   16.27 -    else system.getenv_strict("ISABELLE_LOGIC")
   16.28 +    else Isabelle_System.getenv_strict("ISABELLE_LOGIC")
   16.29    }
   16.30  
   16.31    class Logic_Entry(val name: String, val description: String)
   16.32 @@ -288,7 +287,7 @@
   16.33    {
   16.34      val entries =
   16.35        new Logic_Entry("", "default (" + default_logic() + ")") ::
   16.36 -        system.find_logics().map(name => new Logic_Entry(name, name))
   16.37 +        Isabelle_System.find_logics().map(name => new Logic_Entry(name, name))
   16.38      val component = new ComboBox(entries)
   16.39      entries.find(_.name == logic) match {
   16.40        case None =>
   16.41 @@ -301,7 +300,7 @@
   16.42    def start_session()
   16.43    {
   16.44      val timeout = Time_Property("startup-timeout", Time.seconds(10)) max Time.seconds(5)
   16.45 -    val modes = system.getenv("JEDIT_PRINT_MODE").split(",").toList.map("-m" + _)
   16.46 +    val modes = Isabelle_System.getenv("JEDIT_PRINT_MODE").split(",").toList.map("-m" + _)
   16.47      val logic = {
   16.48        val logic = Property("logic")
   16.49        if (logic != null && logic != "") logic
   16.50 @@ -320,7 +319,7 @@
   16.51    {
   16.52      def read(path: Path): String =
   16.53      {
   16.54 -      val platform_path = Isabelle.system.platform_path(path)
   16.55 +      val platform_path = Isabelle_System.platform_path(path)
   16.56        val canonical_path = MiscUtilities.resolveSymlinks(platform_path)
   16.57  
   16.58        Isabelle.jedit_buffers().find(buffer =>
   16.59 @@ -405,10 +404,10 @@
   16.60    {
   16.61      Isabelle.plugin = this
   16.62      Isabelle.setup_tooltips()
   16.63 -    Isabelle.system = new Isabelle_System
   16.64 -    Isabelle.system.install_fonts()
   16.65 -    Isabelle.session = new Session(Isabelle.system, file_store)
   16.66 -    SyntaxUtilities.setStyleExtender(new Token_Markup.Style_Extender(Isabelle.system.symbols))
   16.67 +    Isabelle_System.init()
   16.68 +    Isabelle_System.install_fonts()
   16.69 +    Isabelle.session = new Session(file_store)
   16.70 +    SyntaxUtilities.setStyleExtender(new Token_Markup.Style_Extender)
   16.71      if (ModeProvider.instance.isInstanceOf[ModeProvider])
   16.72        ModeProvider.instance = new Token_Markup.Mode_Provider(ModeProvider.instance)
   16.73      Isabelle.session.phase_changed += session_manager
    17.1 --- a/src/Tools/jEdit/src/scala_console.scala	Mon Jul 04 20:18:19 2011 +0200
    17.2 +++ b/src/Tools/jEdit/src/scala_console.scala	Mon Jul 04 22:11:32 2011 +0200
    17.3 @@ -127,7 +127,7 @@
    17.4       "The following special toplevel bindings are provided:\n" +
    17.5       "  view      -- current jEdit/Swing view (e.g. view.getBuffer, view.getTextArea)\n" +
    17.6       "  console   -- jEdit Console plugin instance\n" +
    17.7 -     "  Isabelle  -- Isabelle plugin instance (e.g. Isabelle.system, Isabelle.session)\n")
    17.8 +     "  Isabelle  -- Isabelle plugin instance (e.g. Isabelle.session)\n")
    17.9    }
   17.10  
   17.11    override def printPrompt(console: Console, out: Output)
    18.1 --- a/src/Tools/jEdit/src/session_dockable.scala	Mon Jul 04 20:18:19 2011 +0200
    18.2 +++ b/src/Tools/jEdit/src/session_dockable.scala	Mon Jul 04 22:11:32 2011 +0200
    18.3 @@ -24,8 +24,8 @@
    18.4  {
    18.5    /* main tabs */
    18.6  
    18.7 -  private val readme = new HTML_Panel(Isabelle.system, "SansSerif", 14)
    18.8 -  readme.render_document(Isabelle.system.try_read(List(Path.explode("$JEDIT_HOME/README.html"))))
    18.9 +  private val readme = new HTML_Panel("SansSerif", 14)
   18.10 +  readme.render_document(Isabelle_System.try_read(List(Path.explode("$JEDIT_HOME/README.html"))))
   18.11  
   18.12    private val syslog = new TextArea(Isabelle.session.syslog())
   18.13    syslog.editable = false
    19.1 --- a/src/Tools/jEdit/src/token_markup.scala	Mon Jul 04 20:18:19 2011 +0200
    19.2 +++ b/src/Tools/jEdit/src/token_markup.scala	Mon Jul 04 22:11:32 2011 +0200
    19.3 @@ -79,8 +79,9 @@
    19.4    private def bold_style(style: SyntaxStyle): SyntaxStyle =
    19.5      font_style(style, _.deriveFont(Font.BOLD))
    19.6  
    19.7 -  class Style_Extender(symbols: Symbol.Interpretation) extends SyntaxUtilities.StyleExtender
    19.8 +  class Style_Extender extends SyntaxUtilities.StyleExtender
    19.9    {
   19.10 +    val symbols = Isabelle_System.symbols
   19.11      if (symbols.font_names.length > 2)
   19.12        error("Too many user symbol fonts (max 2 permitted): " + symbols.font_names.mkString(", "))
   19.13  
   19.14 @@ -105,9 +106,10 @@
   19.15      }
   19.16    }
   19.17  
   19.18 -  def extended_styles(symbols: Symbol.Interpretation, text: CharSequence)
   19.19 -    : Map[Text.Offset, Byte => Byte] =
   19.20 +  def extended_styles(text: CharSequence): Map[Text.Offset, Byte => Byte] =
   19.21    {
   19.22 +    val symbols = Isabelle_System.symbols
   19.23 +
   19.24      // FIXME symbols.bsub_decoded etc.
   19.25      def ctrl_style(sym: String): Option[Byte => Byte] =
   19.26        if (symbols.is_subscript_decoded(sym)) Some(subscript(_))
   19.27 @@ -163,7 +165,6 @@
   19.28      {
   19.29        val context1 =
   19.30          if (Isabelle.session.is_ready) {
   19.31 -          val symbols = Isabelle.system.symbols
   19.32            val syntax = Isabelle.session.current_syntax()
   19.33      
   19.34            val ctxt =
   19.35 @@ -174,7 +175,7 @@
   19.36            val (tokens, ctxt1) = syntax.scan_context(line, ctxt)
   19.37            val context1 = new Line_Context(ctxt1)
   19.38      
   19.39 -          val extended = extended_styles(symbols, line)
   19.40 +          val extended = extended_styles(line)
   19.41      
   19.42            var offset = 0
   19.43            for (token <- tokens) {