Change: eliminated id, which is merely the resulting document id and is only required in joined state anyway;
authorwenzelm
Thu Aug 12 16:01:44 2010 +0200 (2010-08-12)
changeset 38364827b90f18ff4
parent 38363 af7f41a8a0a8
child 38365 7c6254a9c432
Change: eliminated id, which is merely the resulting document id and is only required in joined state anyway;
Document.edit_text: create new document id here;
src/Pure/PIDE/document.scala
src/Pure/System/session.scala
     1.1 --- a/src/Pure/PIDE/document.scala	Thu Aug 12 15:19:11 2010 +0200
     1.2 +++ b/src/Pure/PIDE/document.scala	Thu Aug 12 16:01:44 2010 +0200
     1.3 @@ -107,11 +107,10 @@
     1.4  
     1.5    object Change
     1.6    {
     1.7 -    val init = new Change(NO_ID, None, Nil, Future.value(Nil, Document.init))
     1.8 +    val init = new Change(None, Nil, Future.value(Nil, Document.init))
     1.9    }
    1.10  
    1.11    class Change(
    1.12 -    val id: Version_ID,
    1.13      val parent: Option[Change],
    1.14      val edits: List[Node_Text_Edit],
    1.15      val result: Future[(List[Edit[Command]], Document)])
    1.16 @@ -156,8 +155,8 @@
    1.17  
    1.18    /** editing **/
    1.19  
    1.20 -  def text_edits(session: Session, old_doc: Document, new_id: Version_ID,
    1.21 -      edits: List[Node_Text_Edit]): (List[Edit[Command]], Document) =
    1.22 +  def text_edits(session: Session, old_doc: Document, edits: List[Node_Text_Edit])
    1.23 +      : (List[Edit[Command]], Document) =
    1.24    {
    1.25      require(old_doc.assignment.is_finished)
    1.26  
    1.27 @@ -258,7 +257,7 @@
    1.28          nodes += (name -> new Node(commands2))
    1.29          former_assignment --= removed_commands
    1.30        }
    1.31 -      (doc_edits.toList, new Document(new_id, nodes, former_assignment))
    1.32 +      (doc_edits.toList, new Document(session.create_id(), nodes, former_assignment))
    1.33      }
    1.34    }
    1.35  }
     2.1 --- a/src/Pure/System/session.scala	Thu Aug 12 15:19:11 2010 +0200
     2.2 +++ b/src/Pure/System/session.scala	Thu Aug 12 16:01:44 2010 +0200
     2.3 @@ -125,7 +125,7 @@
     2.4              (name -> Some(chs))
     2.5          }
     2.6        register_document(doc)
     2.7 -      prover.edit_document(change.parent.get.id, doc.id, id_edits)
     2.8 +      prover.edit_document(change.parent.get.join_document.id, doc.id, id_edits)
     2.9      }
    2.10      //}}}
    2.11  
    2.12 @@ -328,14 +328,13 @@
    2.13          react {
    2.14            case Edit_Document(edits) =>
    2.15              val old_change = history
    2.16 -            val new_id = create_id()
    2.17              val result: isabelle.Future[(List[Document.Edit[Command]], Document)] =
    2.18                isabelle.Future.fork {
    2.19                  val old_doc = old_change.join_document
    2.20                  old_doc.await_assignment
    2.21 -                Document.text_edits(Session.this, old_doc, new_id, edits)
    2.22 +                Document.text_edits(Session.this, old_doc, edits)
    2.23                }
    2.24 -            val new_change = new Document.Change(new_id, Some(old_change), edits, result)
    2.25 +            val new_change = new Document.Change(Some(old_change), edits, result)
    2.26              history = new_change
    2.27              new_change.result.map(_ => session_actor ! new_change)
    2.28              reply(())