# HG changeset patch
# User wenzelm
# Date 1315424328 -7200
# Node ID 48a5c104d434746034a59ef33dc8caece696cc0a
# Parent  3d9ee91394ce06b0210ba6468ae2946fb11163dd
clarified terminology;

diff -r 3d9ee91394ce -r 48a5c104d434 src/Pure/System/session.scala
--- 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]
diff -r 3d9ee91394ce -r 48a5c104d434 src/Tools/jEdit/src/document_view.scala
--- 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() }
   }
diff -r 3d9ee91394ce -r 48a5c104d434 src/Tools/jEdit/src/output_dockable.scala
--- 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
   }