tuned signature;
authorwenzelm
Thu Apr 24 23:21:00 2014 +0200 (2014-04-24)
changeset 56711ef3d00153e3b
parent 56710 8f102c18eab7
child 56712 c7cf653228ed
tuned signature;
src/Pure/PIDE/document.scala
src/Pure/PIDE/session.scala
src/Tools/jEdit/src/pretty_text_area.scala
     1.1 --- a/src/Pure/PIDE/document.scala	Thu Apr 24 23:13:17 2014 +0200
     1.2 +++ b/src/Pure/PIDE/document.scala	Thu Apr 24 23:21:00 2014 +0200
     1.3 @@ -608,12 +608,12 @@
     1.4      def tip_version: Version = history.tip.version.get_finished
     1.5  
     1.6      def continue_history(
     1.7 -        previous: Future[Version],
     1.8 -        edits: List[Edit_Text],
     1.9 -        version: Future[Version]): (Change, State) =
    1.10 +      previous: Future[Version],
    1.11 +      edits: List[Edit_Text],
    1.12 +      version: Future[Version]): State =
    1.13      {
    1.14        val change = Change.make(previous, edits, version)
    1.15 -      (change, copy(history = history + change))
    1.16 +      copy(history = history + change)
    1.17      }
    1.18  
    1.19      def prune_history(retain: Int = 0): (List[Version], State) =
     2.1 --- a/src/Pure/PIDE/session.scala	Thu Apr 24 23:13:17 2014 +0200
     2.2 +++ b/src/Pure/PIDE/session.scala	Thu Apr 24 23:21:00 2014 +0200
     2.3 @@ -345,7 +345,7 @@
     2.4  
     2.5        val previous = global_state.value.history.tip.version
     2.6        val version = Future.promise[Document.Version]
     2.7 -      val change = global_state.change_result(_.continue_history(previous, edits, version))
     2.8 +      global_state.change(_.continue_history(previous, edits, version))
     2.9  
    2.10        raw_edits.event(Session.Raw_Edits(doc_blobs, edits))
    2.11        change_parser.send(Text_Edits(previous, doc_blobs, edits, version))
     3.1 --- a/src/Tools/jEdit/src/pretty_text_area.scala	Thu Apr 24 23:13:17 2014 +0200
     3.2 +++ b/src/Tools/jEdit/src/pretty_text_area.scala	Thu Apr 24 23:21:00 2014 +0200
     3.3 @@ -36,7 +36,7 @@
     3.4      val nodes1 = nodes0 + (node_name -> nodes0(node_name).update_commands(Linear_Set(command)))
     3.5      val version1 = Document.Version.make(version0.syntax, nodes1)
     3.6      val state1 =
     3.7 -      state0.continue_history(Future.value(version0), edits, Future.value(version1))._2
     3.8 +      state0.continue_history(Future.value(version0), edits, Future.value(version1))
     3.9          .define_version(version1, state0.the_assignment(version0))
    3.10          .assign(version1.id, List(command.id -> List(Document_ID.make())))._2
    3.11