src/Tools/jEdit/src/prover/Command.scala
author wenzelm
Fri, 16 Jan 2009 22:57:24 +0100
changeset 34476 e2b1fb731241
parent 34458 e2aa32bb73c0
child 34481 660c639870a4
permissions -rw-r--r--
tuned import;
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
34451
3b9d0074ed44 command id via Isabelle.plugin;
wenzelm
parents: 34410
diff changeset
    10
34393
f0e1608a774f basic tree structure for sidekick
immler@in.tum.de
parents: 34391
diff changeset
    11
import javax.swing.text.Position
f0e1608a774f basic tree structure for sidekick
immler@in.tum.de
parents: 34391
diff changeset
    12
import javax.swing.tree.DefaultMutableTreeNode
34318
c13e168a8ae6 original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff changeset
    13
34451
3b9d0074ed44 command id via Isabelle.plugin;
wenzelm
parents: 34410
diff changeset
    14
import isabelle.proofdocument.Token
3b9d0074ed44 command id via Isabelle.plugin;
wenzelm
parents: 34410
diff changeset
    15
import isabelle.jedit.{Isabelle, Plugin}
34476
e2b1fb731241 tuned import;
wenzelm
parents: 34458
diff changeset
    16
import isabelle.XML
34451
3b9d0074ed44 command id via Isabelle.plugin;
wenzelm
parents: 34410
diff changeset
    17
3b9d0074ed44 command id via Isabelle.plugin;
wenzelm
parents: 34410
diff changeset
    18
import sidekick.{SideKickParsedData, IAsset}
3b9d0074ed44 command id via Isabelle.plugin;
wenzelm
parents: 34410
diff changeset
    19
3b9d0074ed44 command id via Isabelle.plugin;
wenzelm
parents: 34410
diff changeset
    20
34318
c13e168a8ae6 original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff changeset
    21
object Command {
34458
e2aa32bb73c0 - renamed Command.Phase to Command.Status (cf. src/Pure/Isar/isar.ML);
wenzelm
parents: 34451
diff changeset
    22
  object Status extends Enumeration {
34318
c13e168a8ae6 original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff changeset
    23
    val UNPROCESSED = Value("UNPROCESSED")
c13e168a8ae6 original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff changeset
    24
    val FINISHED = Value("FINISHED")
c13e168a8ae6 original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff changeset
    25
    val REMOVE = Value("REMOVE")
c13e168a8ae6 original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff changeset
    26
    val REMOVED = Value("REMOVED")
c13e168a8ae6 original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff changeset
    27
    val FAILED = Value("FAILED")
c13e168a8ae6 original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff changeset
    28
  }
c13e168a8ae6 original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff changeset
    29
}
c13e168a8ae6 original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff changeset
    30
34451
3b9d0074ed44 command id via Isabelle.plugin;
wenzelm
parents: 34410
diff changeset
    31
3b9d0074ed44 command id via Isabelle.plugin;
wenzelm
parents: 34410
diff changeset
    32
class Command(val document: Document, val first: Token[Command], val last: Token[Command])
3b9d0074ed44 command id via Isabelle.plugin;
wenzelm
parents: 34410
diff changeset
    33
{
3b9d0074ed44 command id via Isabelle.plugin;
wenzelm
parents: 34410
diff changeset
    34
  val id = Isabelle.plugin.id()
34318
c13e168a8ae6 original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff changeset
    35
  
c13e168a8ae6 original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff changeset
    36
  {
c13e168a8ae6 original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff changeset
    37
    var t = first
34451
3b9d0074ed44 command id via Isabelle.plugin;
wenzelm
parents: 34410
diff changeset
    38
    while (t != null) {
34318
c13e168a8ae6 original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff changeset
    39
      t.command = this
c13e168a8ae6 original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff changeset
    40
      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
    41
    }
c13e168a8ae6 original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff changeset
    42
  }
34451
3b9d0074ed44 command id via Isabelle.plugin;
wenzelm
parents: 34410
diff changeset
    43
34399
5b8b89b7e597 interpretation of STATUS messages in one place, deleting inner syntax
immler@in.tum.de
parents: 34398
diff changeset
    44
34458
e2aa32bb73c0 - renamed Command.Phase to Command.Status (cf. src/Pure/Isar/isar.ML);
wenzelm
parents: 34451
diff changeset
    45
  /* command status */
34451
3b9d0074ed44 command id via Isabelle.plugin;
wenzelm
parents: 34410
diff changeset
    46
34458
e2aa32bb73c0 - renamed Command.Phase to Command.Status (cf. src/Pure/Isar/isar.ML);
wenzelm
parents: 34451
diff changeset
    47
  private var _status = Command.Status.UNPROCESSED
e2aa32bb73c0 - renamed Command.Phase to Command.Status (cf. src/Pure/Isar/isar.ML);
wenzelm
parents: 34451
diff changeset
    48
  def status = _status
e2aa32bb73c0 - renamed Command.Phase to Command.Status (cf. src/Pure/Isar/isar.ML);
wenzelm
parents: 34451
diff changeset
    49
  def status_=(st: Command.Status.Value) = {
e2aa32bb73c0 - renamed Command.Phase to Command.Status (cf. src/Pure/Isar/isar.ML);
wenzelm
parents: 34451
diff changeset
    50
    if (st == Command.Status.UNPROCESSED) {
34451
3b9d0074ed44 command id via Isabelle.plugin;
wenzelm
parents: 34410
diff changeset
    51
      // delete markup
3b9d0074ed44 command id via Isabelle.plugin;
wenzelm
parents: 34410
diff changeset
    52
      for (child <- root_node.children) {
34401
44241a37b74a structure of markup-tree in scala, keep track of swing-nodes in background
immler@in.tum.de
parents: 34400
diff changeset
    53
        child.children = Nil
34399
5b8b89b7e597 interpretation of STATUS messages in one place, deleting inner syntax
immler@in.tum.de
parents: 34398
diff changeset
    54
      }
5b8b89b7e597 interpretation of STATUS messages in one place, deleting inner syntax
immler@in.tum.de
parents: 34398
diff changeset
    55
    }
34458
e2aa32bb73c0 - renamed Command.Phase to Command.Status (cf. src/Pure/Isar/isar.ML);
wenzelm
parents: 34451
diff changeset
    56
    _status = st
34399
5b8b89b7e597 interpretation of STATUS messages in one place, deleting inner syntax
immler@in.tum.de
parents: 34398
diff changeset
    57
  }
34451
3b9d0074ed44 command id via Isabelle.plugin;
wenzelm
parents: 34410
diff changeset
    58
34391
7b5f44553aaf ugly fine-grained buffer markup
immler@in.tum.de
parents: 34388
diff changeset
    59
34451
3b9d0074ed44 command id via Isabelle.plugin;
wenzelm
parents: 34410
diff changeset
    60
  /* accumulated results */
3b9d0074ed44 command id via Isabelle.plugin;
wenzelm
parents: 34410
diff changeset
    61
3b9d0074ed44 command id via Isabelle.plugin;
wenzelm
parents: 34410
diff changeset
    62
  var results: List[XML.Tree] = Nil
3b9d0074ed44 command id via Isabelle.plugin;
wenzelm
parents: 34410
diff changeset
    63
34410
f2644d2a3e8e misc tuning;
wenzelm
parents: 34407
diff changeset
    64
  def results_xml = XML.document(
f2644d2a3e8e misc tuning;
wenzelm
parents: 34407
diff changeset
    65
    results match {
f2644d2a3e8e misc tuning;
wenzelm
parents: 34407
diff changeset
    66
      case Nil => XML.Elem("message", Nil, Nil)
f2644d2a3e8e misc tuning;
wenzelm
parents: 34407
diff changeset
    67
      case List(elem) => elem
34451
3b9d0074ed44 command id via Isabelle.plugin;
wenzelm
parents: 34410
diff changeset
    68
      case _ => XML.Elem("messages", Nil, List(results.first, results.last))
34410
f2644d2a3e8e misc tuning;
wenzelm
parents: 34407
diff changeset
    69
    }, "style")
34451
3b9d0074ed44 command id via Isabelle.plugin;
wenzelm
parents: 34410
diff changeset
    70
  def add_result(tree: XML.Tree) {
34410
f2644d2a3e8e misc tuning;
wenzelm
parents: 34407
diff changeset
    71
    results = results ::: List(tree)    // FIXME canonical reverse order
34318
c13e168a8ae6 original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff changeset
    72
  }
34451
3b9d0074ed44 command id via Isabelle.plugin;
wenzelm
parents: 34410
diff changeset
    73
34393
f0e1608a774f basic tree structure for sidekick
immler@in.tum.de
parents: 34391
diff changeset
    74
34451
3b9d0074ed44 command id via Isabelle.plugin;
wenzelm
parents: 34410
diff changeset
    75
  /* content */
34391
7b5f44553aaf ugly fine-grained buffer markup
immler@in.tum.de
parents: 34388
diff changeset
    76
34451
3b9d0074ed44 command id via Isabelle.plugin;
wenzelm
parents: 34410
diff changeset
    77
  def content(): String = document.getContent(this)
34396
de809360c51d command property: offset relative to start of command
immler@in.tum.de
parents: 34394
diff changeset
    78
34318
c13e168a8ae6 original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff changeset
    79
  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
    80
  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
    81
34451
3b9d0074ed44 command id via Isabelle.plugin;
wenzelm
parents: 34410
diff changeset
    82
  def start = first.start
3b9d0074ed44 command id via Isabelle.plugin;
wenzelm
parents: 34410
diff changeset
    83
  def stop = last.stop
3b9d0074ed44 command id via Isabelle.plugin;
wenzelm
parents: 34410
diff changeset
    84
3b9d0074ed44 command id via Isabelle.plugin;
wenzelm
parents: 34410
diff changeset
    85
  def proper_start = start
3b9d0074ed44 command id via Isabelle.plugin;
wenzelm
parents: 34410
diff changeset
    86
  def proper_stop = {
34318
c13e168a8ae6 original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff changeset
    87
    var i = last
34388
23b8351ecbbe arbitrary type for tokens
immler@in.tum.de
parents: 34318
diff changeset
    88
    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
    89
      i = i.previous
c13e168a8ae6 original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff changeset
    90
    i.stop
34451
3b9d0074ed44 command id via Isabelle.plugin;
wenzelm
parents: 34410
diff changeset
    91
  }
3b9d0074ed44 command id via Isabelle.plugin;
wenzelm
parents: 34410
diff changeset
    92
3b9d0074ed44 command id via Isabelle.plugin;
wenzelm
parents: 34410
diff changeset
    93
3b9d0074ed44 command id via Isabelle.plugin;
wenzelm
parents: 34410
diff changeset
    94
  /* markup tree */
3b9d0074ed44 command id via Isabelle.plugin;
wenzelm
parents: 34410
diff changeset
    95
3b9d0074ed44 command id via Isabelle.plugin;
wenzelm
parents: 34410
diff changeset
    96
  val root_node =
3b9d0074ed44 command id via Isabelle.plugin;
wenzelm
parents: 34410
diff changeset
    97
    new MarkupNode(this, 0, stop - start, id, Markup.COMMAND_SPAN, content())
3b9d0074ed44 command id via Isabelle.plugin;
wenzelm
parents: 34410
diff changeset
    98
3b9d0074ed44 command id via Isabelle.plugin;
wenzelm
parents: 34410
diff changeset
    99
  def node_from(kind: String, begin: Int, end: Int) = {
3b9d0074ed44 command id via Isabelle.plugin;
wenzelm
parents: 34410
diff changeset
   100
    val markup_content = /*content.substring(begin, end)*/ ""
3b9d0074ed44 command id via Isabelle.plugin;
wenzelm
parents: 34410
diff changeset
   101
    new MarkupNode(this, begin, end, id, kind, markup_content)
3b9d0074ed44 command id via Isabelle.plugin;
wenzelm
parents: 34410
diff changeset
   102
  }
3b9d0074ed44 command id via Isabelle.plugin;
wenzelm
parents: 34410
diff changeset
   103
}