src/Tools/jEdit/src/prover/IsabelleSKParser.scala
author wenzelm
Sat, 20 Dec 2008 14:19:12 +0100
changeset 34417 bce2f2ea9819
parent 34408 ad7b6c4813c8
permissions -rw-r--r--
misc tuning and adaption according to original IsabelleParser -- cf. http://isabelle.in.tum.de/repos/isabelle/file/b1c6f4563df7/lib/jedit/plugin/isabelle_parser.scala;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
34393
f0e1608a774f basic tree structure for sidekick
immler@in.tum.de
parents:
diff changeset
     1
/*
34417
bce2f2ea9819 misc tuning and adaption according to original IsabelleParser --
wenzelm
parents: 34408
diff changeset
     2
 * SideKick parser for Isabelle proof documents
34393
f0e1608a774f basic tree structure for sidekick
immler@in.tum.de
parents:
diff changeset
     3
 *
34407
aad6834ba380 added some headers and comments;
wenzelm
parents: 34406
diff changeset
     4
 * @author Fabian Immler, TU Munich
34417
bce2f2ea9819 misc tuning and adaption according to original IsabelleParser --
wenzelm
parents: 34408
diff changeset
     5
 * @author Makarius
bce2f2ea9819 misc tuning and adaption according to original IsabelleParser --
wenzelm
parents: 34408
diff changeset
     6
 *
bce2f2ea9819 misc tuning and adaption according to original IsabelleParser --
wenzelm
parents: 34408
diff changeset
     7
 * TODO:
bce2f2ea9819 misc tuning and adaption according to original IsabelleParser --
wenzelm
parents: 34408
diff changeset
     8
 *   - locking of buffer and/or document model (!?)
bce2f2ea9819 misc tuning and adaption according to original IsabelleParser --
wenzelm
parents: 34408
diff changeset
     9
 *   - check treatment of assets
bce2f2ea9819 misc tuning and adaption according to original IsabelleParser --
wenzelm
parents: 34408
diff changeset
    10
 *   - completion support
bce2f2ea9819 misc tuning and adaption according to original IsabelleParser --
wenzelm
parents: 34408
diff changeset
    11
 *   - rename to isabelle.jedit.IsabelleSideKickParser
34393
f0e1608a774f basic tree structure for sidekick
immler@in.tum.de
parents:
diff changeset
    12
 */
f0e1608a774f basic tree structure for sidekick
immler@in.tum.de
parents:
diff changeset
    13
f0e1608a774f basic tree structure for sidekick
immler@in.tum.de
parents:
diff changeset
    14
package isabelle.prover
f0e1608a774f basic tree structure for sidekick
immler@in.tum.de
parents:
diff changeset
    15
34417
bce2f2ea9819 misc tuning and adaption according to original IsabelleParser --
wenzelm
parents: 34408
diff changeset
    16
34393
f0e1608a774f basic tree structure for sidekick
immler@in.tum.de
parents:
diff changeset
    17
import javax.swing.tree.DefaultMutableTreeNode
34417
bce2f2ea9819 misc tuning and adaption according to original IsabelleParser --
wenzelm
parents: 34408
diff changeset
    18
bce2f2ea9819 misc tuning and adaption according to original IsabelleParser --
wenzelm
parents: 34408
diff changeset
    19
import isabelle.jedit.Plugin
bce2f2ea9819 misc tuning and adaption according to original IsabelleParser --
wenzelm
parents: 34408
diff changeset
    20
bce2f2ea9819 misc tuning and adaption according to original IsabelleParser --
wenzelm
parents: 34408
diff changeset
    21
import org.gjt.sp.jedit.{Buffer, EditPane}
bce2f2ea9819 misc tuning and adaption according to original IsabelleParser --
wenzelm
parents: 34408
diff changeset
    22
import errorlist.DefaultErrorSource
bce2f2ea9819 misc tuning and adaption according to original IsabelleParser --
wenzelm
parents: 34408
diff changeset
    23
import sidekick.{SideKickParser, SideKickParsedData, SideKickCompletion}
bce2f2ea9819 misc tuning and adaption according to original IsabelleParser --
wenzelm
parents: 34408
diff changeset
    24
34393
f0e1608a774f basic tree structure for sidekick
immler@in.tum.de
parents:
diff changeset
    25
34406
f81cd75ae331 restructured: independent provers in different buffers
immler@in.tum.de
parents: 34401
diff changeset
    26
class IsabelleSKParser extends SideKickParser("isabelle") {
34417
bce2f2ea9819 misc tuning and adaption according to original IsabelleParser --
wenzelm
parents: 34408
diff changeset
    27
bce2f2ea9819 misc tuning and adaption according to original IsabelleParser --
wenzelm
parents: 34408
diff changeset
    28
  /* parsing */
bce2f2ea9819 misc tuning and adaption according to original IsabelleParser --
wenzelm
parents: 34408
diff changeset
    29
bce2f2ea9819 misc tuning and adaption according to original IsabelleParser --
wenzelm
parents: 34408
diff changeset
    30
  private var stopped = false
bce2f2ea9819 misc tuning and adaption according to original IsabelleParser --
wenzelm
parents: 34408
diff changeset
    31
  override def stop () = { stopped = true }
34401
44241a37b74a structure of markup-tree in scala, keep track of swing-nodes in background
immler@in.tum.de
parents: 34393
diff changeset
    32
34417
bce2f2ea9819 misc tuning and adaption according to original IsabelleParser --
wenzelm
parents: 34408
diff changeset
    33
  def parse(buffer : Buffer, error_source : DefaultErrorSource): SideKickParsedData = {
bce2f2ea9819 misc tuning and adaption according to original IsabelleParser --
wenzelm
parents: 34408
diff changeset
    34
    stopped = false
bce2f2ea9819 misc tuning and adaption according to original IsabelleParser --
wenzelm
parents: 34408
diff changeset
    35
    
bce2f2ea9819 misc tuning and adaption according to original IsabelleParser --
wenzelm
parents: 34408
diff changeset
    36
    val data = new SideKickParsedData(buffer.getName)
bce2f2ea9819 misc tuning and adaption according to original IsabelleParser --
wenzelm
parents: 34408
diff changeset
    37
    
bce2f2ea9819 misc tuning and adaption according to original IsabelleParser --
wenzelm
parents: 34408
diff changeset
    38
    Plugin.plugin.prover_setup(buffer) match {
bce2f2ea9819 misc tuning and adaption according to original IsabelleParser --
wenzelm
parents: 34408
diff changeset
    39
      case None =>
bce2f2ea9819 misc tuning and adaption according to original IsabelleParser --
wenzelm
parents: 34408
diff changeset
    40
        data.root.add(new DefaultMutableTreeNode("<buffer inactive>"))
bce2f2ea9819 misc tuning and adaption according to original IsabelleParser --
wenzelm
parents: 34408
diff changeset
    41
      case Some(prover_setup) =>
bce2f2ea9819 misc tuning and adaption according to original IsabelleParser --
wenzelm
parents: 34408
diff changeset
    42
        val document = prover_setup.prover.document
bce2f2ea9819 misc tuning and adaption according to original IsabelleParser --
wenzelm
parents: 34408
diff changeset
    43
        val commands = document.commands()
bce2f2ea9819 misc tuning and adaption according to original IsabelleParser --
wenzelm
parents: 34408
diff changeset
    44
        while (!stopped && commands.hasNext) {
bce2f2ea9819 misc tuning and adaption according to original IsabelleParser --
wenzelm
parents: 34408
diff changeset
    45
          data.root.add(commands.next.root_node.swing_node)
bce2f2ea9819 misc tuning and adaption according to original IsabelleParser --
wenzelm
parents: 34408
diff changeset
    46
        }
bce2f2ea9819 misc tuning and adaption according to original IsabelleParser --
wenzelm
parents: 34408
diff changeset
    47
        if (stopped) data.root.add(new DefaultMutableTreeNode("<parser stopped>"))
34393
f0e1608a774f basic tree structure for sidekick
immler@in.tum.de
parents:
diff changeset
    48
      }
34417
bce2f2ea9819 misc tuning and adaption according to original IsabelleParser --
wenzelm
parents: 34408
diff changeset
    49
bce2f2ea9819 misc tuning and adaption according to original IsabelleParser --
wenzelm
parents: 34408
diff changeset
    50
    data
bce2f2ea9819 misc tuning and adaption according to original IsabelleParser --
wenzelm
parents: 34408
diff changeset
    51
  }
bce2f2ea9819 misc tuning and adaption according to original IsabelleParser --
wenzelm
parents: 34408
diff changeset
    52
34393
f0e1608a774f basic tree structure for sidekick
immler@in.tum.de
parents:
diff changeset
    53
34417
bce2f2ea9819 misc tuning and adaption according to original IsabelleParser --
wenzelm
parents: 34408
diff changeset
    54
  /* completion */
bce2f2ea9819 misc tuning and adaption according to original IsabelleParser --
wenzelm
parents: 34408
diff changeset
    55
bce2f2ea9819 misc tuning and adaption according to original IsabelleParser --
wenzelm
parents: 34408
diff changeset
    56
  override def supportsCompletion = true
bce2f2ea9819 misc tuning and adaption according to original IsabelleParser --
wenzelm
parents: 34408
diff changeset
    57
  override def canCompleteAnywhere = true
bce2f2ea9819 misc tuning and adaption according to original IsabelleParser --
wenzelm
parents: 34408
diff changeset
    58
bce2f2ea9819 misc tuning and adaption according to original IsabelleParser --
wenzelm
parents: 34408
diff changeset
    59
  override def complete(pane: EditPane, caret: Int): SideKickCompletion = null
34393
f0e1608a774f basic tree structure for sidekick
immler@in.tum.de
parents:
diff changeset
    60
}