# HG changeset patch
# User huffman
# Date 1308775532 25200
# Node ID 8f28a91ea135f0f7581450094b4c565251d6dfd0
# Parent d75e285fcf3e021f7ea767120cef13d4e0e7e0e2# Parent 55160cf1e4f658bad962492af4c2932fa98961ce
merged
diff -r d75e285fcf3e -r 8f28a91ea135 etc/settings
--- a/etc/settings Wed Jun 22 13:30:28 2011 -0700
+++ b/etc/settings Wed Jun 22 13:45:32 2011 -0700
@@ -15,7 +15,7 @@
# not invent new ML system names unless you know what you are doing.
# Only one of the sections below should be activated.
-# Poly/ML 5.x (automated settings)
+# Poly/ML 32 bit (automated settings)
ML_PLATFORM="$ISABELLE_PLATFORM"
ML_HOME="$(choosefrom \
"$ISABELLE_HOME/contrib/polyml/$ML_PLATFORM" \
@@ -28,17 +28,17 @@
ML_OPTIONS="-H 200"
ML_SOURCES="$ML_HOME/../src"
-# Poly/ML 5.4.0
-#ML_PLATFORM=x86-linux
-#ML_HOME=/usr/local/polyml/x86-linux
+# Poly/ML 32 bit (manual settings)
#ML_SYSTEM=polyml-5.4.0
+#ML_PLATFORM="$ISABELLE_PLATFORM"
+#ML_HOME="$ISABELLE_HOME/contrib/$ML_SYSTEM/$ML_PLATFORM"
#ML_OPTIONS="-H 500"
#ML_SOURCES="$ML_HOME/../src"
-# Poly/ML 5.4.0 (64 bit)
-#ML_PLATFORM=x86_64-linux
-#ML_HOME=/usr/local/polyml/x86_64-linux
+# Poly/ML 64 bit (manual settings)
#ML_SYSTEM=polyml-5.4.0
+#ML_PLATFORM="${ISABELLE_PLATFORM64:-$ISABELLE_PLATFORM}"
+#ML_HOME="$ISABELLE_HOME/contrib/$ML_SYSTEM/$ML_PLATFORM"
#ML_OPTIONS="-H 1000"
#ML_SOURCES="$ML_HOME/../src"
diff -r d75e285fcf3e -r 8f28a91ea135 src/Pure/General/symbol.scala
--- a/src/Pure/General/symbol.scala Wed Jun 22 13:30:28 2011 -0700
+++ b/src/Pure/General/symbol.scala Wed Jun 22 13:45:32 2011 -0700
@@ -374,10 +374,13 @@
private val subscript_decoded = Set(decode("\\<^sub>"), decode("\\<^isub>"))
private val superscript_decoded = Set(decode("\\<^sup>"), decode("\\<^isup>"))
- val bold_decoded = decode("\\<^bold>")
-
def is_subscript_decoded(sym: String): Boolean = subscript_decoded.contains(sym)
def is_superscript_decoded(sym: String): Boolean = superscript_decoded.contains(sym)
- def is_bold_decoded(sym: String): Boolean = sym == bold_decoded
+
+ val bold_decoded = decode("\\<^bold>")
+ val bsub_decoded = decode("\\<^bsub>")
+ val esub_decoded = decode("\\<^esub>")
+ val bsup_decoded = decode("\\<^bsup>")
+ val esup_decoded = decode("\\<^esup>")
}
}
diff -r d75e285fcf3e -r 8f28a91ea135 src/Pure/System/gui_setup.scala
--- a/src/Pure/System/gui_setup.scala Wed Jun 22 13:30:28 2011 -0700
+++ b/src/Pure/System/gui_setup.scala Wed Jun 22 13:45:32 2011 -0700
@@ -42,7 +42,7 @@
text.append("JVM name: " + Platform.jvm_name + "\n")
text.append("JVM platform: " + Platform.jvm_platform + "\n")
try {
- val isabelle_system = new Isabelle_System
+ 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")
diff -r d75e285fcf3e -r 8f28a91ea135 src/Pure/System/isabelle_process.scala
--- a/src/Pure/System/isabelle_process.scala Wed Jun 22 13:30:28 2011 -0700
+++ b/src/Pure/System/isabelle_process.scala Wed Jun 22 13:45:32 2011 -0700
@@ -69,7 +69,7 @@
/* demo constructor */
def this(args: String*) =
- this(new Isabelle_System, Time.seconds(10),
+ this(Isabelle_System.default, Time.seconds(10),
actor { loop { react { case res => Console.println(res) } } }, args: _*)
diff -r d75e285fcf3e -r 8f28a91ea135 src/Pure/System/isabelle_system.scala
--- a/src/Pure/System/isabelle_system.scala Wed Jun 22 13:30:28 2011 -0700
+++ b/src/Pure/System/isabelle_system.scala Wed Jun 22 13:45:32 2011 -0700
@@ -18,6 +18,11 @@
import scala.collection.mutable
+object Isabelle_System
+{
+ lazy val default: Isabelle_System = new Isabelle_System
+}
+
class Isabelle_System(this_isabelle_home: String) extends Standard_System
{
def this() = this(null)
diff -r d75e285fcf3e -r 8f28a91ea135 src/Pure/Thy/html.scala
--- a/src/Pure/Thy/html.scala Wed Jun 22 13:30:28 2011 -0700
+++ b/src/Pure/Thy/html.scala Wed Jun 22 13:45:32 2011 -0700
@@ -82,13 +82,13 @@
val s1 = syms.next
def s2() = if (syms.hasNext) syms.next else ""
if (s1 == "\n") add(XML.elem(BR))
- else if (s1 == "\\<^bsub>") t ++= s1 // FIXME
- else if (s1 == "\\<^esub>") t ++= s1 // FIXME
- else if (s1 == "\\<^bsup>") t ++= s1 // FIXME
- else if (s1 == "\\<^esup>") t ++= s1 // FIXME
+ else if (s1 == symbols.bsub_decoded) t ++= s1 // FIXME
+ else if (s1 == symbols.esub_decoded) t ++= s1 // FIXME
+ else if (s1 == symbols.bsup_decoded) t ++= s1 // FIXME
+ else if (s1 == symbols.esup_decoded) t ++= s1 // FIXME
else if (symbols.is_subscript_decoded(s1)) { add(hidden(s1)); add(sub(s2())) }
else if (symbols.is_superscript_decoded(s1)) { add(hidden(s1)); add(sup(s2())) }
- else if (symbols.is_bold_decoded(s1)) { add(hidden(s1)); add(bold(s2())) }
+ else if (s1 == symbols.bold_decoded) { add(hidden(s1)); add(bold(s2())) }
else if (symbols.fonts.isDefinedAt(s1)) { add(user_font(symbols.fonts(s1), s1)) }
else t ++= s1
}
diff -r d75e285fcf3e -r 8f28a91ea135 src/Tools/jEdit/README.html
--- a/src/Tools/jEdit/README.html Wed Jun 22 13:30:28 2011 -0700
+++ b/src/Tools/jEdit/README.html Wed Jun 22 13:45:32 2011 -0700
@@ -5,7 +5,7 @@
Notes on the Isabelle/jEdit Prover IDE
diff -r d75e285fcf3e -r 8f28a91ea135 src/Tools/jEdit/src/document_model.scala
--- a/src/Tools/jEdit/src/document_model.scala Wed Jun 22 13:30:28 2011 -0700
+++ b/src/Tools/jEdit/src/document_model.scala Wed Jun 22 13:45:32 2011 -0700
@@ -131,16 +131,17 @@
/* activation */
- def activate()
+ private def activate()
{
buffer.addBufferListener(buffer_listener)
+ pending_edits.init()
buffer.propertiesChanged()
- pending_edits.init()
}
- def deactivate()
+ private def deactivate()
{
pending_edits.flush()
buffer.removeBufferListener(buffer_listener)
+ buffer.propertiesChanged()
}
}
diff -r d75e285fcf3e -r 8f28a91ea135 src/Tools/jEdit/src/document_view.scala
--- a/src/Tools/jEdit/src/document_view.scala Wed Jun 22 13:30:28 2011 -0700
+++ b/src/Tools/jEdit/src/document_view.scala Wed Jun 22 13:45:32 2011 -0700
@@ -77,7 +77,7 @@
Swing_Thread.require()
if (model.buffer == text_area.getBuffer) body
else {
- // FIXME Log.log(Log.ERROR, this, new RuntimeException("Inconsistent document model"))
+ Log.log(Log.ERROR, this, new RuntimeException("Inconsistent document model"))
default
}
}
diff -r d75e285fcf3e -r 8f28a91ea135 src/Tools/jEdit/src/plugin.scala
--- a/src/Tools/jEdit/src/plugin.scala Wed Jun 22 13:30:28 2011 -0700
+++ b/src/Tools/jEdit/src/plugin.scala Wed Jun 22 13:45:32 2011 -0700
@@ -191,6 +191,54 @@
def document_model(buffer: Buffer): Option[Document_Model] = Document_Model(buffer)
def document_view(text_area: JEditTextArea): Option[Document_View] = Document_View(text_area)
+ def init_model(buffer: Buffer)
+ {
+ swing_buffer_lock(buffer) {
+ val opt_model =
+ document_model(buffer) match {
+ case Some(model) => Some(model)
+ case None =>
+ // FIXME strip protocol prefix of URL
+ Thy_Header.split_thy_path(system.posix_path(buffer.getPath)) match {
+ case Some((dir, thy_name)) =>
+ Some(Document_Model.init(session, buffer, dir + "/" + thy_name))
+ case None => None
+ }
+ }
+ if (opt_model.isDefined) {
+ for (text_area <- jedit_text_areas(buffer)) {
+ if (document_view(text_area).map(_.model) != opt_model)
+ Document_View.init(opt_model.get, text_area)
+ }
+ }
+ }
+ }
+
+ def exit_model(buffer: Buffer)
+ {
+ swing_buffer_lock(buffer) {
+ jedit_text_areas(buffer).foreach(Document_View.exit)
+ Document_Model.exit(buffer)
+ }
+ }
+
+ def init_view(buffer: Buffer, text_area: JEditTextArea)
+ {
+ swing_buffer_lock(buffer) {
+ document_model(buffer) match {
+ case Some(model) => Document_View.init(model, text_area)
+ case None =>
+ }
+ }
+ }
+
+ def exit_view(buffer: Buffer, text_area: JEditTextArea)
+ {
+ swing_buffer_lock(buffer) {
+ Document_View.exit(text_area)
+ }
+ }
+
/* dockable windows */
@@ -267,47 +315,13 @@
{
/* session management */
- private def init_model(buffer: Buffer)
- {
- Isabelle.swing_buffer_lock(buffer) {
- val opt_model =
- Document_Model(buffer) match {
- case Some(model) => Some(model)
- case None =>
- Thy_Header.split_thy_path(Isabelle.system.posix_path(buffer.getPath)) match {
- case Some((dir, thy_name)) =>
- Some(Document_Model.init(Isabelle.session, buffer, dir + "/" + thy_name))
- case None => None
- }
- }
- if (opt_model.isDefined) {
- for (text_area <- Isabelle.jedit_text_areas(buffer)) {
- if (Document_View(text_area).map(_.model) != opt_model)
- Document_View.init(opt_model.get, text_area)
- }
- }
- }
- }
-
- private def exit_model(buffer: Buffer)
- {
- Isabelle.swing_buffer_lock(buffer) {
- Isabelle.jedit_text_areas(buffer).foreach(Document_View.exit)
- Document_Model.exit(buffer)
- }
- }
-
- private case class Init_Model(buffer: Buffer)
- private case class Exit_Model(buffer: Buffer)
- private case class Init_View(buffer: Buffer, text_area: JEditTextArea)
- private case class Exit_View(buffer: Buffer, text_area: JEditTextArea)
+ @volatile private var session_ready = false
private val session_manager = actor {
- var ready = false
loop {
react {
case phase: Session.Phase =>
- ready = phase == Session.Ready
+ session_ready = phase == Session.Ready
phase match {
case Session.Failed =>
Swing_Thread.now {
@@ -316,32 +330,11 @@
Library.error_dialog(jEdit.getActiveView, "Failed to start Isabelle process", text)
}
- case Session.Ready => Isabelle.jedit_buffers.foreach(init_model)
- case Session.Shutdown => Isabelle.jedit_buffers.foreach(exit_model)
+ case Session.Ready => Isabelle.jedit_buffers.foreach(Isabelle.init_model)
+ case Session.Shutdown => Isabelle.jedit_buffers.foreach(Isabelle.exit_model)
case _ =>
}
- case Init_Model(buffer) =>
- if (ready) init_model(buffer)
-
- case Exit_Model(buffer) =>
- exit_model(buffer)
-
- case Init_View(buffer, text_area) =>
- if (ready) {
- Isabelle.swing_buffer_lock(buffer) {
- Document_Model(buffer) match {
- case Some(model) => Document_View.init(model, text_area)
- case None =>
- }
- }
- }
-
- case Exit_View(buffer, text_area) =>
- Isabelle.swing_buffer_lock(buffer) {
- Document_View.exit(text_area)
- }
-
case bad => System.err.println("session_manager: ignoring bad message " + bad)
}
}
@@ -352,16 +345,19 @@
override def handleMessage(message: EBMessage)
{
+ Swing_Thread.assert()
message match {
case msg: EditorStarted =>
- Isabelle.check_jvm()
- if (Isabelle.Boolean_Property("auto-start")) Isabelle.start_session()
+ Isabelle.check_jvm()
+ if (Isabelle.Boolean_Property("auto-start"))
+ Isabelle.start_session()
case msg: BufferUpdate
if msg.getWhat == BufferUpdate.PROPERTIES_CHANGED =>
val buffer = msg.getBuffer
- if (buffer != null) session_manager ! Init_Model(buffer)
+ if (buffer != null && session_ready)
+ Isabelle.init_model(buffer)
case msg: EditPaneUpdate
if (msg.getWhat == EditPaneUpdate.BUFFER_CHANGING ||
@@ -375,10 +371,11 @@
if (buffer != null && text_area != null) {
if (msg.getWhat == EditPaneUpdate.BUFFER_CHANGED ||
- msg.getWhat == EditPaneUpdate.CREATED)
- session_manager ! Init_View(buffer, text_area)
- else
- session_manager ! Exit_View(buffer, text_area)
+ msg.getWhat == EditPaneUpdate.CREATED) {
+ if (session_ready)
+ Isabelle.init_view(buffer, text_area)
+ }
+ else Isabelle.exit_view(buffer, text_area)
}
case msg: PropertiesChanged =>
@@ -397,13 +394,15 @@
Isabelle.system.install_fonts()
Isabelle.session = new Session(Isabelle.system)
SyntaxUtilities.setStyleExtender(new Token_Markup.Style_Extender(Isabelle.system.symbols))
- ModeProvider.instance = new Token_Markup.Mode_Provider(ModeProvider.instance)
+ if (ModeProvider.instance.isInstanceOf[ModeProvider])
+ ModeProvider.instance = new Token_Markup.Mode_Provider(ModeProvider.instance)
Isabelle.session.phase_changed += session_manager
}
override def stop()
{
+ Isabelle.session.phase_changed -= session_manager
+ Isabelle.jedit_buffers.foreach(Isabelle.exit_model)
Isabelle.session.stop()
- Isabelle.session.phase_changed -= session_manager
}
}
diff -r d75e285fcf3e -r 8f28a91ea135 src/Tools/jEdit/src/token_markup.scala
--- a/src/Tools/jEdit/src/token_markup.scala Wed Jun 22 13:30:28 2011 -0700
+++ b/src/Tools/jEdit/src/token_markup.scala Wed Jun 22 13:45:32 2011 -0700
@@ -108,11 +108,11 @@
def extended_styles(symbols: Symbol.Interpretation, text: CharSequence)
: Map[Text.Offset, Byte => Byte] =
{
- // FIXME \\<^bsub> \\<^esub> \\<^bsup> \\<^esup>
+ // FIXME symbols.bsub_decoded etc.
def ctrl_style(sym: String): Option[Byte => Byte] =
if (symbols.is_subscript_decoded(sym)) Some(subscript(_))
else if (symbols.is_superscript_decoded(sym)) Some(superscript(_))
- else if (symbols.is_bold_decoded(sym)) Some(bold(_))
+ else if (sym == symbols.bold_decoded) Some(bold(_))
else None
var result = Map[Text.Offset, Byte => Byte]()