# HG changeset patch # User wenzelm # Date 1348315381 -7200 # Node ID dc06703640082ec753a5be88cdf68e2aa43fe0d7 # Parent 355f3d076924a8e3cfe0e4a520c1983763ce2759 tuned signature; diff -r 355f3d076924 -r dc0670364008 src/Pure/System/session.scala --- 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] diff -r 355f3d076924 -r dc0670364008 src/Tools/jEdit/src/output1_dockable.scala --- 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() diff -r 355f3d076924 -r dc0670364008 src/Tools/jEdit/src/output_dockable.scala --- 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() diff -r 355f3d076924 -r dc0670364008 src/Tools/jEdit/src/plugin.scala --- 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 _ => } diff -r 355f3d076924 -r dc0670364008 src/Tools/jEdit/src/session_dockable.scala --- 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 } }