src/Tools/jEdit/src/prover/Command.scala
author wenzelm
Tue Jan 27 16:16:55 2009 +0100 (2009-01-27 ago)
changeset 34497 184fda8cce04
parent 34495 722533c532da
child 34500 384427c750c8
permissions -rw-r--r--
more explicit indication of mutable collections;
     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 REMOVE = Value("REMOVE")
    28     val REMOVED = Value("REMOVED")
    29     val FAILED = Value("FAILED")
    30   }
    31 }
    32 
    33 
    34 class Command(text: Text, val first: Token, val last: Token)
    35 {
    36   val id = Isabelle.plugin.id()
    37   
    38   {
    39     var t = first
    40     while (t != null) {
    41       t.command = this
    42       t = if (t == last) null else t.next
    43     }
    44   }
    45 
    46 
    47   /* command status */
    48 
    49   private var _status = Command.Status.UNPROCESSED
    50   def status = _status
    51   def status_=(st: Command.Status.Value) = {
    52     if (st == Command.Status.UNPROCESSED) {
    53       // delete markup
    54       for (child <- root_node.children) {
    55         child.children = Nil
    56       }
    57     }
    58     _status = st
    59   }
    60 
    61 
    62   /* accumulated results */
    63 
    64   private val results = new mutable.ListBuffer[XML.Tree]
    65   def add_result(tree: XML.Tree) { results += tree }
    66 
    67   def result_document = XML.document(
    68     results.toList match {
    69       case Nil => XML.Elem("message", Nil, Nil)
    70       case List(elem) => elem
    71       case elems => XML.Elem("messages", Nil, List(elems.first, elems.last))  // FIXME all elems!?
    72     }, "style")
    73 
    74 
    75   /* content */
    76 
    77   override def toString = name
    78 
    79   val name = text.content(first.start, first.stop)
    80   val content = text.content(proper_start, proper_stop)
    81 
    82   def next = if (last.next != null) last.next.command else null
    83   def prev = if (first.prev != null) first.prev.command else null
    84 
    85   def start = first.start
    86   def stop = last.stop
    87 
    88   def proper_start = start
    89   def proper_stop = {
    90     var i = last
    91     while (i != first && i.kind == Token.Kind.COMMENT)
    92       i = i.prev
    93     i.stop
    94   }
    95 
    96 
    97   /* markup tree */
    98 
    99   val root_node =
   100     new MarkupNode(this, 0, stop - start, id, Markup.COMMAND_SPAN, content)
   101 
   102   def node_from(kind: String, begin: Int, end: Int) = {
   103     val markup_content = /*content.substring(begin, end)*/ ""
   104     new MarkupNode(this, begin, end, id, kind, markup_content)
   105   }
   106 }