--- 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)
--- 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))
//}}}
}
--- 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 **/
+
+ private case class State(
+ standard_system: Standard_System,
+ settings: Map[String, String],
+ symbols: Symbol.Interpretation)
+
+ @volatile private var _state: Option[State] = None
-class Isabelle_System(this_isabelle_home: String) extends Standard_System
-{
- def this() = this(null)
+ private def check_state(): State =
+ {
+ if (_state.isEmpty) init() // unsynchronized check
+ _state.get
+ }
-
- /** Isabelle environment **/
+ 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 =
--- 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 =>
--- 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
}
}
--- 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 =
--- 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) =>
--- 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))
}
}
--- 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
--- 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()
--- 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(
--- 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()
}
--- 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) =>
--- 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(
--- 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" =>
--- 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
--- 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)
--- 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
--- 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) {