src/Tools/jEdit/src/proofdocument/change.scala
changeset 34827 69852bd3c4c4
parent 34825 7f72547f9b12
child 34833 683ddf358698
equal deleted inserted replaced
34826:6b38fc0b3406 34827:69852bd3c4c4
    38 }
    38 }
    39 // TODO: merge multiple inserts?
    39 // TODO: merge multiple inserts?
    40 
    40 
    41 
    41 
    42 class Change(
    42 class Change(
    43   val id: Isar_Document.Document_ID,
       
    44   val parent: Option[Change],
    43   val parent: Option[Change],
    45   val edits: List[Edit],
    44   val edits: List[Edit],
    46   val result: Future[Document.Result])
    45   val result: Future[Document.Result])
    47 {
    46 {
    48   // FIXME iterator
    47   // FIXME iterator