extractors for document updates;
authorwenzelm
Thu May 06 15:04:37 2010 +0200 (2010-05-06)
changeset 366823f989067f87d
parent 36681 dffeca08d3bf
child 36683 41a1210519fd
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;
src/Pure/Isar/isar_document.scala
src/Pure/System/session.scala
     1.1 --- a/src/Pure/Isar/isar_document.scala	Thu May 06 13:41:30 2010 +0200
     1.2 +++ b/src/Pure/Isar/isar_document.scala	Thu May 06 15:04:37 2010 +0200
     1.3 @@ -14,6 +14,26 @@
     1.4    type State_ID = String
     1.5    type Command_ID = String
     1.6    type Document_ID = String
     1.7 +
     1.8 +
     1.9 +  /* reports */
    1.10 +
    1.11 +  object Assign {
    1.12 +    def unapply(msg: XML.Tree): Option[List[XML.Tree]] =
    1.13 +      msg match {
    1.14 +        case XML.Elem(Markup.ASSIGN, Nil, edits) => Some(edits)
    1.15 +        case _ => None
    1.16 +      }
    1.17 +  }
    1.18 +
    1.19 +  object Edit {
    1.20 +    def unapply(msg: XML.Tree): Option[(Command_ID, State_ID)] =
    1.21 +      msg match {
    1.22 +        case XML.Elem(Markup.EDIT, List((Markup.ID, cmd_id), (Markup.STATE, state_id)), Nil) =>
    1.23 +          Some(cmd_id, state_id)
    1.24 +        case _ => None
    1.25 +      }
    1.26 +  }
    1.27  }
    1.28  
    1.29  
     2.1 --- a/src/Pure/System/session.scala	Thu May 06 13:41:30 2010 +0200
     2.2 +++ b/src/Pure/System/session.scala	Thu May 06 15:04:37 2010 +0200
     2.3 @@ -123,12 +123,12 @@
     2.4          result.body match {
     2.5  
     2.6            // document state assignment
     2.7 -          case List(XML.Elem(Markup.ASSIGN, _, edits)) if target_id.isDefined =>
     2.8 +          case List(Isar_Document.Assign(edits)) if target_id.isDefined =>
     2.9              documents.get(target_id.get) match {
    2.10                case Some(doc) =>
    2.11                  val states =
    2.12                    for {
    2.13 -                    XML.Elem(Markup.EDIT, (Markup.ID, cmd_id) :: (Markup.STATE, state_id) :: _, _) <- edits
    2.14 +                    Isar_Document.Edit(cmd_id, state_id) <- edits
    2.15                      cmd <- lookup_command(cmd_id)
    2.16                    } yield {
    2.17                      val st = cmd.assign_state(state_id)
    2.18 @@ -139,11 +139,9 @@
    2.19                case None => bad_result(result)
    2.20              }
    2.21  
    2.22 -          // command and keyword declarations
    2.23 -          case List(XML.Elem(Markup.COMMAND_DECL, (Markup.NAME, name) :: (Markup.KIND, kind) :: _, _)) =>
    2.24 -            syntax += (name, kind)
    2.25 -          case List(XML.Elem(Markup.KEYWORD_DECL, (Markup.NAME, name) :: _, _)) =>
    2.26 -            syntax += name
    2.27 +          // keyword declarations
    2.28 +          case List(Outer_Keyword.Command_Decl(name, kind)) => syntax += (name, kind)
    2.29 +          case List(Outer_Keyword.Keyword_Decl(name)) => syntax += name
    2.30  
    2.31            case _ => if (!result.is_ready) bad_result(result)
    2.32          }