src/Pure/System/isar_document.scala
changeset 38417 b8922ae21111
parent 38414 49f1f657adc2
child 38418 9a7af64d71bb
     1.1 --- a/src/Pure/System/isar_document.scala	Sun Aug 15 13:17:45 2010 +0200
     1.2 +++ b/src/Pure/System/isar_document.scala	Sun Aug 15 14:18:52 2010 +0200
     1.3 @@ -46,9 +46,9 @@
     1.4      input("Isar_Document.define_command", Document.ID(id), text)
     1.5  
     1.6  
     1.7 -  /* documents */
     1.8 +  /* document versions */
     1.9  
    1.10 -  def edit_document(old_id: Document.Version_ID, new_id: Document.Version_ID,
    1.11 +  def edit_version(old_id: Document.Version_ID, new_id: Document.Version_ID,
    1.12        edits: List[Document.Edit[Document.Command_ID]])
    1.13    {
    1.14      def make_id1(id1: Option[Document.Command_ID]): XML.Body =
    1.15 @@ -60,7 +60,7 @@
    1.16            XML_Data.make_option(XML_Data.make_list(
    1.17                XML_Data.make_pair(make_id1)(XML_Data.make_option(XML_Data.make_long))))))(edits)
    1.18  
    1.19 -    input("Isar_Document.edit_document",
    1.20 +    input("Isar_Document.edit_version",
    1.21        Document.ID(old_id), Document.ID(new_id), YXML.string_of_body(arg))
    1.22    }
    1.23  }