# HG changeset patch
# User immler@in.tum.de
# Date 1224598873 -7200
# Node ID 0b846b3ccc32e9e2d8a8cb6c6fa3d66bda35cddc
# Parent  8622e3a0274ef28534aeed0d0ea7b66f1d5ee116
reading command_decls from 'new' protocol

diff -r 8622e3a0274e -r 0b846b3ccc32 src/Tools/jEdit/src/prover/Prover.scala
--- a/src/Tools/jEdit/src/prover/Prover.scala	Mon Oct 20 20:25:54 2008 +0200
+++ b/src/Tools/jEdit/src/prover/Prover.scala	Tue Oct 21 16:21:13 2008 +0200
@@ -57,12 +57,21 @@
         else {
           val tree = parse_failsafe(converter.decode(r.result))
           tree match {
-            case Elem("message", _, List(Elem("command_decl", List(("name", name), 
-                                                                   ("kind", _)), _))) =>
-              commandKeywords.addEntry(name)
+            case Elem("message", List(("class","status")), decls) =>
+              decls map (decl => decl match{
+                  case Elem("command_decl", List(("name", name), ("kind", _)), _) =>
+                    commandKeywords.addEntry(name)
+                  case Elem("keyword_decl", List(("name", keyw)), _) => 
+                    () //TODO: with these keywords simplify the token-regex in ProofDocument
+                  case _ => 
+                    //TODO
+                    if (st != null)
+                    handleResult(st, r, tree)
+                }) 
             case _ =>
+              //TODO
               if (st != null)
-                handleResult(st, r, tree)
+              handleResult(st, r, tree)
           }
         }