src/Pure/System/session.scala
changeset 38364 827b90f18ff4
parent 38363 af7f41a8a0a8
child 38365 7c6254a9c432
     1.1 --- a/src/Pure/System/session.scala	Thu Aug 12 15:19:11 2010 +0200
     1.2 +++ b/src/Pure/System/session.scala	Thu Aug 12 16:01:44 2010 +0200
     1.3 @@ -125,7 +125,7 @@
     1.4              (name -> Some(chs))
     1.5          }
     1.6        register_document(doc)
     1.7 -      prover.edit_document(change.parent.get.id, doc.id, id_edits)
     1.8 +      prover.edit_document(change.parent.get.join_document.id, doc.id, id_edits)
     1.9      }
    1.10      //}}}
    1.11  
    1.12 @@ -328,14 +328,13 @@
    1.13          react {
    1.14            case Edit_Document(edits) =>
    1.15              val old_change = history
    1.16 -            val new_id = create_id()
    1.17              val result: isabelle.Future[(List[Document.Edit[Command]], Document)] =
    1.18                isabelle.Future.fork {
    1.19                  val old_doc = old_change.join_document
    1.20                  old_doc.await_assignment
    1.21 -                Document.text_edits(Session.this, old_doc, new_id, edits)
    1.22 +                Document.text_edits(Session.this, old_doc, edits)
    1.23                }
    1.24 -            val new_change = new Document.Change(new_id, Some(old_change), edits, result)
    1.25 +            val new_change = new Document.Change(Some(old_change), edits, result)
    1.26              history = new_change
    1.27              new_change.result.map(_ => session_actor ! new_change)
    1.28              reply(())