# 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
   }
 }