--- a/src/Pure/System/session.scala Wed Sep 07 21:31:50 2011 +0200
+++ b/src/Pure/System/session.scala Wed Sep 07 21:38:48 2011 +0200
@@ -22,7 +22,7 @@
//{{{
case object Global_Settings
- case object Perspective
+ case object Caret_Focus
case object Assignment
case class Commands_Changed(nodes: Set[Document.Node.Name], commands: Set[Command])
@@ -52,7 +52,7 @@
/* pervasive event buses */
val global_settings = new Event_Bus[Session.Global_Settings.type]
- val perspective = new Event_Bus[Session.Perspective.type]
+ val caret_focus = new Event_Bus[Session.Caret_Focus.type]
val assignments = new Event_Bus[Session.Assignment.type]
val commands_changed = new Event_Bus[Session.Commands_Changed]
val phase_changed = new Event_Bus[Session.Phase]
--- a/src/Tools/jEdit/src/document_view.scala Wed Sep 07 21:31:50 2011 +0200
+++ b/src/Tools/jEdit/src/document_view.scala Wed Sep 07 21:38:48 2011 +0200
@@ -362,7 +362,7 @@
private val caret_listener = new CaretListener {
private val delay = Swing_Thread.delay_last(session.input_delay) {
- session.perspective.event(Session.Perspective)
+ session.caret_focus.event(Session.Caret_Focus)
}
override def caretUpdate(e: CaretEvent) { delay() }
}
--- a/src/Tools/jEdit/src/output_dockable.scala Wed Sep 07 21:31:50 2011 +0200
+++ b/src/Tools/jEdit/src/output_dockable.scala Wed Sep 07 21:38:48 2011 +0200
@@ -106,7 +106,7 @@
react {
case Session.Global_Settings => handle_resize()
case changed: Session.Commands_Changed => handle_update(Some(changed.commands))
- case Session.Perspective => if (follow_caret && handle_perspective()) handle_update()
+ case Session.Caret_Focus => if (follow_caret && handle_perspective()) handle_update()
case bad => System.err.println("Output_Dockable: ignoring bad message " + bad)
}
}
@@ -116,14 +116,14 @@
{
Isabelle.session.global_settings += main_actor
Isabelle.session.commands_changed += main_actor
- Isabelle.session.perspective += main_actor
+ Isabelle.session.caret_focus += main_actor
}
override def exit()
{
Isabelle.session.global_settings -= main_actor
Isabelle.session.commands_changed -= main_actor
- Isabelle.session.perspective -= main_actor
+ Isabelle.session.caret_focus -= main_actor
}