equal
deleted
inserted
replaced
59 /* protocol messages */ |
59 /* protocol messages */ |
60 |
60 |
61 object Keyword_Decl { |
61 object Keyword_Decl { |
62 def unapply(msg: XML.Tree): Option[String] = |
62 def unapply(msg: XML.Tree): Option[String] = |
63 msg match { |
63 msg match { |
64 case XML.Elem(Markup(Markup.KEYWORD_DECL, List((Markup.NAME, name))), _) => Some(name) |
64 case XML.Elem(Markup(Isabelle_Markup.KEYWORD_DECL, List((Markup.NAME, name))), _) => |
|
65 Some(name) |
65 case _ => None |
66 case _ => None |
66 } |
67 } |
67 } |
68 } |
68 |
69 |
69 object Command_Decl { |
70 object Command_Decl { |
70 def unapply(msg: XML.Tree): Option[(String, String)] = |
71 def unapply(msg: XML.Tree): Option[(String, String)] = |
71 msg match { |
72 msg match { |
72 case XML.Elem(Markup(Markup.COMMAND_DECL, List((Markup.NAME, name), (Markup.KIND, kind))), _) => |
73 case XML.Elem(Markup(Isabelle_Markup.COMMAND_DECL, |
73 Some((name, kind)) |
74 List((Markup.NAME, name), (Markup.KIND, kind))), _) => Some((name, kind)) |
74 case _ => None |
75 case _ => None |
75 } |
76 } |
76 } |
77 } |
77 } |
78 } |
78 |
79 |