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@34451: import isabelle.proofdocument.Token
wenzelm@34451: import isabelle.jedit.{Isabelle, Plugin}
wenzelm@34451: import isabelle.{YXML, XML}
wenzelm@34451: 
wenzelm@34451: import sidekick.{SideKickParsedData, IAsset}
wenzelm@34451: 
wenzelm@34451: 
wenzelm@34318: object Command {
wenzelm@34318:   object Phase 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@34451: class Command(val document: Document, val first: Token[Command], val last: Token[Command])
wenzelm@34451: {
wenzelm@34451:   val id = Isabelle.plugin.id()
wenzelm@34318:   
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: 
immler@34399: 
wenzelm@34451:   /* command phase */
wenzelm@34451: 
wenzelm@34451:   private var p = Command.Phase.UNPROCESSED
immler@34399:   def phase = p
wenzelm@34451:   def phase_=(p_new: Command.Phase.Value) = {
wenzelm@34451:     if (p_new == Command.Phase.UNPROCESSED) {
wenzelm@34451:       // delete markup
wenzelm@34451:       for (child <- root_node.children) {
immler@34401:         child.children = Nil
immler@34399:       }
immler@34399:     }
immler@34399:     p = p_new
immler@34399:   }
wenzelm@34451: 
immler@34391: 
wenzelm@34451:   /* accumulated results */
wenzelm@34451: 
wenzelm@34451:   var results: List[XML.Tree] = Nil
wenzelm@34451: 
wenzelm@34410:   def results_xml = XML.document(
wenzelm@34410:     results match {
wenzelm@34410:       case Nil => XML.Elem("message", Nil, Nil)
wenzelm@34410:       case List(elem) => elem
wenzelm@34451:       case _ => XML.Elem("messages", Nil, List(results.first, results.last))
wenzelm@34410:     }, "style")
wenzelm@34451:   def add_result(tree: XML.Tree) {
wenzelm@34410:     results = results ::: List(tree)    // FIXME canonical reverse order
wenzelm@34318:   }
wenzelm@34451: 
immler@34393: 
wenzelm@34451:   /* content */
immler@34391: 
wenzelm@34451:   def content(): String = document.getContent(this)
immler@34396: 
wenzelm@34318:   def next = if (last.next != null) last.next.command else null
wenzelm@34318:   def previous = if (first.previous != null) first.previous.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
immler@34388:     while (i != first && i.kind.equals(Token.Kind.COMMENT))
wenzelm@34318:       i = i.previous
wenzelm@34318:     i.stop
wenzelm@34451:   }
wenzelm@34451: 
wenzelm@34451: 
wenzelm@34451:   /* markup tree */
wenzelm@34451: 
wenzelm@34451:   val root_node =
wenzelm@34451:     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: }