src/Tools/jEdit/src/prover/Command.scala
author wenzelm
Tue Jan 27 22:16:29 2009 +0100 (2009-01-27 ago)
changeset 34508 422a43b76f77
parent 34500 384427c750c8
child 34511 5839e34ef0bd
child 34533 35308320713a
permissions -rw-r--r--
eliminated Command.Status.REMOVE/REMOVED;
added state_id;
refined add_result: running flag;
     1 /*
     2  * Prover commands with semantic state
     3  *
     4  * @author Johannes Hölzl, TU Munich
     5  * @author Fabian Immler, TU Munich
     6  */
     7 
     8 package isabelle.prover
     9 
    10 
    11 import javax.swing.text.Position
    12 import javax.swing.tree.DefaultMutableTreeNode
    13 
    14 import scala.collection.mutable
    15 
    16 import isabelle.proofdocument.{Text, Token, ProofDocument}
    17 import isabelle.jedit.{Isabelle, Plugin}
    18 import isabelle.XML
    19 
    20 import sidekick.{SideKickParsedData, IAsset}
    21 
    22 
    23 object Command {
    24   object Status extends Enumeration {
    25     val UNPROCESSED = Value("UNPROCESSED")
    26     val FINISHED = Value("FINISHED")
    27     val FAILED = Value("FAILED")
    28   }
    29 }
    30 
    31 
    32 class Command(text: Text, val first: Token, val last: Token)
    33 {
    34   val id = Isabelle.plugin.id()
    35 
    36 
    37   /* content */
    38 
    39   {
    40     var t = first
    41     while (t != null) {
    42       t.command = this
    43       t = if (t == last) null else t.next
    44     }
    45   }
    46 
    47   override def toString = name
    48 
    49   val name = text.content(first.start, first.stop)
    50   val content = text.content(proper_start, proper_stop)
    51 
    52   def next = if (last.next != null) last.next.command else null
    53   def prev = if (first.prev != null) first.prev.command else null
    54 
    55   def start = first.start
    56   def stop = last.stop
    57 
    58   def proper_start = start
    59   def proper_stop = {
    60     var i = last
    61     while (i != first && i.kind == Token.Kind.COMMENT)
    62       i = i.prev
    63     i.stop
    64   }
    65 
    66 
    67   /* command status */
    68 
    69   var state_id: IsarDocument.State_ID = null
    70 
    71   private var _status = Command.Status.UNPROCESSED
    72   def status = _status
    73   def status_=(st: Command.Status.Value) {
    74     if (st == Command.Status.UNPROCESSED) {
    75       // delete markup
    76       for (child <- root_node.children) {
    77         child.children = Nil
    78       }
    79     }
    80     _status = st
    81   }
    82 
    83 
    84   /* results */
    85 
    86   private val results = new mutable.ListBuffer[XML.Tree]
    87   private val state_results = new mutable.ListBuffer[XML.Tree]
    88   def add_result(running: Boolean, tree: XML.Tree) {
    89     (if (running) state_results else results) += tree
    90   }
    91 
    92   def result_document = XML.document(
    93     results.toList ::: state_results.toList match {
    94       case Nil => XML.Elem("message", Nil, Nil)
    95       case List(elem) => elem
    96       case elems => XML.Elem("messages", Nil, elems)
    97     }, "style")
    98 
    99 
   100   /* markup */
   101 
   102   val root_node =
   103     new MarkupNode(this, 0, stop - start, id, Markup.COMMAND_SPAN, content)
   104 
   105   def node_from(kind: String, begin: Int, end: Int) = {
   106     val markup_content = /*content.substring(begin, end)*/ ""
   107     new MarkupNode(this, begin, end, id, kind, markup_content)
   108   }
   109 }