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]