1.1 --- a/src/Pure/Thy/command.scala Fri May 07 09:59:59 2010 +0200
1.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
1.3 @@ -1,100 +0,0 @@
1.4 -/*
1.5 - * Prover commands with semantic state
1.6 - *
1.7 - * @author Johannes Hölzl, TU Munich
1.8 - * @author Fabian Immler, TU Munich
1.9 - */
1.10 -
1.11 -package isabelle
1.12 -
1.13 -
1.14 -import scala.actors.Actor, Actor._
1.15 -import scala.collection.mutable
1.16 -
1.17 -
1.18 -object Command
1.19 -{
1.20 - object Status extends Enumeration
1.21 - {
1.22 - val UNPROCESSED = Value("UNPROCESSED")
1.23 - val FINISHED = Value("FINISHED")
1.24 - val FAILED = Value("FAILED")
1.25 - }
1.26 -
1.27 - case class HighlightInfo(highlight: String) { override def toString = highlight }
1.28 - case class TypeInfo(ty: String)
1.29 - case class RefInfo(file: Option[String], line: Option[Int],
1.30 - command_id: Option[String], offset: Option[Int])
1.31 -}
1.32 -
1.33 -
1.34 -class Command(
1.35 - val id: Isar_Document.Command_ID,
1.36 - val span: Thy_Syntax.Span)
1.37 - extends Session.Entity
1.38 -{
1.39 - /* classification */
1.40 -
1.41 - def is_command: Boolean = !span.isEmpty && span.head.is_command
1.42 - def is_ignored: Boolean = span.forall(_.is_ignored)
1.43 - def is_malformed: Boolean = !is_command && !is_ignored
1.44 -
1.45 - def name: String = if (is_command) span.head.content else ""
1.46 - override def toString = if (is_command) name else if (is_ignored) "<ignored>" else "<malformed>"
1.47 -
1.48 -
1.49 - /* source text */
1.50 -
1.51 - val source: String = span.map(_.source).mkString
1.52 - def source(i: Int, j: Int): String = source.substring(i, j)
1.53 - def length: Int = source.length
1.54 -
1.55 - lazy val symbol_index = new Symbol.Index(source)
1.56 -
1.57 -
1.58 - /* accumulated messages */
1.59 -
1.60 - @volatile protected var state = new State(this)
1.61 - def current_state: State = state
1.62 -
1.63 - private case class Consume(session: Session, message: XML.Tree)
1.64 - private case object Assign
1.65 -
1.66 - private val accumulator = actor {
1.67 - var assigned = false
1.68 - loop {
1.69 - react {
1.70 - case Consume(session: Session, message: XML.Tree) if !assigned =>
1.71 - state = state.+(session, message)
1.72 -
1.73 - case Assign =>
1.74 - assigned = true // single assignment
1.75 - reply(())
1.76 -
1.77 - case bad => System.err.println("command accumulator: ignoring bad message " + bad)
1.78 - }
1.79 - }
1.80 - }
1.81 -
1.82 - def consume(session: Session, message: XML.Tree) { accumulator ! Consume(session, message) }
1.83 -
1.84 - def assign_state(state_id: Isar_Document.State_ID): Command =
1.85 - {
1.86 - val cmd = new Command(state_id, span)
1.87 - accumulator !? Assign
1.88 - cmd.state = current_state
1.89 - cmd
1.90 - }
1.91 -
1.92 -
1.93 - /* markup */
1.94 -
1.95 - lazy val empty_markup = new Markup_Text(Nil, source)
1.96 -
1.97 - def markup_node(begin: Int, end: Int, info: Any): Markup_Tree =
1.98 - {
1.99 - val start = symbol_index.decode(begin)
1.100 - val stop = symbol_index.decode(end)
1.101 - new Markup_Tree(new Markup_Node(start, stop, info), Nil)
1.102 - }
1.103 -}