clarified terminology;
authorwenzelm
Wed Sep 07 21:38:48 2011 +0200 (2011-09-07)
changeset 4480548a5c104d434
parent 44804 3d9ee91394ce
child 44806 3950842bb628
clarified terminology;
src/Pure/System/session.scala
src/Tools/jEdit/src/document_view.scala
src/Tools/jEdit/src/output_dockable.scala
     1.1 --- a/src/Pure/System/session.scala	Wed Sep 07 21:31:50 2011 +0200
     1.2 +++ b/src/Pure/System/session.scala	Wed Sep 07 21:38:48 2011 +0200
     1.3 @@ -22,7 +22,7 @@
     1.4  
     1.5    //{{{
     1.6    case object Global_Settings
     1.7 -  case object Perspective
     1.8 +  case object Caret_Focus
     1.9    case object Assignment
    1.10    case class Commands_Changed(nodes: Set[Document.Node.Name], commands: Set[Command])
    1.11  
    1.12 @@ -52,7 +52,7 @@
    1.13    /* pervasive event buses */
    1.14  
    1.15    val global_settings = new Event_Bus[Session.Global_Settings.type]
    1.16 -  val perspective = new Event_Bus[Session.Perspective.type]
    1.17 +  val caret_focus = new Event_Bus[Session.Caret_Focus.type]
    1.18    val assignments = new Event_Bus[Session.Assignment.type]
    1.19    val commands_changed = new Event_Bus[Session.Commands_Changed]
    1.20    val phase_changed = new Event_Bus[Session.Phase]
     2.1 --- a/src/Tools/jEdit/src/document_view.scala	Wed Sep 07 21:31:50 2011 +0200
     2.2 +++ b/src/Tools/jEdit/src/document_view.scala	Wed Sep 07 21:38:48 2011 +0200
     2.3 @@ -362,7 +362,7 @@
     2.4  
     2.5    private val caret_listener = new CaretListener {
     2.6      private val delay = Swing_Thread.delay_last(session.input_delay) {
     2.7 -      session.perspective.event(Session.Perspective)
     2.8 +      session.caret_focus.event(Session.Caret_Focus)
     2.9      }
    2.10      override def caretUpdate(e: CaretEvent) { delay() }
    2.11    }
     3.1 --- a/src/Tools/jEdit/src/output_dockable.scala	Wed Sep 07 21:31:50 2011 +0200
     3.2 +++ b/src/Tools/jEdit/src/output_dockable.scala	Wed Sep 07 21:38:48 2011 +0200
     3.3 @@ -106,7 +106,7 @@
     3.4        react {
     3.5          case Session.Global_Settings => handle_resize()
     3.6          case changed: Session.Commands_Changed => handle_update(Some(changed.commands))
     3.7 -        case Session.Perspective => if (follow_caret && handle_perspective()) handle_update()
     3.8 +        case Session.Caret_Focus => if (follow_caret && handle_perspective()) handle_update()
     3.9          case bad => System.err.println("Output_Dockable: ignoring bad message " + bad)
    3.10        }
    3.11      }
    3.12 @@ -116,14 +116,14 @@
    3.13    {
    3.14      Isabelle.session.global_settings += main_actor
    3.15      Isabelle.session.commands_changed += main_actor
    3.16 -    Isabelle.session.perspective += main_actor
    3.17 +    Isabelle.session.caret_focus += main_actor
    3.18    }
    3.19  
    3.20    override def exit()
    3.21    {
    3.22      Isabelle.session.global_settings -= main_actor
    3.23      Isabelle.session.commands_changed -= main_actor
    3.24 -    Isabelle.session.perspective -= main_actor
    3.25 +    Isabelle.session.caret_focus -= main_actor
    3.26    }
    3.27  
    3.28