# HG changeset patch
# User wenzelm
# Date 1314040166 -7200
# Node ID f99906c2a1d3afd824f0e18c03000721269e40a8
# Parent  9afa4a0e6f3cd7f8faf782d697fba4ccfd391d73
discontinued redundant Edit_Command_ID;

diff -r 9afa4a0e6f3c -r f99906c2a1d3 src/Pure/PIDE/document.scala
--- a/src/Pure/PIDE/document.scala	Mon Aug 22 20:11:44 2011 +0200
+++ b/src/Pure/PIDE/document.scala	Mon Aug 22 21:09:26 2011 +0200
@@ -34,7 +34,6 @@
   type Edit[A] = (String, Node.Edit[A])
   type Edit_Text = Edit[Text.Edit]
   type Edit_Command = Edit[(Option[Command], Option[Command])]
-  type Edit_Command_ID = Edit[(Option[Command_ID], Option[Command_ID])]
 
   type Node_Header = Exn.Result[Thy_Header]
 
@@ -42,12 +41,13 @@
   {
     sealed abstract class Edit[A]
     {
-      def map[B](f: A => B): Edit[B] =
+      def foreach(f: A => Unit)
+      {
         this match {
-          case Clear() => Clear()
-          case Edits(es) => Edits(es.map(f))
-          case Header(header) => Header(header)
+          case Edits(es) => es.foreach(f)
+          case _ =>
         }
+      }
     }
     case class Clear[A]() extends Edit[A]
     case class Edits[A](edits: List[A]) extends Edit[A]
diff -r 9afa4a0e6f3c -r f99906c2a1d3 src/Pure/PIDE/isar_document.scala
--- a/src/Pure/PIDE/isar_document.scala	Mon Aug 22 20:11:44 2011 +0200
+++ b/src/Pure/PIDE/isar_document.scala	Mon Aug 22 21:09:26 2011 +0200
@@ -140,15 +140,16 @@
   /* document versions */
 
   def edit_version(old_id: Document.Version_ID, new_id: Document.Version_ID,
-    edits: List[Document.Edit_Command_ID])
+    edits: List[Document.Edit_Command])
   {
     val edits_yxml =
     { import XML.Encode._
-      def encode: T[List[Document.Edit_Command_ID]] =
+      def id: T[Command] = (cmd => long(cmd.id))
+      def encode: T[List[Document.Edit_Command]] =
         list(pair(string,
           variant(List(
             { case Document.Node.Clear() => (Nil, Nil) },
-            { case Document.Node.Edits(a) => (Nil, list(pair(option(long), option(long)))(a)) },
+            { case Document.Node.Edits(a) => (Nil, list(pair(option(id), option(id)))(a)) },
             { case Document.Node.Header(Exn.Res(Thy_Header(a, b, c))) =>
                 (Nil, triple(string, list(string), list(pair(string, bool)))(a, b, c)) },
             { case Document.Node.Header(Exn.Exn(e)) => (List(Exn.message(e)), Nil) }))))
diff -r 9afa4a0e6f3c -r f99906c2a1d3 src/Pure/System/session.scala
--- a/src/Pure/System/session.scala	Mon Aug 22 20:11:44 2011 +0200
+++ b/src/Pure/System/session.scala	Mon Aug 22 21:09:26 2011 +0200
@@ -229,22 +229,20 @@
         removed <- previous.nodes(name).commands.get_after(prev)
       } former_assignment -= removed
 
-      def id_command(command: Command): Document.Command_ID =
+      def id_command(command: Command)
       {
         if (global_state().lookup_command(command.id).isEmpty) {
           global_state.change(_.define_command(command))
           prover.get.define_command(command.id, Symbol.encode(command.source))
         }
-        command.id
       }
-      val id_edits =
-        doc_edits map {
-          case (name, edit) =>
-            (name, edit.map({ case (c1, c2) => (c1.map(id_command), c2.map(id_command)) }))
-        }
+      doc_edits foreach {
+        case (_, edit) =>
+          edit foreach { case (c1, c2) => c1 foreach id_command; c2 foreach id_command }
+      }
 
       global_state.change(_.define_version(version, former_assignment))
-      prover.get.edit_version(previous.id, version.id, id_edits)
+      prover.get.edit_version(previous.id, version.id, doc_edits)
     }
     //}}}