changeset 40479 | cc06f5528bb1 |
parent 39627 | 108901b49210 |
child 43722 | 9b5dadb0c28d |
--- a/src/Pure/PIDE/isar_document.scala Thu Nov 11 16:48:46 2010 +0100 +++ b/src/Pure/PIDE/isar_document.scala Thu Nov 11 17:07:05 2010 +0100 @@ -140,7 +140,7 @@ /* document versions */ def edit_version(old_id: Document.Version_ID, new_id: Document.Version_ID, - edits: List[Document.Edit[Document.Command_ID]]) + edits: List[Document.Edit_Command_ID]) { val arg = XML_Data.make_list(