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
+  }
+
 }