--- a/src/Tools/jEdit/src/jedit/OptionPane.scala Sat Jun 27 00:19:11 2009 +0200
+++ b/src/Tools/jEdit/src/jedit/OptionPane.scala Tue Jun 30 21:22:50 2009 +0200
@@ -41,7 +41,7 @@
if (Isabelle.Int_Property("font-size") != size)
{
Isabelle.Int_Property("font-size") = size
- Swing.later { Isabelle.plugin.set_font(size) }
+ Swing_Thread.later { Isabelle.plugin.set_font(size) }
}
}
}
--- a/src/Tools/jEdit/src/jedit/TheoryView.scala Sat Jun 27 00:19:11 2009 +0200
+++ b/src/Tools/jEdit/src/jedit/TheoryView.scala Tue Jun 30 21:22:50 2009 +0200
@@ -101,7 +101,7 @@
loop {
react {
case _ => { // FIXME potentially blocking within loop/react!?!?!?!
- Swing.now {
+ Swing_Thread.now {
repaint_delay.delay_or_ignore()
phase_overview.repaint_delay.delay_or_ignore()
}
--- a/src/Tools/jEdit/src/prover/Prover.scala Sat Jun 27 00:19:11 2009 +0200
+++ b/src/Tools/jEdit/src/prover/Prover.scala Tue Jun 30 21:22:50 2009 +0200
@@ -138,7 +138,7 @@
case XML.Elem(Markup.READY, _, _)
if !initialized =>
initialized = true
- Swing.now { this ! ProverEvents.Activate }
+ Swing_Thread.now { this ! ProverEvents.Activate }
// document edits
case XML.Elem(Markup.EDITS, (Markup.ID, doc_id) :: _, edits)
@@ -262,20 +262,20 @@
process.begin_document(document_id0, path)
}
- private def edit_document(old_id: String, document_id: String, changes: StructureChange) = Swing.now
- {
- val removes =
- for (cmd <- changes.removed_commands) yield {
- commands -= cmd.id
- if (cmd.state_id != null) states -= cmd.state_id
- changes.before_change.map(_.id).getOrElse(document_id0) -> None
- }
- val inserts =
- for (cmd <- changes.added_commands) yield {
- commands += (cmd.id -> cmd)
- process.define_command(cmd.id, isabelle_system.symbols.encode(cmd.content))
- (document.commands.prev(cmd).map(_.id).getOrElse(document_id0)) -> Some(cmd.id)
- }
- process.edit_document(old_id, document_id, removes.reverse ++ inserts)
- }
+ private def edit_document(old_id: String, document_id: String, changes: StructureChange) =
+ Swing_Thread.now {
+ val removes =
+ for (cmd <- changes.removed_commands) yield {
+ commands -= cmd.id
+ if (cmd.state_id != null) states -= cmd.state_id
+ changes.before_change.map(_.id).getOrElse(document_id0) -> None
+ }
+ val inserts =
+ for (cmd <- changes.added_commands) yield {
+ commands += (cmd.id -> cmd)
+ process.define_command(cmd.id, isabelle_system.symbols.encode(cmd.content))
+ (document.commands.prev(cmd).map(_.id).getOrElse(document_id0)) -> Some(cmd.id)
+ }
+ process.edit_document(old_id, document_id, removes.reverse ++ inserts)
+ }
}