src/Tools/jEdit/src/prover/Command.scala
author wenzelm
Fri, 19 Dec 2008 22:24:32 +0100
changeset 34407 aad6834ba380
parent 34401 44241a37b74a
child 34410 f2644d2a3e8e
permissions -rw-r--r--
added some headers and comments;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
34407
aad6834ba380 added some headers and comments;
wenzelm
parents: 34401
diff changeset
     1
/*
aad6834ba380 added some headers and comments;
wenzelm
parents: 34401
diff changeset
     2
 * Prover commands with semantic state
aad6834ba380 added some headers and comments;
wenzelm
parents: 34401
diff changeset
     3
 *
aad6834ba380 added some headers and comments;
wenzelm
parents: 34401
diff changeset
     4
 * @author Johannes Hölzl, TU Munich
aad6834ba380 added some headers and comments;
wenzelm
parents: 34401
diff changeset
     5
 * @author Fabian Immler, TU Munich
aad6834ba380 added some headers and comments;
wenzelm
parents: 34401
diff changeset
     6
 */
aad6834ba380 added some headers and comments;
wenzelm
parents: 34401
diff changeset
     7
34318
c13e168a8ae6 original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff changeset
     8
package isabelle.prover
c13e168a8ae6 original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff changeset
     9
c13e168a8ae6 original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff changeset
    10
import isabelle.proofdocument.Token
34393
f0e1608a774f basic tree structure for sidekick
immler@in.tum.de
parents: 34391
diff changeset
    11
import isabelle.jedit.Plugin
34318
c13e168a8ae6 original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff changeset
    12
import isabelle.{ YXML, XML }
34400
1b61a92f8675 MarkupNode instead of DefaultMutableTreeNode and RelativeAsset
immler@in.tum.de
parents: 34399
diff changeset
    13
import sidekick.{SideKickParsedData, IAsset}
34393
f0e1608a774f basic tree structure for sidekick
immler@in.tum.de
parents: 34391
diff changeset
    14
import javax.swing.text.Position
f0e1608a774f basic tree structure for sidekick
immler@in.tum.de
parents: 34391
diff changeset
    15
import javax.swing.tree.DefaultMutableTreeNode
34318
c13e168a8ae6 original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff changeset
    16
c13e168a8ae6 original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff changeset
    17
object Command {
c13e168a8ae6 original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff changeset
    18
  object Phase extends Enumeration {
c13e168a8ae6 original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff changeset
    19
    val UNPROCESSED = Value("UNPROCESSED")
c13e168a8ae6 original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff changeset
    20
    val FINISHED = Value("FINISHED")
c13e168a8ae6 original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff changeset
    21
    val REMOVE = Value("REMOVE")
c13e168a8ae6 original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff changeset
    22
    val REMOVED = Value("REMOVED")
c13e168a8ae6 original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff changeset
    23
    val FAILED = Value("FAILED")
c13e168a8ae6 original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff changeset
    24
  }
c13e168a8ae6 original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff changeset
    25
c13e168a8ae6 original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff changeset
    26
  private var nextId : Long = 0
c13e168a8ae6 original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff changeset
    27
  def generateId : Long = {
c13e168a8ae6 original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff changeset
    28
    nextId = nextId + 1
c13e168a8ae6 original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff changeset
    29
    return nextId
c13e168a8ae6 original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff changeset
    30
  }
c13e168a8ae6 original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff changeset
    31
  
c13e168a8ae6 original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff changeset
    32
  def idFromString(id : String) = Long.unbox(java.lang.Long.valueOf(id, 36))
c13e168a8ae6 original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff changeset
    33
}
c13e168a8ae6 original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff changeset
    34
34397
86daaf5db016 handle statuses in Command
immler@in.tum.de
parents: 34396
diff changeset
    35
class Command(val document : Document, val first : Token[Command], val last : Token[Command]) {
34318
c13e168a8ae6 original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff changeset
    36
  import Command._
c13e168a8ae6 original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff changeset
    37
  
c13e168a8ae6 original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff changeset
    38
  {
c13e168a8ae6 original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff changeset
    39
    var t = first
c13e168a8ae6 original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff changeset
    40
    while(t != null) {
c13e168a8ae6 original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff changeset
    41
      t.command = this
c13e168a8ae6 original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff changeset
    42
      t = if (t == last) null else t.next
c13e168a8ae6 original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff changeset
    43
    }
c13e168a8ae6 original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff changeset
    44
  }
c13e168a8ae6 original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff changeset
    45
  
c13e168a8ae6 original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff changeset
    46
  val id : Long = generateId
34399
5b8b89b7e597 interpretation of STATUS messages in one place, deleting inner syntax
immler@in.tum.de
parents: 34398
diff changeset
    47
5b8b89b7e597 interpretation of STATUS messages in one place, deleting inner syntax
immler@in.tum.de
parents: 34398
diff changeset
    48
  private var p = Phase.UNPROCESSED
5b8b89b7e597 interpretation of STATUS messages in one place, deleting inner syntax
immler@in.tum.de
parents: 34398
diff changeset
    49
  def phase = p
5b8b89b7e597 interpretation of STATUS messages in one place, deleting inner syntax
immler@in.tum.de
parents: 34398
diff changeset
    50
  def phase_=(p_new : Phase.Value) = {
5b8b89b7e597 interpretation of STATUS messages in one place, deleting inner syntax
immler@in.tum.de
parents: 34398
diff changeset
    51
    if(p_new == Phase.UNPROCESSED){
5b8b89b7e597 interpretation of STATUS messages in one place, deleting inner syntax
immler@in.tum.de
parents: 34398
diff changeset
    52
      //delete inner syntax
34401
44241a37b74a structure of markup-tree in scala, keep track of swing-nodes in background
immler@in.tum.de
parents: 34400
diff changeset
    53
      for(child <- root_node.children){
44241a37b74a structure of markup-tree in scala, keep track of swing-nodes in background
immler@in.tum.de
parents: 34400
diff changeset
    54
        child.children = Nil
34399
5b8b89b7e597 interpretation of STATUS messages in one place, deleting inner syntax
immler@in.tum.de
parents: 34398
diff changeset
    55
      }
5b8b89b7e597 interpretation of STATUS messages in one place, deleting inner syntax
immler@in.tum.de
parents: 34398
diff changeset
    56
    }
5b8b89b7e597 interpretation of STATUS messages in one place, deleting inner syntax
immler@in.tum.de
parents: 34398
diff changeset
    57
    p = p_new
5b8b89b7e597 interpretation of STATUS messages in one place, deleting inner syntax
immler@in.tum.de
parents: 34398
diff changeset
    58
  }
34318
c13e168a8ae6 original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff changeset
    59
	
c13e168a8ae6 original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff changeset
    60
  var results = Nil : List[XML.Tree]
34391
7b5f44553aaf ugly fine-grained buffer markup
immler@in.tum.de
parents: 34388
diff changeset
    61
34318
c13e168a8ae6 original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff changeset
    62
  def idString = java.lang.Long.toString(id, 36)
34397
86daaf5db016 handle statuses in Command
immler@in.tum.de
parents: 34396
diff changeset
    63
  def results_xml = XML.document(results match {
34318
c13e168a8ae6 original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff changeset
    64
                                case Nil => XML.Elem("message", List(), List())
c13e168a8ae6 original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff changeset
    65
                                case List(elem) => elem
34391
7b5f44553aaf ugly fine-grained buffer markup
immler@in.tum.de
parents: 34388
diff changeset
    66
                                case _ =>
34318
c13e168a8ae6 original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff changeset
    67
                                  XML.Elem("messages", List(), List(results.first,
c13e168a8ae6 original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff changeset
    68
                                                                    results.last))
c13e168a8ae6 original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff changeset
    69
                              }, "style")
c13e168a8ae6 original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff changeset
    70
  def addResult(tree : XML.Tree) {
c13e168a8ae6 original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff changeset
    71
    results = results ::: List(tree)
c13e168a8ae6 original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff changeset
    72
  }
34393
f0e1608a774f basic tree structure for sidekick
immler@in.tum.de
parents: 34391
diff changeset
    73
  
34400
1b61a92f8675 MarkupNode instead of DefaultMutableTreeNode and RelativeAsset
immler@in.tum.de
parents: 34399
diff changeset
    74
  val root_node = 
1b61a92f8675 MarkupNode instead of DefaultMutableTreeNode and RelativeAsset
immler@in.tum.de
parents: 34399
diff changeset
    75
    new MarkupNode(this, 0, stop - start, idString, "Command", document.getContent(this))
34393
f0e1608a774f basic tree structure for sidekick
immler@in.tum.de
parents: 34391
diff changeset
    76
34400
1b61a92f8675 MarkupNode instead of DefaultMutableTreeNode and RelativeAsset
immler@in.tum.de
parents: 34399
diff changeset
    77
  def node_from(kind : String, begin : Int, end : Int) : MarkupNode = {
1b61a92f8675 MarkupNode instead of DefaultMutableTreeNode and RelativeAsset
immler@in.tum.de
parents: 34399
diff changeset
    78
    val markup_content = /*content.substring(begin, end)*/ ""
1b61a92f8675 MarkupNode instead of DefaultMutableTreeNode and RelativeAsset
immler@in.tum.de
parents: 34399
diff changeset
    79
    new MarkupNode(this, begin, end, idString, kind, markup_content)
34391
7b5f44553aaf ugly fine-grained buffer markup
immler@in.tum.de
parents: 34388
diff changeset
    80
  }
7b5f44553aaf ugly fine-grained buffer markup
immler@in.tum.de
parents: 34388
diff changeset
    81
34397
86daaf5db016 handle statuses in Command
immler@in.tum.de
parents: 34396
diff changeset
    82
  def content = document.getContent(this)
34396
de809360c51d command property: offset relative to start of command
immler@in.tum.de
parents: 34394
diff changeset
    83
34318
c13e168a8ae6 original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff changeset
    84
  def next = if (last.next != null) last.next.command else null
c13e168a8ae6 original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff changeset
    85
  def previous = if (first.previous != null) first.previous.command else null
c13e168a8ae6 original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff changeset
    86
c13e168a8ae6 original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff changeset
    87
  def start = first start
c13e168a8ae6 original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff changeset
    88
  def stop = last stop
c13e168a8ae6 original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff changeset
    89
  
c13e168a8ae6 original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff changeset
    90
  def properStart = start
c13e168a8ae6 original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff changeset
    91
  def properStop = {
c13e168a8ae6 original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff changeset
    92
    var i = last
34388
23b8351ecbbe arbitrary type for tokens
immler@in.tum.de
parents: 34318
diff changeset
    93
    while (i != first && i.kind.equals(Token.Kind.COMMENT))
34318
c13e168a8ae6 original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff changeset
    94
      i = i.previous
c13e168a8ae6 original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff changeset
    95
    i.stop
c13e168a8ae6 original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff changeset
    96
  }  	
c13e168a8ae6 original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff changeset
    97
}