# HG changeset patch
# User wenzelm
# Date 1253131271 -7200
# Node ID 4431c498726d321eb8d0c72a88474db746198204
# Parent  ec35626a2aa58a765a583bee2db96a1c8bde9bb3
tuned;

diff -r ec35626a2aa5 -r 4431c498726d src/Tools/jEdit/src/jedit/TheoryView.scala
--- a/src/Tools/jEdit/src/jedit/TheoryView.scala	Wed Sep 16 17:13:14 2009 +0200
+++ b/src/Tools/jEdit/src/jedit/TheoryView.scala	Wed Sep 16 22:01:11 2009 +0200
@@ -290,7 +290,7 @@
     text_area.invalidateLineRange(start, stop)
 
     if (Isabelle.plugin.selected_state == cmd)
-        Isabelle.plugin.selected_state = cmd  // update State view
+      Isabelle.plugin.selected_state = cmd  // update State view
   }
 
   private def invalidate_all() =
diff -r ec35626a2aa5 -r 4431c498726d src/Tools/jEdit/src/proofdocument/ProofDocument.scala
--- a/src/Tools/jEdit/src/proofdocument/ProofDocument.scala	Wed Sep 16 17:13:14 2009 +0200
+++ b/src/Tools/jEdit/src/proofdocument/ProofDocument.scala	Wed Sep 16 22:01:11 2009 +0200
@@ -70,7 +70,7 @@
     ((this, Nil: StructureChange) /: change.edits)(edit_doc)
   }
 
-  def text_edit(e: Edit, id: String): (ProofDocument,StructureChange) =
+  def text_edit(e: Edit, id: String): (ProofDocument, StructureChange) =
   {
     case class TextChange(start: Int, added: String, removed: String)
     val change = e match {
diff -r ec35626a2aa5 -r 4431c498726d src/Tools/jEdit/src/prover/Prover.scala
--- a/src/Tools/jEdit/src/prover/Prover.scala	Wed Sep 16 17:13:14 2009 +0200
+++ b/src/Tools/jEdit/src/prover/Prover.scala	Wed Sep 16 22:01:11 2009 +0200
@@ -43,7 +43,7 @@
   /* prover process */
 
   private val process =
-  new Isabelle_Process(system, this, "-m", "xsymbols", logic) with Isar_Document
+    new Isabelle_Process(system, this, "-m", "xsymbols", logic) with Isar_Document
 
   def stop() { process.kill }
 
@@ -103,20 +103,21 @@
                   case Some(doc) =>
                     for {
                       XML.Elem(Markup.EDIT, (Markup.ID, cmd_id) :: (Markup.STATE, state_id) :: _, _)
-                      <- edits
-                    } {
-                      if (commands.contains(cmd_id)) {
-                        val cmd = commands(cmd_id)
-                        val state = new Command_State(cmd)
-                        states += (state_id -> state)
-                        doc.states += (cmd -> state)
-                        command_change.event(cmd)
-                     }
+                      <- edits }
+                    {
+                      commands.get(cmd_id) match {
+                        case Some(cmd) =>
+                          val state = new Command_State(cmd)
+                          states += (state_id -> state)
+                          doc.states += (cmd -> state)
+                          command_change.event(cmd)
+                        case None =>
+                      }
                     }
                   case None =>
                 }
 
-                // command and keyword declarations
+              // command and keyword declarations
               case XML.Elem(Markup.COMMAND_DECL, (Markup.NAME, name) :: (Markup.KIND, kind) :: _, _) =>
                 _command_decls += (name -> kind)
                 _completion += name
@@ -124,7 +125,7 @@
                 _keyword_decls += name
                 _completion += name
 
-                // process ready (after initialization)
+              // process ready (after initialization)
               case XML.Elem(Markup.READY, _, _) => prover_ready = true
 
               case _ =>