# HG changeset patch
# User wenzelm
# Date 1310230490 -7200
# Node ID 8dd722886c76ab0277a5e8e958a0da759477f7b1
# Parent  ba1b2c918c322771550cd9ac7a2cbe9e28f62147
tuned;

diff -r ba1b2c918c32 -r 8dd722886c76 src/Pure/System/session.scala
--- a/src/Pure/System/session.scala	Sat Jul 09 18:35:00 2011 +0200
+++ b/src/Pure/System/session.scala	Sat Jul 09 18:54:50 2011 +0200
@@ -207,27 +207,20 @@
         removed <- previous.nodes(name).commands.get_after(prev)
       } former_assignment -= removed
 
+      def id_command(command: Command): Document.Command_ID =
+      {
+        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 =
         node_edits map {
-          case (name, None) => (name, None)
-          case (name, Some(cmd_edits)) =>
+          case (name, edits) =>
             val ids =
-              cmd_edits map {
-                case (c1, c2) =>
-                  val id1 = c1.map(_.id)
-                  val id2 =
-                    c2 match {
-                      case None => None
-                      case Some(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))
-                        }
-                        Some(command.id)
-                    }
-                  (id1, id2)
-              }
-            (name -> Some(ids))
+              edits.map(_.map { case (c1, c2) => (c1.map(id_command), c2.map(id_command)) })
+            (name, ids)
         }
       global_state.change(_.define_version(version, former_assignment))
       prover.get.edit_version(previous.id, version.id, id_edits)