# HG changeset patch
# User wenzelm
# Date 1251983347 -7200
# Node ID 33286290e3b0b8508277bac8e853be29e5aef0e8
# Parent  3d4874198e62dcdddc223d3c2d614fc96963f9d4
tuned;

diff -r 3d4874198e62 -r 33286290e3b0 src/Tools/jEdit/src/prover/Command.scala
--- a/src/Tools/jEdit/src/prover/Command.scala	Thu Sep 03 14:46:42 2009 +0200
+++ b/src/Tools/jEdit/src/prover/Command.scala	Thu Sep 03 15:09:07 2009 +0200
@@ -105,32 +105,25 @@
 }
 
 
-class Command_State(val cmd: Command)
-extends Accumulator
+class Command_State(val command: Command) extends Accumulator
 {
-
-  protected override var _state = new State(cmd)
+  protected override var _state = new State(command)
 
-
-  // combining command and state
-  def result_document = {
-    val cmd_results = cmd.state.results
+  def result_document: org.w3c.dom.Document =
     XML.document(
-      cmd_results.toList ::: state.results.toList match {
+      command.state.results ::: state.results match {
         case Nil => XML.Elem("message", Nil, Nil)
         case List(elem) => elem
         case elems => XML.Elem("messages", Nil, elems)
       }, "style")
-  }
 
   def markup_root: MarkupNode =
-    (cmd.state.markup_root /: state.markup_root.children) (_ + _)
+    (command.state.markup_root /: state.markup_root.children) (_ + _)
 
   def type_at(pos: Int): String = state.type_at(pos)
 
   def ref_at(pos: Int): Option[MarkupNode] = state.ref_at(pos)
 
-  def highlight_node =
-    (cmd.state.highlight_node /: state.highlight_node.children) (_ + _)
-
+  def highlight_node: MarkupNode =
+    (command.state.highlight_node /: state.highlight_node.children) (_ + _)
 }
\ No newline at end of file