src/Pure/System/session.scala

       val (perspective, version) = Thy_Syntax.edit_perspective(previous, name, text_perspective)
 
       val text_edits: List[Document.Edit_Text] =
         List((name, Document.Node.Perspective(text_perspective)))
       val change =
-        global_state.change_yield(
-          _.continue_history(Future.value(previous), text_edits, Future.value(version)))
+        global_state >>>
+          (_.continue_history(Future.value(previous), text_edits, Future.value(version)))
 
       val assignment = global_state().the_assignment(previous).check_finished
-      global_state.change(_.define_version(version, assignment))
-      global_state.change_yield(_.assign(version.id))
+      global_state >> (_.define_version(version, assignment))
+      global_state >>> (_.assign(version.id))
 
       prover.get.update_perspective(previous.id, version.id, name, perspective)
     }
 
 

 
       prover.get.cancel_execution()
 
       val text_edits = header_edit(name, header) :: edits.map(edit => (name, edit))
       val version = Future.promise[Document.Version]
-      val change = global_state.change_yield(_.continue_history(previous, text_edits, version))
+      val change = global_state >>> (_.continue_history(previous, text_edits, version))
 
       change_parser ! Text_Edits(syntax, name, previous, text_edits, version)
     }
     //}}}
 

     /* exec state assignment */
 
     def handle_assign(id: Document.Version_ID, assign: Document.Assign)
     //{{{
     {
-      val cmds = global_state.change_yield(_.assign(id, assign))
+      val cmds = global_state >>> (_.assign(id, assign))
       for (cmd <- cmds) delay_commands_changed.invoke(cmd)
     }
     //}}}
 
 
     /* removed versions */
 
     def handle_removed(removed: List[Document.Version_ID])
     //{{{
     {
-      global_state.change(_.removed_versions(removed))
+      global_state >> (_.removed_versions(removed))
     }
     //}}}
 
 
     /* resulting changes */

       val doc_edits = change.doc_edits
 
       def id_command(command: Command)
       {
         if (!global_state().defined_command(command.id)) {
-          global_state.change(_.define_command(command))
+          global_state >> (_.define_command(command))
           prover.get.define_command(command)
         }
       }
       doc_edits foreach {
         case (_, edit) =>
           edit foreach { case (c1, c2) => c1 foreach id_command; c2 foreach id_command }
       }
 
       val assignment = global_state().the_assignment(previous).check_finished
-      global_state.change(_.define_version(version, assignment))
+      global_state >> (_.define_version(version, assignment))
       prover.get.update(previous.id, version.id, doc_edits)
     }
     //}}}
 
 

 
       result.properties match {
 
         case Position.Id(state_id) if !result.is_raw =>
           try {
-            val st = global_state.change_yield(_.accumulate(state_id, result.message))
+            val st = global_state >>> (_.accumulate(state_id, result.message))
             delay_commands_changed.invoke(st.command)
           }
           catch {
             case _: Document.State.Fail => bad_result(result)
           }

               catch { case _: Document.State.Fail => bad_result(result) }
             case _ => bad_result(result)
           }
           // FIXME separate timeout event/message!?
           if (prover.isDefined && System.currentTimeMillis() > prune_next) {
-            val old_versions = global_state.change_yield(_.prune_history(prune_size))
+            val old_versions = global_state >>> (_.prune_history(prune_size))
             if (!old_versions.isEmpty) prover.get.remove_versions(old_versions)
             prune_next = System.currentTimeMillis() + prune_delay.ms
           }
 
         case Isabelle_Markup.Removed_Versions if result.is_raw =>

             prover = Some(new Isabelle_Process(timeout, receiver.invoke _, args) with Protocol)
           }
 
         case Stop =>
           if (phase == Session.Ready) {
-            global_state.change(_ => Document.State.init)  // FIXME event bus!?
+            global_state >> (_ => Document.State.init)  // FIXME event bus!?
             phase = Session.Shutdown
             prover.get.terminate
             prover = None
             phase = Session.Inactive
           }