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@34318: package isabelle.prover
wenzelm@34318: 
wenzelm@34451: 
immler@34393: import javax.swing.text.Position
immler@34393: import javax.swing.tree.DefaultMutableTreeNode
wenzelm@34318: 
wenzelm@34497: import scala.collection.mutable
wenzelm@34486: 
wenzelm@34491: import isabelle.proofdocument.{Text, Token, ProofDocument}
wenzelm@34451: import isabelle.jedit.{Isabelle, Plugin}
wenzelm@34476: import isabelle.XML
wenzelm@34451: 
wenzelm@34451: import sidekick.{SideKickParsedData, IAsset}
wenzelm@34451: 
wenzelm@34451: 
wenzelm@34318: object Command {
wenzelm@34458:   object Status extends Enumeration {
wenzelm@34318:     val UNPROCESSED = Value("UNPROCESSED")
wenzelm@34318:     val FINISHED = Value("FINISHED")
wenzelm@34318:     val REMOVE = Value("REMOVE")
wenzelm@34318:     val REMOVED = Value("REMOVED")
wenzelm@34318:     val FAILED = Value("FAILED")
wenzelm@34318:   }
wenzelm@34318: }
wenzelm@34318: 
wenzelm@34451: 
wenzelm@34491: class Command(text: Text, val first: Token, val last: Token)
wenzelm@34451: {
wenzelm@34451:   val id = Isabelle.plugin.id()
wenzelm@34500: 
wenzelm@34500: 
wenzelm@34500:   /* content */
wenzelm@34500: 
wenzelm@34318:   {
wenzelm@34318:     var t = first
wenzelm@34451:     while (t != null) {
wenzelm@34318:       t.command = this
wenzelm@34318:       t = if (t == last) null else t.next
wenzelm@34318:     }
wenzelm@34318:   }
wenzelm@34451: 
wenzelm@34495:   override def toString = name
wenzelm@34495: 
wenzelm@34495:   val name = text.content(first.start, first.stop)
wenzelm@34491:   val content = text.content(proper_start, proper_stop)
immler@34396: 
wenzelm@34318:   def next = if (last.next != null) last.next.command else null
wenzelm@34483:   def prev = if (first.prev != null) first.prev.command else null
wenzelm@34318: 
wenzelm@34451:   def start = first.start
wenzelm@34451:   def stop = last.stop
wenzelm@34451: 
wenzelm@34451:   def proper_start = start
wenzelm@34451:   def proper_stop = {
wenzelm@34318:     var i = last
wenzelm@34484:     while (i != first && i.kind == Token.Kind.COMMENT)
wenzelm@34483:       i = i.prev
wenzelm@34318:     i.stop
wenzelm@34451:   }
wenzelm@34451: 
wenzelm@34451: 
wenzelm@34500:   /* command status */
wenzelm@34500: 
wenzelm@34500:   private var _status = Command.Status.UNPROCESSED
wenzelm@34500:   def status = _status
wenzelm@34500:   def status_=(st: Command.Status.Value) {
wenzelm@34500:     if (st == Command.Status.UNPROCESSED) {
wenzelm@34500:       // delete markup
wenzelm@34500:       for (child <- root_node.children) {
wenzelm@34500:         child.children = Nil
wenzelm@34500:       }
wenzelm@34500:     }
wenzelm@34500:     _status = st
wenzelm@34500:   }
wenzelm@34500: 
wenzelm@34500: 
wenzelm@34500:   /* results */
wenzelm@34500: 
wenzelm@34500:   private val results = new mutable.ListBuffer[XML.Tree]
wenzelm@34500:   def add_result(tree: XML.Tree) { results += tree }
wenzelm@34500: 
wenzelm@34500:   private val state_results = new mutable.ListBuffer[XML.Tree]
wenzelm@34500:   def add_state_result(tree: XML.Tree) { state_results += tree }
wenzelm@34500: 
wenzelm@34500:   def result_document = XML.document(
wenzelm@34500:     results.toList ::: state_results.toList match {
wenzelm@34500:       case Nil => XML.Elem("message", Nil, Nil)
wenzelm@34500:       case List(elem) => elem
wenzelm@34500:       case elems => XML.Elem("messages", Nil, elems)
wenzelm@34500:     }, "style")
wenzelm@34500: 
wenzelm@34500: 
wenzelm@34500:   /* markup */
wenzelm@34451: 
wenzelm@34451:   val root_node =
wenzelm@34491:     new MarkupNode(this, 0, stop - start, id, Markup.COMMAND_SPAN, content)
wenzelm@34451: 
wenzelm@34451:   def node_from(kind: String, begin: Int, end: Int) = {
wenzelm@34451:     val markup_content = /*content.substring(begin, end)*/ ""
wenzelm@34451:     new MarkupNode(this, begin, end, id, kind, markup_content)
wenzelm@34451:   }
wenzelm@34451: }