extractors for document updates;
Session.handle_result: use extractors instead of raw patterns -- NB: using mixed patterns of case classes vs. extractors crashes Scala 2.8.1 RC1;

--- a/src/Pure/Isar/isar_document.scala	Thu May 06 13:41:30 2010 +0200
+++ b/src/Pure/Isar/isar_document.scala	Thu May 06 15:04:37 2010 +0200
@@ -14,6 +14,26 @@
   type State_ID = String
   type Command_ID = String
   type Document_ID = String
+
+
+  /* reports */
+
+  object Assign {
+    def unapply(msg: XML.Tree): Option[List[XML.Tree]] =
+      msg match {
+        case XML.Elem(Markup.ASSIGN, Nil, edits) => Some(edits)
+        case _ => None
+      }
+  }
+
+  object Edit {
+    def unapply(msg: XML.Tree): Option[(Command_ID, State_ID)] =
+      msg match {
+        case XML.Elem(Markup.EDIT, List((Markup.ID, cmd_id), (Markup.STATE, state_id)), Nil) =>
+          Some(cmd_id, state_id)
+        case _ => None
+      }
+  }
 }
 
 

--- a/src/Pure/System/session.scala	Thu May 06 13:41:30 2010 +0200
+++ b/src/Pure/System/session.scala	Thu May 06 15:04:37 2010 +0200
@@ -123,12 +123,12 @@
         result.body match {
 
           // document state assignment
-          case List(XML.Elem(Markup.ASSIGN, _, edits)) if target_id.isDefined =>
+          case List(Isar_Document.Assign(edits)) if target_id.isDefined =>
             documents.get(target_id.get) match {
               case Some(doc) =>
                 val states =
                   for {
-                    XML.Elem(Markup.EDIT, (Markup.ID, cmd_id) :: (Markup.STATE, state_id) :: _, _) <- edits
+                    Isar_Document.Edit(cmd_id, state_id) <- edits
                     cmd <- lookup_command(cmd_id)
                   } yield {
                     val st = cmd.assign_state(state_id)
@@ -139,11 +139,9 @@
               case None => bad_result(result)
             }
 
-          // command and keyword declarations
-          case List(XML.Elem(Markup.COMMAND_DECL, (Markup.NAME, name) :: (Markup.KIND, kind) :: _, _)) =>
-            syntax += (name, kind)
-          case List(XML.Elem(Markup.KEYWORD_DECL, (Markup.NAME, name) :: _, _)) =>
-            syntax += name
+          // keyword declarations
+          case List(Outer_Keyword.Command_Decl(name, kind)) => syntax += (name, kind)
+          case List(Outer_Keyword.Keyword_Decl(name)) => syntax += name
 
           case _ => if (!result.is_ready) bad_result(result)
         }