src/Pure/Thy/thy_syntax.scala
changeset 38417 b8922ae21111
parent 38374 7eb0f6991e25
child 38419 f9dc924e54f8
     1.1 --- a/src/Pure/Thy/thy_syntax.scala	Sun Aug 15 13:17:45 2010 +0200
     1.2 +++ b/src/Pure/Thy/thy_syntax.scala	Sun Aug 15 14:18:52 2010 +0200
     1.3 @@ -38,8 +38,8 @@
     1.4  
     1.5    /** text edits **/
     1.6  
     1.7 -  def text_edits(session: Session, old_doc: Document, edits: List[Document.Node_Text_Edit])
     1.8 -      : (List[Document.Edit[Command]], Document) =
     1.9 +  def text_edits(session: Session, previous: Document.Version,
    1.10 +      edits: List[Document.Node_Text_Edit]): (List[Document.Edit[Command]], Document.Version) =
    1.11    {
    1.12      /* phase 1: edit individual command source */
    1.13  
    1.14 @@ -110,7 +110,7 @@
    1.15  
    1.16      {
    1.17        val doc_edits = new mutable.ListBuffer[Document.Edit[Command]]
    1.18 -      var nodes = old_doc.nodes
    1.19 +      var nodes = previous.nodes
    1.20  
    1.21        for ((name, text_edits) <- edits) {
    1.22          val commands0 = nodes(name).commands
    1.23 @@ -127,7 +127,7 @@
    1.24          doc_edits += (name -> Some(cmd_edits))
    1.25          nodes += (name -> new Document.Node(commands2))
    1.26        }
    1.27 -      (doc_edits.toList, new Document(session.create_id(), nodes))
    1.28 +      (doc_edits.toList, new Document.Version(session.create_id(), nodes))
    1.29      }
    1.30    }
    1.31  }