more uniform treatment of Swing_Thread context switch: prefer asynchronous Swing_Thread.later from actor;
--- a/src/Tools/jEdit/src/documentation_dockable.scala Sat Aug 24 12:31:24 2013 +0200
+++ b/src/Tools/jEdit/src/documentation_dockable.scala Sat Aug 24 13:32:51 2013 +0200
@@ -19,8 +19,6 @@
class Documentation_Dockable(view: View, position: String) extends Dockable(view, position)
{
- Swing_Thread.require()
-
private val docs = Doc.contents()
private case class Documentation(name: String, title: String)
--- a/src/Tools/jEdit/src/find_dockable.scala Sat Aug 24 12:31:24 2013 +0200
+++ b/src/Tools/jEdit/src/find_dockable.scala Sat Aug 24 13:32:51 2013 +0200
@@ -23,8 +23,6 @@
class Find_Dockable(view: View, position: String) extends Dockable(view, position)
{
- Swing_Thread.require()
-
val pretty_text_area = new Pretty_Text_Area(view)
set_content(pretty_text_area)
@@ -78,6 +76,7 @@
react {
case _: Session.Global_Options =>
Swing_Thread.later { handle_resize() }
+
case bad =>
java.lang.System.err.println("Find_Dockable: ignoring bad message " + bad)
}
@@ -86,8 +85,6 @@
override def init()
{
- Swing_Thread.require()
-
PIDE.session.global_options += main_actor
handle_resize()
find_theorems.activate()
@@ -95,8 +92,6 @@
override def exit()
{
- Swing_Thread.require()
-
find_theorems.deactivate()
PIDE.session.global_options -= main_actor
delay_resize.revoke()
--- a/src/Tools/jEdit/src/graphview_dockable.scala Sat Aug 24 12:31:24 2013 +0200
+++ b/src/Tools/jEdit/src/graphview_dockable.scala Sat Aug 24 13:32:51 2013 +0200
@@ -48,8 +48,6 @@
class Graphview_Dockable(view: View, position: String) extends Dockable(view, position)
{
- Swing_Thread.require()
-
private val snapshot = Graphview_Dockable.implicit_snapshot
private val graph = Graphview_Dockable.implicit_graph
@@ -82,13 +80,11 @@
override def init()
{
- Swing_Thread.require()
JEdit_Lib.parent_window(this).map(_.addWindowFocusListener(window_focus_listener))
}
override def exit()
{
- Swing_Thread.require()
JEdit_Lib.parent_window(this).map(_.removeWindowFocusListener(window_focus_listener))
}
}
--- a/src/Tools/jEdit/src/info_dockable.scala Sat Aug 24 12:31:24 2013 +0200
+++ b/src/Tools/jEdit/src/info_dockable.scala Sat Aug 24 13:32:51 2013 +0200
@@ -51,9 +51,6 @@
class Info_Dockable(view: View, position: String) extends Dockable(view, position)
{
- Swing_Thread.require()
-
-
/* component state -- owned by Swing thread */
private var zoom_factor = 100
@@ -108,6 +105,7 @@
react {
case _: Session.Global_Options =>
Swing_Thread.later { handle_resize() }
+
case bad => System.err.println("Info_Dockable: ignoring bad message " + bad)
}
}
@@ -115,8 +113,6 @@
override def init()
{
- Swing_Thread.require()
-
JEdit_Lib.parent_window(this).map(_.addWindowFocusListener(window_focus_listener))
PIDE.session.global_options += main_actor
handle_resize()
@@ -124,8 +120,6 @@
override def exit()
{
- Swing_Thread.require()
-
JEdit_Lib.parent_window(this).map(_.removeWindowFocusListener(window_focus_listener))
PIDE.session.global_options -= main_actor
delay_resize.revoke()
--- a/src/Tools/jEdit/src/monitor_dockable.scala Sat Aug 24 12:31:24 2013 +0200
+++ b/src/Tools/jEdit/src/monitor_dockable.scala Sat Aug 24 13:32:51 2013 +0200
@@ -45,6 +45,7 @@
rev_stats ::= props
delay_update.invoke()
}
+
case bad => java.lang.System.err.println("Monitor_Dockable: ignoring bad message " + bad)
}
}
--- a/src/Tools/jEdit/src/output_dockable.scala Sat Aug 24 12:31:24 2013 +0200
+++ b/src/Tools/jEdit/src/output_dockable.scala Sat Aug 24 13:32:51 2013 +0200
@@ -23,9 +23,6 @@
class Output_Dockable(view: View, position: String) extends Dockable(view, position)
{
- Swing_Thread.require()
-
-
/* component state -- owned by Swing thread */
private var zoom_factor = 100
@@ -91,11 +88,14 @@
react {
case _: Session.Global_Options =>
Swing_Thread.later { handle_resize() }
+
case changed: Session.Commands_Changed =>
val restriction = if (changed.assignment) None else Some(changed.commands)
Swing_Thread.later { handle_update(do_update, restriction) }
+
case Session.Caret_Focus =>
Swing_Thread.later { handle_update(do_update, None) }
+
case bad => System.err.println("Output_Dockable: ignoring bad message " + bad)
}
}
@@ -103,8 +103,6 @@
override def init()
{
- Swing_Thread.require()
-
PIDE.session.global_options += main_actor
PIDE.session.commands_changed += main_actor
PIDE.session.caret_focus += main_actor
@@ -113,8 +111,6 @@
override def exit()
{
- Swing_Thread.require()
-
PIDE.session.global_options -= main_actor
PIDE.session.commands_changed -= main_actor
PIDE.session.caret_focus -= main_actor
--- a/src/Tools/jEdit/src/readme_dockable.scala Sat Aug 24 12:31:24 2013 +0200
+++ b/src/Tools/jEdit/src/readme_dockable.scala Sat Aug 24 13:32:51 2013 +0200
@@ -14,8 +14,6 @@
class README_Dockable(view: View, position: String) extends Dockable(view, position)
{
- Swing_Thread.require()
-
private val readme = new HTML_Panel
private val readme_path = Path.explode("$JEDIT_HOME/README.html")
readme.render_document(Isabelle_System.platform_file_url(readme_path), File.read(readme_path))
--- a/src/Tools/jEdit/src/sledgehammer_dockable.scala Sat Aug 24 12:31:24 2013 +0200
+++ b/src/Tools/jEdit/src/sledgehammer_dockable.scala Sat Aug 24 13:32:51 2013 +0200
@@ -23,8 +23,6 @@
class Sledgehammer_Dockable(view: View, position: String) extends Dockable(view, position)
{
- Swing_Thread.require()
-
val pretty_text_area = new Pretty_Text_Area(view)
set_content(pretty_text_area)
@@ -98,9 +96,13 @@
case _: Session.Global_Options =>
Swing_Thread.later { handle_resize() }
query_provers()
- case Session.Ready => query_provers()
+
+ case Session.Ready =>
+ query_provers()
+
case Sledgehammer_Params.Provers =>
Swing_Thread.later { update_provers() }
+
case bad =>
java.lang.System.err.println("Sledgehammer_Dockable: ignoring bad message " + bad)
}
@@ -109,8 +111,6 @@
override def init()
{
- Swing_Thread.require()
-
PIDE.session.phase_changed += main_actor
PIDE.session.global_options += main_actor
Sledgehammer_Params.provers += main_actor
@@ -121,8 +121,6 @@
override def exit()
{
- Swing_Thread.require()
-
sledgehammer.deactivate()
PIDE.session.phase_changed -= main_actor
PIDE.session.global_options -= main_actor
--- a/src/Tools/jEdit/src/syslog_dockable.scala Sat Aug 24 12:31:24 2013 +0200
+++ b/src/Tools/jEdit/src/syslog_dockable.scala Sat Aug 24 13:32:51 2013 +0200
@@ -23,10 +23,10 @@
private def update_syslog()
{
- Swing_Thread.later {
- val text = PIDE.session.current_syslog()
- if (text != syslog.text) syslog.text = text
- }
+ Swing_Thread.require()
+
+ val text = PIDE.session.current_syslog()
+ if (text != syslog.text) syslog.text = text
}
set_content(syslog)
@@ -38,7 +38,7 @@
loop {
react {
case output: Isabelle_Process.Output =>
- if (output.is_syslog) update_syslog()
+ if (output.is_syslog) Swing_Thread.later { update_syslog() }
case bad => java.lang.System.err.println("Syslog_Dockable: ignoring bad message " + bad)
}
--- a/src/Tools/jEdit/src/theories_dockable.scala Sat Aug 24 12:31:24 2013 +0200
+++ b/src/Tools/jEdit/src/theories_dockable.scala Sat Aug 24 13:32:51 2013 +0200
@@ -69,7 +69,8 @@
private def handle_phase(phase: Session.Phase)
{
- Swing_Thread.later { session_phase.text = " " + phase_text(phase) + " " }
+ Swing_Thread.require()
+ session_phase.text = " " + phase_text(phase) + " "
}
private val continuous_checking = new CheckBox("Continuous checking") {
@@ -183,25 +184,25 @@
private def handle_update(restriction: Option[Set[Document.Node.Name]] = None)
{
- Swing_Thread.now {
- val snapshot = PIDE.session.snapshot()
+ Swing_Thread.require()
+
+ val snapshot = PIDE.session.snapshot()
- val iterator =
- restriction match {
- case Some(names) => names.iterator.map(name => (name, snapshot.version.nodes(name)))
- case None => snapshot.version.nodes.entries
- }
- val nodes_status1 =
- (nodes_status /: iterator)({ case (status, (name, node)) =>
- if (PIDE.thy_load.loaded_theories(name.theory)) status
- else status + (name -> Protocol.node_status(snapshot.state, snapshot.version, node)) })
+ val iterator =
+ restriction match {
+ case Some(names) => names.iterator.map(name => (name, snapshot.version.nodes(name)))
+ case None => snapshot.version.nodes.entries
+ }
+ val nodes_status1 =
+ (nodes_status /: iterator)({ case (status, (name, node)) =>
+ if (PIDE.thy_load.loaded_theories(name.theory)) status
+ else status + (name -> Protocol.node_status(snapshot.state, snapshot.version, node)) })
- if (nodes_status != nodes_status1) {
- nodes_status = nodes_status1
- status.listData =
- snapshot.version.nodes.topological_order.filter(
- (name: Document.Node.Name) => nodes_status.isDefinedAt(name))
- }
+ if (nodes_status != nodes_status1) {
+ nodes_status = nodes_status1
+ status.listData =
+ snapshot.version.nodes.topological_order.filter(
+ (name: Document.Node.Name) => nodes_status.isDefinedAt(name))
}
}
@@ -211,7 +212,8 @@
private val main_actor = actor {
loop {
react {
- case phase: Session.Phase => handle_phase(phase)
+ case phase: Session.Phase =>
+ Swing_Thread.later { handle_phase(phase) }
case _: Session.Global_Options =>
Swing_Thread.later {
@@ -221,7 +223,8 @@
status.repaint()
}
- case changed: Session.Commands_Changed => handle_update(Some(changed.nodes))
+ case changed: Session.Commands_Changed =>
+ Swing_Thread.later { handle_update(Some(changed.nodes)) }
case bad => System.err.println("Theories_Dockable: ignoring bad message " + bad)
}
@@ -230,9 +233,12 @@
override def init()
{
- PIDE.session.phase_changed += main_actor; handle_phase(PIDE.session.phase)
+ PIDE.session.phase_changed += main_actor
PIDE.session.global_options += main_actor
- PIDE.session.commands_changed += main_actor; handle_update()
+ PIDE.session.commands_changed += main_actor
+
+ handle_phase(PIDE.session.phase)
+ handle_update()
}
override def exit()
--- a/src/Tools/jEdit/src/timing_dockable.scala Sat Aug 24 12:31:24 2013 +0200
+++ b/src/Tools/jEdit/src/timing_dockable.scala Sat Aug 24 13:32:51 2013 +0200
@@ -175,28 +175,28 @@
private def handle_update(restriction: Option[Set[Document.Node.Name]] = None)
{
- Swing_Thread.now {
- val snapshot = PIDE.session.snapshot()
+ Swing_Thread.require()
+
+ val snapshot = PIDE.session.snapshot()
- val iterator =
- restriction match {
- case Some(names) => names.iterator.map(name => (name, snapshot.version.nodes(name)))
- case None => snapshot.version.nodes.entries
- }
- val nodes_timing1 =
- (nodes_timing /: iterator)({ case (timing1, (name, node)) =>
- if (PIDE.thy_load.loaded_theories(name.theory)) timing1
- else {
- val node_timing =
- Protocol.node_timing(snapshot.state, snapshot.version, node, timing_threshold)
- timing1 + (name -> node_timing)
- }
- })
- nodes_timing = nodes_timing1
+ val iterator =
+ restriction match {
+ case Some(names) => names.iterator.map(name => (name, snapshot.version.nodes(name)))
+ case None => snapshot.version.nodes.entries
+ }
+ val nodes_timing1 =
+ (nodes_timing /: iterator)({ case (timing1, (name, node)) =>
+ if (PIDE.thy_load.loaded_theories(name.theory)) timing1
+ else {
+ val node_timing =
+ Protocol.node_timing(snapshot.state, snapshot.version, node, timing_threshold)
+ timing1 + (name -> node_timing)
+ }
+ })
+ nodes_timing = nodes_timing1
- val entries = make_entries()
- if (timing_view.listData.toList != entries) timing_view.listData = entries
- }
+ val entries = make_entries()
+ if (timing_view.listData.toList != entries) timing_view.listData = entries
}
@@ -205,7 +205,8 @@
private val main_actor = actor {
loop {
react {
- case changed: Session.Commands_Changed => handle_update(Some(changed.nodes))
+ case changed: Session.Commands_Changed =>
+ Swing_Thread.later { handle_update(Some(changed.nodes)) }
case bad => System.err.println("Timing_Dockable: ignoring bad message " + bad)
}