wenzelm@34407: /*
wenzelm@34407:  * Prover commands with semantic state
wenzelm@34407:  *
wenzelm@34407:  * @author Johannes Hölzl, TU Munich
wenzelm@34407:  * @author Fabian Immler, TU Munich
wenzelm@34407:  */
wenzelm@34407: 
wenzelm@34760: package isabelle.proofdocument
wenzelm@34318: 
wenzelm@34451: 
wenzelm@34699: import scala.actors.Actor, Actor._
wenzelm@34497: import scala.collection.mutable
wenzelm@34486: 
wenzelm@34777: import isabelle.jedit.Isabelle
immler@34675: 
wenzelm@34451: 
wenzelm@34637: object Command
wenzelm@34637: {
wenzelm@34637:   object Status extends Enumeration
wenzelm@34637:   {
wenzelm@34318:     val UNPROCESSED = Value("UNPROCESSED")
wenzelm@34318:     val FINISHED = Value("FINISHED")
wenzelm@34318:     val FAILED = Value("FAILED")
wenzelm@34318:   }
wenzelm@34707: 
wenzelm@34707:   case class HighlightInfo(highlight: String) { override def toString = highlight }
wenzelm@34717:   case class TypeInfo(ty: String)
wenzelm@34707:   case class RefInfo(file: Option[String], line: Option[Int],
wenzelm@34717:     command_id: Option[String], offset: Option[Int])
wenzelm@34318: }
wenzelm@34318: 
wenzelm@34451: 
wenzelm@34697: class Command(
wenzelm@34813:     val id: Isar_Document.Command_ID,
wenzelm@34859:     val span: Thy_Syntax.Span)
wenzelm@34815:   extends Session.Entity
wenzelm@34451: {
wenzelm@34859:   /* classification */
wenzelm@34500: 
wenzelm@34859:   def is_command: Boolean = !span.isEmpty && span.first.is_command
wenzelm@34865:   def is_ignored: Boolean = span.forall(_.is_ignored)
wenzelm@34859:   def is_malformed: Boolean = !is_command && !is_ignored
wenzelm@34859: 
wenzelm@34859:   def name: String = if (is_command) span.first.content else ""
wenzelm@34859:   override def toString = if (is_command) name else if (is_ignored) "<ignored>" else "<malformed>"
wenzelm@34495: 
wenzelm@34859: 
wenzelm@34859:   /* source text */
wenzelm@34451: 
wenzelm@34859:   val source: String = span.map(_.source).mkString
wenzelm@34859:   def source(i: Int, j: Int): String = source.substring(i, j)
wenzelm@34859:   def length: Int = source.length
wenzelm@34855: 
wenzelm@34859:   lazy val symbol_index = new Symbol.Index(source)
immler@34593: 
wenzelm@34815: 
wenzelm@34815:   /* accumulated messages */
wenzelm@34815: 
wenzelm@34815:   @volatile protected var state = new State(this)
wenzelm@34815:   def current_state: State = state
wenzelm@34815: 
wenzelm@34815:   private case class Consume(session: Session, message: XML.Tree)
wenzelm@34832:   private case object Assign
wenzelm@34815: 
wenzelm@34815:   private val accumulator = actor {
wenzelm@34832:     var assigned = false
wenzelm@34815:     loop {
wenzelm@34815:       react {
wenzelm@34832:         case Consume(session: Session, message: XML.Tree) if !assigned =>
wenzelm@34815:           state = state.+(session, message)
wenzelm@34815: 
wenzelm@34832:         case Assign =>
wenzelm@34835:           assigned = true  // single assignment
wenzelm@34832:           reply(())
wenzelm@34815: 
wenzelm@34815:         case bad => System.err.println("command accumulator: ignoring bad message " + bad)
wenzelm@34815:       }
wenzelm@34815:     }
wenzelm@34815:   }
wenzelm@34815: 
wenzelm@34815:   def consume(session: Session, message: XML.Tree) { accumulator ! Consume(session, message) }
wenzelm@34815: 
wenzelm@34832:   def assign_state(state_id: Isar_Document.State_ID): Command =
wenzelm@34815:   {
wenzelm@34859:     val cmd = new Command(state_id, span)
wenzelm@34832:     accumulator !? Assign
wenzelm@34815:     cmd.state = current_state
wenzelm@34815:     cmd
wenzelm@34815:   }
immler@34676: 
immler@34676: 
immler@34676:   /* markup */
wenzelm@34508: 
wenzelm@34859:   lazy val empty_markup = new Markup_Text(Nil, source)
immler@34676: 
wenzelm@34717:   def markup_node(begin: Int, end: Int, info: Any): Markup_Tree =
wenzelm@34699:   {
wenzelm@34703:     val start = symbol_index.decode(begin)
wenzelm@34703:     val stop = symbol_index.decode(end)
wenzelm@34717:     new Markup_Tree(new Markup_Node(start, stop, info), Nil)
wenzelm@34500:   }
immler@34676: }