--- a/src/Pure/System/session.scala Fri Sep 21 22:45:14 2012 +0200
+++ b/src/Pure/System/session.scala Sat Sep 22 14:03:01 2012 +0200
@@ -22,7 +22,7 @@
/* events */
//{{{
- case object Global_Settings
+ case object Global_Options
case object Caret_Focus
case class Raw_Edits(edits: List[Document.Edit_Text])
case class Commands_Changed(
@@ -57,7 +57,7 @@
/* pervasive event buses */
- val global_settings = new Event_Bus[Session.Global_Settings.type]
+ val global_options = new Event_Bus[Session.Global_Options.type]
val caret_focus = new Event_Bus[Session.Caret_Focus.type]
val raw_edits = new Event_Bus[Session.Raw_Edits]
val commands_changed = new Event_Bus[Session.Commands_Changed]
--- a/src/Tools/jEdit/src/output1_dockable.scala Fri Sep 21 22:45:14 2012 +0200
+++ b/src/Tools/jEdit/src/output1_dockable.scala Sat Sep 22 14:03:01 2012 +0200
@@ -116,7 +116,7 @@
private val main_actor = actor {
loop {
react {
- case Session.Global_Settings =>
+ case Session.Global_Options =>
Swing_Thread.later { handle_resize() }
case changed: Session.Commands_Changed =>
Swing_Thread.later { handle_update(do_update, Some(changed.commands)) }
@@ -131,7 +131,7 @@
{
Swing_Thread.require()
- Isabelle.session.global_settings += main_actor
+ Isabelle.session.global_options += main_actor
Isabelle.session.commands_changed += main_actor
Isabelle.session.caret_focus += main_actor
handle_update(true, None)
@@ -141,7 +141,7 @@
{
Swing_Thread.require()
- Isabelle.session.global_settings -= main_actor
+ Isabelle.session.global_options -= main_actor
Isabelle.session.commands_changed -= main_actor
Isabelle.session.caret_focus -= main_actor
delay_resize.revoke()
--- a/src/Tools/jEdit/src/output_dockable.scala Fri Sep 21 22:45:14 2012 +0200
+++ b/src/Tools/jEdit/src/output_dockable.scala Sat Sep 22 14:03:01 2012 +0200
@@ -90,7 +90,7 @@
private val main_actor = actor {
loop {
react {
- case Session.Global_Settings =>
+ case Session.Global_Options =>
Swing_Thread.later { handle_resize() }
case changed: Session.Commands_Changed =>
Swing_Thread.later { handle_update(do_update, Some(changed.commands)) }
@@ -105,7 +105,7 @@
{
Swing_Thread.require()
- Isabelle.session.global_settings += main_actor
+ Isabelle.session.global_options += main_actor
Isabelle.session.commands_changed += main_actor
Isabelle.session.caret_focus += main_actor
handle_update(true, None)
@@ -115,7 +115,7 @@
{
Swing_Thread.require()
- Isabelle.session.global_settings -= main_actor
+ Isabelle.session.global_options -= main_actor
Isabelle.session.commands_changed -= main_actor
Isabelle.session.caret_focus -= main_actor
delay_resize.revoke()
--- a/src/Tools/jEdit/src/plugin.scala Fri Sep 21 22:45:14 2012 +0200
+++ b/src/Tools/jEdit/src/plugin.scala Sat Sep 22 14:03:01 2012 +0200
@@ -318,7 +318,7 @@
case msg: PropertiesChanged =>
Isabelle.setup_tooltips()
- Isabelle.session.global_settings.event(Session.Global_Settings)
+ Isabelle.session.global_options.event(Session.Global_Options)
case _ =>
}
--- a/src/Tools/jEdit/src/session_dockable.scala Fri Sep 21 22:45:14 2012 +0200
+++ b/src/Tools/jEdit/src/session_dockable.scala Sat Sep 22 14:03:01 2012 +0200
@@ -150,7 +150,7 @@
react {
case phase: Session.Phase => handle_phase(phase)
- case Session.Global_Settings => Swing_Thread.later { logic.load () }
+ case Session.Global_Options => Swing_Thread.later { logic.load () }
case changed: Session.Commands_Changed => handle_update(Some(changed.nodes))
@@ -162,14 +162,14 @@
override def init()
{
Isabelle.session.phase_changed += main_actor; handle_phase(Isabelle.session.phase)
- Isabelle.session.global_settings += main_actor
+ Isabelle.session.global_options += main_actor
Isabelle.session.commands_changed += main_actor; handle_update()
}
override def exit()
{
Isabelle.session.phase_changed -= main_actor
- Isabelle.session.global_settings -= main_actor
+ Isabelle.session.global_options -= main_actor
Isabelle.session.commands_changed -= main_actor
}
}