src/Pure/PIDE/command.scala

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/PIDE/command.scala	Wed May 05 22:23:45 2010 +0200
@@ -0,0 +1,101 @@
+/*  Title:      Pure/PIDE/command.scala
+    Author:     Johannes Hölzl, TU Munich
+    Author:     Fabian Immler, TU Munich
+    Author:     Makarius
+
+Prover commands with semantic state.
+*/
+
+package isabelle
+
+
+import scala.actors.Actor, Actor._
+import scala.collection.mutable
+
+
+object Command
+{
+  object Status extends Enumeration
+  {
+    val UNPROCESSED = Value("UNPROCESSED")
+    val FINISHED = Value("FINISHED")
+    val FAILED = Value("FAILED")
+  }
+
+  case class HighlightInfo(highlight: String) { override def toString = highlight }
+  case class TypeInfo(ty: String)
+  case class RefInfo(file: Option[String], line: Option[Int],
+    command_id: Option[String], offset: Option[Int])
+}
+
+
+class Command(
+    val id: Isar_Document.Command_ID,
+    val span: Thy_Syntax.Span)
+  extends Session.Entity
+{
+  /* classification */
+
+  def is_command: Boolean = !span.isEmpty && span.head.is_command
+  def is_ignored: Boolean = span.forall(_.is_ignored)
+  def is_malformed: Boolean = !is_command && !is_ignored
+
+  def name: String = if (is_command) span.head.content else ""
+  override def toString = if (is_command) name else if (is_ignored) "<ignored>" else "<malformed>"
+
+
+  /* source text */
+
+  val source: String = span.map(_.source).mkString
+  def source(i: Int, j: Int): String = source.substring(i, j)
+  def length: Int = source.length
+
+  lazy val symbol_index = new Symbol.Index(source)
+
+
+  /* accumulated messages */
+
+  @volatile protected var state = new State(this)
+  def current_state: State = state
+
+  private case class Consume(session: Session, message: XML.Tree)
+  private case object Assign
+
+  private val accumulator = actor {
+    var assigned = false
+    loop {
+      react {
+        case Consume(session: Session, message: XML.Tree) if !assigned =>
+          state = state.+(session, message)
+
+        case Assign =>
+          assigned = true  // single assignment
+          reply(())
+
+        case bad => System.err.println("command accumulator: ignoring bad message " + bad)
+      }
+    }
+  }
+
+  def consume(session: Session, message: XML.Tree) { accumulator ! Consume(session, message) }
+
+  def assign_state(state_id: Isar_Document.State_ID): Command =
+  {
+    val cmd = new Command(state_id, span)
+    accumulator !? Assign
+    cmd.state = current_state
+    cmd
+  }
+
+
+  /* markup */
+
+  lazy val empty_markup = new Markup_Text(Nil, source)
+
+  def markup_node(begin: Int, end: Int, info: Any): Markup_Tree =
+  {
+    val start = symbol_index.decode(begin)
+    val stop = symbol_index.decode(end)
+    new Markup_Tree(new Markup_Node(start, stop, info), Nil)
+  }
+}