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 -class Isabelle_System(this_isabelle_home: String) extends Standard_System
3.22 -{
3.23 - def this() = this(null)
3.24 + private case class State(
3.25 + standard_system: Standard_System,
3.26 + settings: Map[String, String],
3.27 + symbols: Symbol.Interpretation)
3.28
3.29 + @volatile private var _state: Option[State] = None
3.30
3.31 - /** Isabelle environment **/
3.32 + private def check_state(): State =
3.33 + {
3.34 + if (_state.isEmpty) init() // unsynchronized check
3.35 + _state.get
3.36 + }
3.37 +
3.38 + def standard_system: Standard_System = check_state().standard_system
3.39 + def settings: Map[String, String] = check_state().settings
3.40 + def symbols: Symbol.Interpretation = check_state().symbols
3.41
3.42 /*
3.43 isabelle_home precedence:
3.44 @@ -37,50 +47,67 @@
3.45 (2) ISABELLE_HOME process environment variable (e.g. inherited from running isabelle tool)
3.46 (3) isabelle.home system property (e.g. via JVM application boot process)
3.47 */
3.48 + def init(this_isabelle_home: String = null) = synchronized {
3.49 + if (_state.isEmpty) {
3.50 + import scala.collection.JavaConversions._
3.51
3.52 - private val environment: Map[String, String] =
3.53 - {
3.54 - import scala.collection.JavaConversions._
3.55 + val standard_system = new Standard_System
3.56
3.57 - val env0 = Map(System.getenv.toList: _*) +
3.58 - ("THIS_JAVA" -> this_java())
3.59 + val settings =
3.60 + {
3.61 + val env = Map(System.getenv.toList: _*) +
3.62 + ("THIS_JAVA" -> standard_system.this_java())
3.63
3.64 - val isabelle_home =
3.65 - if (this_isabelle_home != null) this_isabelle_home
3.66 - else
3.67 - env0.get("ISABELLE_HOME") match {
3.68 - case None | Some("") =>
3.69 - val path = System.getProperty("isabelle.home")
3.70 - if (path == null || path == "") error("Unknown Isabelle home directory")
3.71 - else path
3.72 - case Some(path) => path
3.73 - }
3.74 + val isabelle_home =
3.75 + if (this_isabelle_home != null) this_isabelle_home
3.76 + else
3.77 + env.get("ISABELLE_HOME") match {
3.78 + case None | Some("") =>
3.79 + val path = System.getProperty("isabelle.home")
3.80 + if (path == null || path == "") error("Unknown Isabelle home directory")
3.81 + else path
3.82 + case Some(path) => path
3.83 + }
3.84
3.85 - Standard_System.with_tmp_file("settings") { dump =>
3.86 - val shell_prefix =
3.87 - if (Platform.is_windows) List(platform_root + "\\bin\\bash", "-l") else Nil
3.88 - val cmdline =
3.89 - shell_prefix ::: List(isabelle_home + "/bin/isabelle", "getenv", "-d", dump.toString)
3.90 - val (output, rc) = Standard_System.raw_exec(null, env0, true, cmdline: _*)
3.91 - if (rc != 0) error(output)
3.92 + Standard_System.with_tmp_file("settings") { dump =>
3.93 + val shell_prefix =
3.94 + if (Platform.is_windows) List(standard_system.platform_root + "\\bin\\bash", "-l")
3.95 + else Nil
3.96 + val cmdline =
3.97 + shell_prefix ::: List(isabelle_home + "/bin/isabelle", "getenv", "-d", dump.toString)
3.98 + val (output, rc) = Standard_System.raw_exec(null, env, true, cmdline: _*)
3.99 + if (rc != 0) error(output)
3.100
3.101 - val entries =
3.102 - for (entry <- Source.fromFile(dump).mkString split "\0" if entry != "") yield {
3.103 - val i = entry.indexOf('=')
3.104 - if (i <= 0) (entry -> "")
3.105 - else (entry.substring(0, i) -> entry.substring(i + 1))
3.106 + val entries =
3.107 + for (entry <- Source.fromFile(dump).mkString split "\0" if entry != "") yield {
3.108 + val i = entry.indexOf('=')
3.109 + if (i <= 0) (entry -> "")
3.110 + else (entry.substring(0, i) -> entry.substring(i + 1))
3.111 + }
3.112 + Map(entries: _*) +
3.113 + ("HOME" -> System.getenv("HOME")) +
3.114 + ("PATH" -> System.getenv("PATH"))
3.115 + }
3.116 }
3.117 - Map(entries: _*) +
3.118 - ("HOME" -> System.getenv("HOME")) +
3.119 - ("PATH" -> System.getenv("PATH"))
3.120 +
3.121 + val symbols =
3.122 + {
3.123 + val isabelle_symbols = settings.getOrElse("ISABELLE_SYMBOLS", "")
3.124 + if (isabelle_symbols == "") error("Undefined environment variable: ISABELLE_SYMBOLS")
3.125 + val files =
3.126 + isabelle_symbols.split(":").toList.map(s => new File(standard_system.jvm_path(s)))
3.127 + new Symbol.Interpretation(Standard_System.try_read(files).split("\n").toList)
3.128 }
3.129 +
3.130 + _state = Some(State(standard_system, settings, symbols))
3.131 + }
3.132 }
3.133
3.134
3.135 /* getenv */
3.136
3.137 def getenv(name: String): String =
3.138 - environment.getOrElse(if (name == "HOME") "HOME_JVM" else name, "")
3.139 + settings.getOrElse(if (name == "HOME") "HOME_JVM" else name, "")
3.140
3.141 def getenv_strict(name: String): String =
3.142 {
3.143 @@ -88,9 +115,6 @@
3.144 if (value != "") value else error("Undefined environment variable: " + name)
3.145 }
3.146
3.147 - override def toString = getenv_strict("ISABELLE_HOME")
3.148 -
3.149 -
3.150
3.151 /** file-system operations **/
3.152
3.153 @@ -98,9 +122,11 @@
3.154
3.155 def standard_path(path: Path): String = path.expand(getenv_strict).implode
3.156
3.157 - def platform_path(path: Path): String = jvm_path(standard_path(path))
3.158 + def platform_path(path: Path): String = standard_system.jvm_path(standard_path(path))
3.159 def platform_file(path: Path) = new File(platform_path(path))
3.160
3.161 + def posix_path(jvm_path: String): String = standard_system.posix_path(jvm_path)
3.162 +
3.163
3.164 /* try_read */
3.165
3.166 @@ -142,9 +168,9 @@
3.167 def execute(redirect: Boolean, args: String*): Process =
3.168 {
3.169 val cmdline =
3.170 - if (Platform.is_windows) List(platform_root + "\\bin\\env.exe") ++ args
3.171 + if (Platform.is_windows) List(standard_system.platform_root + "\\bin\\env.exe") ++ args
3.172 else args
3.173 - Standard_System.raw_execute(null, environment, redirect, cmdline: _*)
3.174 + Standard_System.raw_execute(null, settings, redirect, cmdline: _*)
3.175 }
3.176
3.177
3.178 @@ -271,7 +297,7 @@
3.179 }
3.180
3.181 def rm_fifo(fifo: String): Boolean =
3.182 - (new File(jvm_path(if (Platform.is_windows) fifo + ".lnk" else fifo))).delete
3.183 + (new File(standard_system.jvm_path(if (Platform.is_windows) fifo + ".lnk" else fifo))).delete
3.184
3.185 def fifo_input_stream(fifo: String): InputStream =
3.186 {
3.187 @@ -328,13 +354,6 @@
3.188 }
3.189
3.190
3.191 - /* symbols */
3.192 -
3.193 - val symbols = new Symbol.Interpretation(
3.194 - try_read(getenv_strict("ISABELLE_SYMBOLS").split(":").toList.map(Path.explode))
3.195 - .split("\n").toList)
3.196 -
3.197 -
3.198 /* fonts */
3.199
3.200 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) {