# HG changeset patch
# User immler@in.tum.de
# Date 1251363069 -7200
# Node ID 9e725d34df7bb78a9a7166fe7b8815b2f610e85b
# Parent  5427df0f6bcb9a59400277251af562f8fdcabe60
Command and Command_State handle results from prover as Accumulator
accumulating results in State;
prover outputs any result

diff -r 5427df0f6bcb -r 9e725d34df7b src/Tools/jEdit/src/proofdocument/ProofDocument.scala
--- a/src/Tools/jEdit/src/proofdocument/ProofDocument.scala	Thu Aug 27 10:51:09 2009 +0200
+++ b/src/Tools/jEdit/src/proofdocument/ProofDocument.scala	Thu Aug 27 10:51:09 2009 +0200
@@ -48,7 +48,7 @@
   val tokens: LinearSet[Token],
   val token_start: Map[Token, Int],
   val commands: LinearSet[Command],
-  var states: Map[Command, IsarDocument.State_ID],
+  var states: Map[Command, Command_State],
   is_command_keyword: String => Boolean,
   change_receiver: Actor)
 {
diff -r 5427df0f6bcb -r 9e725d34df7b src/Tools/jEdit/src/prover/Command.scala
--- a/src/Tools/jEdit/src/prover/Command.scala	Thu Aug 27 10:51:09 2009 +0200
+++ b/src/Tools/jEdit/src/prover/Command.scala	Thu Aug 27 10:51:09 2009 +0200
@@ -49,6 +49,7 @@
 
 
 class Command(val tokens: List[Token], val starts: Map[Token, Int], chg_rec: Actor)
+extends Accumulator
 {
   require(!tokens.isEmpty)
 
@@ -71,113 +72,82 @@
 
   def contains(p: Token) = tokens.contains(p)
 
-  /* states */
-  val states = mutable.Map[IsarDocument.State_ID, Command_State]()
-  private def state(doc: ProofDocument) = doc.states.get(this)
-  
-  /* command status */
+  protected override var _state = State.empty(this)
+
+
+  /* markup */
 
-  def set_status(state: IsarDocument.State_ID, status: Command.Status.Value) = {
-    if (state != null)
-      states.getOrElseUpdate(state, new Command_State(this)).status = status
+  lazy val empty_root_node =
+    new MarkupNode(this, 0, starts(tokens.last) - starts(tokens.first) + tokens.last.length,
+      Nil, id, content, RootInfo())
+
+  def markup_node(begin: Int, end: Int, info: MarkupInfo) = {
+    new MarkupNode(this, symbol_index.decode(begin), symbol_index.decode(end), Nil, id,
+      content.substring(symbol_index.decode(begin), symbol_index.decode(end)),
+      info)
   }
 
-  def status(doc: ProofDocument) =
-    state(doc) match {
-      case Some(s) => states.getOrElseUpdate(s, new Command_State(this)).status
-      case _ => Command.Status.UNPROCESSED
-    }
+
+  /* results, markup, ... */
 
-  /* results */
+  private val empty_cmd_state = new Command_State(this)
+  private def cmd_state(doc: ProofDocument) =
+    doc.states.getOrElse(this, empty_cmd_state)
 
-  private val results = new mutable.ListBuffer[XML.Tree]
-  def add_result(state: IsarDocument.State_ID, tree: XML.Tree) = synchronized {
-    (if (state == null) results else states(state).results) += tree
-  }
+  def status(doc: ProofDocument) = cmd_state(doc).state.status
+  def result_document(doc: ProofDocument) = cmd_state(doc).result_document
+  def markup_root(doc: ProofDocument) = cmd_state(doc).markup_root
+  def highlight_node(doc: ProofDocument) = cmd_state(doc).highlight_node
+  def type_at(doc: ProofDocument, offset: Int) = cmd_state(doc).type_at(offset)
+  def ref_at(doc: ProofDocument, offset: Int) = cmd_state(doc).ref_at(offset)
+}
+
 
-  def result_document(doc: ProofDocument) = {
-    val state_results = state(doc) match {
-      case Some(s) =>
-        states.getOrElseUpdate(s, new Command_State(this)).results
-      case _ => Nil}
+class Command_State(val cmd: Command)
+extends Accumulator
+{
+
+  protected override var _state = State.empty(cmd)
+
+
+  // combining command and state
+  def result_document = {
+    val cmd_results = cmd.state.results
     XML.document(
-      results.toList ::: state_results.toList match {
+      cmd_results.toList ::: state.results.toList match {
         case Nil => XML.Elem("message", Nil, Nil)
         case List(elem) => elem
         case elems => XML.Elem("messages", Nil, elems)
       }, "style")
   }
 
-
-  /* markup */
-
-  val empty_root_node =
-    new MarkupNode(this, 0, starts(tokens.last) - starts(tokens.first) + tokens.last.length,
-      Nil, id, content, RootInfo())
-  private var _markup_root = empty_root_node
-  def add_markup(state: IsarDocument.State_ID, raw_node: MarkupNode) = {
-    // decode node
-    val node = raw_node transform symbol_index.decode
-    if (state == null) _markup_root += node
-    else {
-      val cmd_state = states.getOrElseUpdate(state, new Command_State(this))
-      cmd_state.markup_root += node
-    }
+  def markup_root: MarkupNode = {
+    val cmd_markup_root = cmd.state.markup_root
+    (cmd_markup_root /: state.markup_root.children) (_ + _)
   }
 
-  def markup_root(doc: ProofDocument): MarkupNode = {
-    state(doc) match {
-      case Some(s) =>
-        (_markup_root /: states(s).markup_root.children) (_ + _)
-      case _ => _markup_root
-    }
-  }
-
-  def highlight_node(doc: ProofDocument): MarkupNode =
+  def highlight_node: MarkupNode =
   {
     import MarkupNode._
-    markup_root(doc).filter(_.info match {
-      case RootInfo() | OuterInfo(_) | HighlightInfo(_) => true
+    markup_root.filter(_.info match {
+      case RootInfo() | HighlightInfo(_) => true
       case _ => false
     }).head
   }
 
-  def markup_node(begin: Int, end: Int, info: MarkupInfo) =
-    new MarkupNode(this, begin, end, Nil, id,
-      if (end <= content.length && begin >= 0) content.substring(begin, end)
-      else "wrong indices??",
-      info)
-
-  def type_at(doc: ProofDocument, pos: Int) =
-    state(doc).map(states(_).type_at(pos)).getOrElse(null)
-
-  def ref_at(doc: ProofDocument, pos: Int) =
-    state(doc).flatMap(states(_).ref_at(pos))
-
-}
-
-class Command_State(val cmd: Command) {
-
-  var status = Command.Status.UNPROCESSED
-
-  /* results */
-  val results = new mutable.ListBuffer[XML.Tree]
-
-  /* markup */
-  val empty_root_node = cmd.empty_root_node
-  var markup_root = empty_root_node
-
   def type_at(pos: Int): String =
   {
-    val types = markup_root.filter(_.info match { case TypeInfo(_) => true case _ => false })
+    val types = state.markup_root.
+      filter(_.info match { case TypeInfo(_) => true case _ => false })
     types.flatten(_.flatten).
-      find(t => t.start <= pos && t.stop > pos).
-      map(t => t.content + ": " + (t.info match { case TypeInfo(i) => i case _ => "" })).
-      getOrElse(null)
+    find(t => t.start <= pos && t.stop > pos).
+    map(t => t.content + ": " + (t.info match { case TypeInfo(i) => i case _ => "" })).
+    getOrElse(null)
   }
 
   def ref_at(pos: Int): Option[MarkupNode] =
-    markup_root.filter(_.info match { case RefInfo(_, _, _, _) => true case _ => false }).
+    state.markup_root.
+      filter(_.info match { case RefInfo(_, _, _, _) => true case _ => false }).
       flatten(_.flatten).
       find(t => t.start <= pos && t.stop > pos)
 }
diff -r 5427df0f6bcb -r 9e725d34df7b src/Tools/jEdit/src/prover/MarkupNode.scala
--- a/src/Tools/jEdit/src/prover/MarkupNode.scala	Thu Aug 27 10:51:09 2009 +0200
+++ b/src/Tools/jEdit/src/prover/MarkupNode.scala	Thu Aug 27 10:51:09 2009 +0200
@@ -15,8 +15,6 @@
 
 abstract class MarkupInfo
 case class RootInfo() extends MarkupInfo
-case class OuterInfo(highlight: String) extends
-  MarkupInfo { override def toString = highlight }
 case class HighlightInfo(highlight: String) extends
   MarkupInfo { override def toString = highlight }
 case class TypeInfo(type_kind: String) extends
@@ -56,9 +54,6 @@
   val id: String, val content: String, val info: MarkupInfo)
 {
 
-  def transform(f: Int => Int): MarkupNode = new MarkupNode(base,
-    f(start), f(stop), children map (_ transform f), id, content, info)
-
   def swing_node(doc: ProofDocument): DefaultMutableTreeNode = {
     val node = MarkupNode.markup2default_node (this, base, doc)
     children.map(node add _.swing_node(doc))
diff -r 5427df0f6bcb -r 9e725d34df7b src/Tools/jEdit/src/prover/Prover.scala
--- a/src/Tools/jEdit/src/prover/Prover.scala	Thu Aug 27 10:51:09 2009 +0200
+++ b/src/Tools/jEdit/src/prover/Prover.scala	Thu Aug 27 10:51:09 2009 +0200
@@ -43,12 +43,14 @@
   
   /* document state information */
 
-  private val states = new mutable.HashMap[IsarDocument.State_ID, Command] with
-    mutable.SynchronizedMap[IsarDocument.State_ID, Command]
+  private val states = new mutable.HashMap[IsarDocument.State_ID, Command_State] with
+    mutable.SynchronizedMap[IsarDocument.State_ID, Command_State]
   private val commands = new mutable.HashMap[IsarDocument.Command_ID, Command] with
     mutable.SynchronizedMap[IsarDocument.Command_ID, Command]
   val document_0 =
-    ProofDocument.empty.set_command_keyword(command_decls.contains)
+    ProofDocument.empty.
+      set_command_keyword(command_decls.contains).
+      set_change_receiver(change_receiver)
   private var document_versions = List(document_0)
 
   def command(id: IsarDocument.Command_ID): Option[Command] = commands.get(id)
@@ -92,138 +94,72 @@
 
   private def handle_result(result: Isabelle_Process.Result)
   {
-    def command_change(c: Command) = c.changed()
-    val (state, command) =
+    val state =
       result.props.find(p => p._1 == Markup.ID) match {
-        case None => (null, null)
+        case None => None
         case Some((_, id)) =>
-          if (commands.contains(id)) (null, commands(id))
-          else if (states.contains(id)) (id, states(id))
-          else (null, null)
+          if (commands.contains(id)) Some(commands(id))
+          else if (states.contains(id)) Some(states(id))
+          else None
       }
-
-    if (result.kind == Isabelle_Process.Kind.STDOUT ||
-        result.kind == Isabelle_Process.Kind.STDIN)
-      output_info.event(result)
-    else {
-      result.kind match {
-
-        case Isabelle_Process.Kind.WRITELN
-        | Isabelle_Process.Kind.PRIORITY
-        | Isabelle_Process.Kind.WARNING
-        | Isabelle_Process.Kind.ERROR =>
-          if (command != null) {
-            if (result.kind == Isabelle_Process.Kind.ERROR)
-              command.set_status(state, Command.Status.FAILED)
-            command.add_result(state, process.parse_message(result))
-            command_change(command)
-          } else {
-            output_info.event(result)
-          }
+    output_info.event(result)
+    val message = process.parse_message(result)
+    if (state.isDefined) state.get ! message
+    else result.kind match {
 
-        case Isabelle_Process.Kind.STATUS =>
-          //{{{ handle all kinds of status messages here
-          process.parse_message(result) match {
-            case XML.Elem(Markup.MESSAGE, _, elems) =>
-              for (elem <- elems) {
-                elem match {
-                  //{{{
-                  // command and keyword declarations
-                  case XML.Elem(Markup.COMMAND_DECL,
-                      (Markup.NAME, name) :: (Markup.KIND, kind) :: _, _) =>
-                    command_decls += (name -> kind)
-                  case XML.Elem(Markup.KEYWORD_DECL, (Markup.NAME, name) :: _, _) =>
-                    keyword_decls += name
+      case Isabelle_Process.Kind.STATUS =>
+        //{{{ handle all kinds of status messages here
+        message match {
+          case XML.Elem(Markup.MESSAGE, _, elems) =>
+            for (elem <- elems) {
+              elem match {
+                //{{{
+                // command and keyword declarations
+                case XML.Elem(Markup.COMMAND_DECL,
+                    (Markup.NAME, name) :: (Markup.KIND, kind) :: _, _) =>
+                  command_decls += (name -> kind)
+                case XML.Elem(Markup.KEYWORD_DECL, (Markup.NAME, name) :: _, _) =>
+                  keyword_decls += name
 
-                  // process ready (after initialization)
-                  case XML.Elem(Markup.READY, _, _)
-                  if !initialized =>
-                    initialized = true
-                    change_receiver ! ProverEvents.Activate
-
-                  // document edits
-                  case XML.Elem(Markup.EDITS, (Markup.ID, doc_id) :: _, edits)
-                  if document_versions.exists(_.id == doc_id) =>
-                    output_info.event(result)
-                    val doc = document_versions.find(_.id == doc_id).get
-                    for {
-                      XML.Elem(Markup.EDIT, (Markup.ID, cmd_id) :: (Markup.STATE, state_id) :: _, _)
-                        <- edits
-                    } {
-                      if (commands.contains(cmd_id)) {
-                        val cmd = commands(cmd_id)
-                        states(state_id) = cmd
-                        doc.states += (cmd -> state_id)
-                        cmd.states += (state_id -> new Command_State(cmd))
-                        command_change(cmd)
-                      }
+                // process ready (after initialization)
+                case XML.Elem(Markup.READY, _, _)
+                if !initialized =>
+                  initialized = true
+                  change_receiver ! ProverEvents.Activate
 
+                // document edits
+                case XML.Elem(Markup.EDITS, (Markup.ID, doc_id) :: _, edits)
+                if document_versions.exists(_.id == doc_id) =>
+                  val doc = document_versions.find(_.id == doc_id).get
+                  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 status
-                  case XML.Elem(Markup.UNPROCESSED, _, _)
-                  if command != null =>
-                    output_info.event(result)
-                    command.set_status(state, Command.Status.UNPROCESSED)
-                    command_change(command)
-                  case XML.Elem(Markup.FINISHED, _, _)
-                  if command != null =>
-                    output_info.event(result)
-                    command.set_status(state, Command.Status.FINISHED)
-                    command_change(command)
-                  case XML.Elem(Markup.FAILED, _, _)
-                  if command != null =>
-                    output_info.event(result)
-                    command.set_status(state, Command.Status.FAILED)
-                    command_change(command)
-                  case XML.Elem(kind, attr, body)
-                  if command != null =>
-                    val (begin, end) = Position.offsets_of(attr)
-                    if (begin.isDefined && end.isDefined) {
-                      if (kind == Markup.ML_TYPING) {
-                        val info = body.first.asInstanceOf[XML.Text].content
-                        command.add_markup(state,
-                          command.markup_node(begin.get - 1, end.get - 1, TypeInfo(info)))
-                      } else if (kind == Markup.ML_REF) {
-                        body match {
-                          case List(XML.Elem(Markup.ML_DEF, attr, _)) =>
-                            command.add_markup(state, command.markup_node(
-                              begin.get - 1, end.get - 1,
-                              RefInfo(
-                                Position.file_of(attr),
-                                Position.line_of(attr),
-                                Position.id_of(attr),
-                                Position.offset_of(attr))))
-                          case _ =>
-                        }
-                      } else {
-                        command.add_markup(state,
-                          command.markup_node(begin.get - 1, end.get - 1, HighlightInfo(kind)))
-                      }
-                    }
-                    command_change(command)
-                  case XML.Elem(kind, attr, body)
-                  if command == null =>
-                    // TODO: This is mostly irrelevant information on removed commands, but it can
-                    // also be outer-syntax-markup since there is no id in props (fix that?)
-                    val (begin, end) = Position.offsets_of(attr)
-                    val markup_id = Position.id_of(attr)
-                    val outer = isabelle.jedit.DynamicTokenMarker.is_outer(kind)
-                    if (outer && state == null && begin.isDefined && end.isDefined && markup_id.isDefined)
-                      commands.get(markup_id.get).map (cmd => {
-                        cmd.add_markup(state,
-                          cmd.markup_node(begin.get - 1, end.get - 1, OuterInfo(kind)))
-                        command_change(cmd)
-                      })
-                  case _ =>
-                  //}}}
-                }
+
+                  }
+                case XML.Elem(kind, attr, body) =>
+                  // TODO: This is mostly irrelevant information on removed commands, but it can
+                  // also be outer-syntax-markup since there is no id in props (fix that?)
+                  val (begin, end) = Position.offsets_of(attr)
+                  val markup_id = Position.id_of(attr)
+                  val outer = isabelle.jedit.DynamicTokenMarker.is_outer(kind)
+                  if (outer && begin.isDefined && end.isDefined && markup_id.isDefined)
+                    commands.get(markup_id.get).map (cmd => cmd ! message)
+                case _ =>
+                //}}}
               }
-            case _ =>
-          }
-          //}}}
+            }
+          case _ =>
+        }
+        //}}}
 
-        case _ =>
-      }
+      case _ =>
     }
   }
 
diff -r 5427df0f6bcb -r 9e725d34df7b src/Tools/jEdit/src/prover/State.scala
--- a/src/Tools/jEdit/src/prover/State.scala	Thu Aug 27 10:51:09 2009 +0200
+++ b/src/Tools/jEdit/src/prover/State.scala	Thu Aug 27 10:51:09 2009 +0200
@@ -6,7 +6,96 @@
 
 package isabelle.prover
 
-abstract class State
+import scala.collection.mutable
+
+object State
+{
+  def empty(cmd: Command) = State(cmd, Command.Status.UNPROCESSED,
+    new mutable.ListBuffer, cmd.empty_root_node)
+}
+
+case class State(
+  cmd: Command,
+  status: Command.Status.Value,
+  results: mutable.Buffer[XML.Tree],
+  markup_root: MarkupNode
+)
 {
-  def +(message: XML.Tree): State
+
+  private def set_status(st: Command.Status.Value):State =
+    State(cmd, st, results, markup_root)
+  private def add_result(res: XML.Tree):State =
+    State(cmd, status, results + res, markup_root)
+  private def add_markup(markup: MarkupNode):State =
+    State(cmd, status, results, markup_root + markup)
+  /* markup */
+
+  def type_at(pos: Int): String =
+  {
+    val types = markup_root.filter(_.info match { case TypeInfo(_) => true case _ => false })
+    types.flatten(_.flatten).
+      find(t => t.start <= pos && t.stop > pos).
+      map(t => t.content + ": " + (t.info match { case TypeInfo(i) => i case _ => "" })).
+      getOrElse(null)
+  }
+
+  def ref_at(pos: Int): Option[MarkupNode] =
+    markup_root.filter(_.info match { case RefInfo(_, _, _, _) => true case _ => false }).
+      flatten(_.flatten).
+      find(t => t.start <= pos && t.stop > pos)
+
+  def +(message: XML.Tree) = {
+    val changed: State =
+    message match {
+      case XML.Elem(Markup.MESSAGE, (Markup.CLASS, Markup.WRITELN) :: _, _)
+      | XML.Elem(Markup.MESSAGE, (Markup.CLASS, Markup.PRIORITY) :: _, _)
+      | XML.Elem(Markup.MESSAGE, (Markup.CLASS, Markup.WARNING) :: _, _) =>
+        add_result(message)
+      case XML.Elem(Markup.MESSAGE, (Markup.CLASS, Markup.ERROR) :: _, _) =>
+        set_status(Command.Status.FAILED).add_result(message)
+      case XML.Elem(Markup.MESSAGE, (Markup.CLASS, Markup.STATUS) :: _, elems) =>
+        (this /: elems) ((r, e) =>
+          e match {
+            // command status
+            case XML.Elem(Markup.UNPROCESSED, _, _) =>
+              r.set_status(Command.Status.UNPROCESSED)
+            case XML.Elem(Markup.FINISHED, _, _) =>
+              r.set_status(Command.Status.FINISHED)
+            case XML.Elem(Markup.FAILED, _, _) =>
+              r.set_status(Command.Status.FAILED)
+            case XML.Elem(kind, attr, body) =>
+              val (begin, end) = Position.offsets_of(attr)
+              if (begin.isDefined && end.isDefined) {
+                if (kind == Markup.ML_TYPING) {
+                  val info = body.first.asInstanceOf[XML.Text].content
+                  r.add_markup(cmd.markup_node(begin.get - 1, end.get - 1, TypeInfo(info)))
+                } else if (kind == Markup.ML_REF) {
+                  body match {
+                    case List(XML.Elem(Markup.ML_DEF, attr, _)) =>
+                      r.add_markup(cmd.markup_node(
+                        begin.get - 1, end.get - 1,
+                        RefInfo(
+                          Position.file_of(attr),
+                          Position.line_of(attr),
+                          Position.id_of(attr),
+                          Position.offset_of(attr))))
+                    case _ =>
+                      r
+                  }
+                } else {
+                  r.add_markup(cmd.markup_node(begin.get - 1, end.get - 1, HighlightInfo(kind)))
+                }
+              } else
+                r
+            case _ =>
+              r
+          })
+      case _ =>
+        System.err.println("ignored: " + message)
+        this
+    }
+    cmd.changed()
+    changed
+  }
+
 }