tuned signature (in accordance with ML);
authorwenzelm
Sun, 26 Feb 2012 19:36:35 +0100
changeset 475597e47ae85e161
parent 47558 b2ae19322ff8
child 47560 134982ee4ecb
tuned signature (in accordance with ML);
src/Pure/Concurrent/volatile.scala
src/Pure/System/session.scala
     1.1 --- a/src/Pure/Concurrent/volatile.scala	Sun Feb 26 19:20:46 2012 +0100
     1.2 +++ b/src/Pure/Concurrent/volatile.scala	Sun Feb 26 19:36:35 2012 +0100
     1.3 @@ -18,8 +18,8 @@
     1.4  {
     1.5    @volatile private var state: A = init
     1.6    def apply(): A = state
     1.7 -  def change(f: A => A) { state = f(state) }
     1.8 -  def change_yield[B](f: A => (B, A)): B =
     1.9 +  def >> (f: A => A) { state = f(state) }
    1.10 +  def >>>[B] (f: A => (B, A)): B =
    1.11    {
    1.12      val (result, new_state) = f(state)
    1.13      state = new_state
     2.1 --- a/src/Pure/System/session.scala	Sun Feb 26 19:20:46 2012 +0100
     2.2 +++ b/src/Pure/System/session.scala	Sun Feb 26 19:36:35 2012 +0100
     2.3 @@ -262,12 +262,12 @@
     2.4        val text_edits: List[Document.Edit_Text] =
     2.5          List((name, Document.Node.Perspective(text_perspective)))
     2.6        val change =
     2.7 -        global_state.change_yield(
     2.8 -          _.continue_history(Future.value(previous), text_edits, Future.value(version)))
     2.9 +        global_state >>>
    2.10 +          (_.continue_history(Future.value(previous), text_edits, Future.value(version)))
    2.11  
    2.12        val assignment = global_state().the_assignment(previous).check_finished
    2.13 -      global_state.change(_.define_version(version, assignment))
    2.14 -      global_state.change_yield(_.assign(version.id))
    2.15 +      global_state >> (_.define_version(version, assignment))
    2.16 +      global_state >>> (_.assign(version.id))
    2.17  
    2.18        prover.get.update_perspective(previous.id, version.id, name, perspective)
    2.19      }
    2.20 @@ -286,7 +286,7 @@
    2.21  
    2.22        val text_edits = header_edit(name, header) :: edits.map(edit => (name, edit))
    2.23        val version = Future.promise[Document.Version]
    2.24 -      val change = global_state.change_yield(_.continue_history(previous, text_edits, version))
    2.25 +      val change = global_state >>> (_.continue_history(previous, text_edits, version))
    2.26  
    2.27        change_parser ! Text_Edits(syntax, name, previous, text_edits, version)
    2.28      }
    2.29 @@ -298,7 +298,7 @@
    2.30      def handle_assign(id: Document.Version_ID, assign: Document.Assign)
    2.31      //{{{
    2.32      {
    2.33 -      val cmds = global_state.change_yield(_.assign(id, assign))
    2.34 +      val cmds = global_state >>> (_.assign(id, assign))
    2.35        for (cmd <- cmds) delay_commands_changed.invoke(cmd)
    2.36      }
    2.37      //}}}
    2.38 @@ -309,7 +309,7 @@
    2.39      def handle_removed(removed: List[Document.Version_ID])
    2.40      //{{{
    2.41      {
    2.42 -      global_state.change(_.removed_versions(removed))
    2.43 +      global_state >> (_.removed_versions(removed))
    2.44      }
    2.45      //}}}
    2.46  
    2.47 @@ -327,7 +327,7 @@
    2.48        def id_command(command: Command)
    2.49        {
    2.50          if (!global_state().defined_command(command.id)) {
    2.51 -          global_state.change(_.define_command(command))
    2.52 +          global_state >> (_.define_command(command))
    2.53            prover.get.define_command(command)
    2.54          }
    2.55        }
    2.56 @@ -337,7 +337,7 @@
    2.57        }
    2.58  
    2.59        val assignment = global_state().the_assignment(previous).check_finished
    2.60 -      global_state.change(_.define_version(version, assignment))
    2.61 +      global_state >> (_.define_version(version, assignment))
    2.62        prover.get.update(previous.id, version.id, doc_edits)
    2.63      }
    2.64      //}}}
    2.65 @@ -358,7 +358,7 @@
    2.66  
    2.67          case Position.Id(state_id) if !result.is_raw =>
    2.68            try {
    2.69 -            val st = global_state.change_yield(_.accumulate(state_id, result.message))
    2.70 +            val st = global_state >>> (_.accumulate(state_id, result.message))
    2.71              delay_commands_changed.invoke(st.command)
    2.72            }
    2.73            catch {
    2.74 @@ -374,7 +374,7 @@
    2.75            }
    2.76            // FIXME separate timeout event/message!?
    2.77            if (prover.isDefined && System.currentTimeMillis() > prune_next) {
    2.78 -            val old_versions = global_state.change_yield(_.prune_history(prune_size))
    2.79 +            val old_versions = global_state >>> (_.prune_history(prune_size))
    2.80              if (!old_versions.isEmpty) prover.get.remove_versions(old_versions)
    2.81              prune_next = System.currentTimeMillis() + prune_delay.ms
    2.82            }
    2.83 @@ -441,7 +441,7 @@
    2.84  
    2.85          case Stop =>
    2.86            if (phase == Session.Ready) {
    2.87 -            global_state.change(_ => Document.State.init)  // FIXME event bus!?
    2.88 +            global_state >> (_ => Document.State.init)  // FIXME event bus!?
    2.89              phase = Session.Shutdown
    2.90              prover.get.terminate
    2.91              prover = None