--- 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]