src/Tools/jEdit/src/jedit/isabelle_sidekick.scala
author wenzelm
Tue Dec 08 16:30:20 2009 +0100 (2009-12-08)
changeset 34760 dc7f5e0d9d27
parent 34759 bfea7839d9e1
child 34777 91d6089cef88
permissions -rw-r--r--
misc modernization of names;
immler@34393
     1
/*
wenzelm@34417
     2
 * SideKick parser for Isabelle proof documents
immler@34393
     3
 *
wenzelm@34407
     4
 * @author Fabian Immler, TU Munich
wenzelm@34417
     5
 * @author Makarius
immler@34393
     6
 */
immler@34393
     7
wenzelm@34426
     8
package isabelle.jedit
immler@34393
     9
wenzelm@34760
    10
immler@34475
    11
import scala.collection.Set
immler@34475
    12
import scala.collection.immutable.TreeSet
wenzelm@34417
    13
immler@34393
    14
import javax.swing.tree.DefaultMutableTreeNode
wenzelm@34701
    15
import javax.swing.text.Position
wenzelm@34701
    16
import javax.swing.Icon
wenzelm@34417
    17
wenzelm@34609
    18
import org.gjt.sp.jedit.{Buffer, EditPane, TextUtilities, View}
wenzelm@34417
    19
import errorlist.DefaultErrorSource
wenzelm@34701
    20
import sidekick.{SideKickParser, SideKickParsedData, SideKickCompletion, IAsset}
wenzelm@34701
    21
wenzelm@34760
    22
import isabelle.proofdocument.{Command, Markup_Node, Proof_Document}
wenzelm@34417
    23
immler@34393
    24
wenzelm@34760
    25
class Isabelle_Sidekick extends SideKickParser("isabelle")
wenzelm@34625
    26
{
wenzelm@34417
    27
  /* parsing */
wenzelm@34417
    28
wenzelm@34625
    29
  @volatile private var stopped = false
wenzelm@34503
    30
  override def stop() = { stopped = true }
immler@34401
    31
wenzelm@34625
    32
  def parse(buffer: Buffer, error_source: DefaultErrorSource): SideKickParsedData =
wenzelm@34625
    33
  {
wenzelm@34717
    34
    implicit def int_to_pos(offset: Int): Position =
wenzelm@34717
    35
      new Position { def getOffset = offset; override def toString = offset.toString }
wenzelm@34717
    36
wenzelm@34417
    37
    stopped = false
wenzelm@34625
    38
wenzelm@34417
    39
    val data = new SideKickParsedData(buffer.getName)
wenzelm@34717
    40
    val root = data.root
wenzelm@34717
    41
    data.getAsset(root).setEnd(buffer.getLength)
immler@34475
    42
immler@34669
    43
    val prover_setup = Isabelle.prover_setup(buffer)
wenzelm@34503
    44
    if (prover_setup.isDefined) {
immler@34650
    45
      val document = prover_setup.get.theory_view.current_document()
wenzelm@34701
    46
      for (command <- document.commands if !stopped) {
wenzelm@34717
    47
        root.add(command.markup_root(document).swing_tree((node: Markup_Node) =>
wenzelm@34701
    48
            {
wenzelm@34717
    49
              val content = command.content(node.start, node.stop)
wenzelm@34704
    50
              val command_start = command.start(document)
wenzelm@34705
    51
              val id = command.id
wenzelm@34705
    52
wenzelm@34701
    53
              new DefaultMutableTreeNode(new IAsset {
wenzelm@34701
    54
                override def getIcon: Icon = null
wenzelm@34717
    55
                override def getShortString: String = content
wenzelm@34701
    56
                override def getLongString: String = node.info.toString
wenzelm@34705
    57
                override def getName: String = id
wenzelm@34701
    58
                override def setName(name: String) = ()
wenzelm@34701
    59
                override def setStart(start: Position) = ()
wenzelm@34704
    60
                override def getStart: Position = command_start + node.start
wenzelm@34701
    61
                override def setEnd(end: Position) = ()
wenzelm@34704
    62
                override def getEnd: Position = command_start + node.stop
wenzelm@34717
    63
                override def toString = id + ": " + content + "[" + getStart + " - " + getEnd + "]"
wenzelm@34701
    64
              })
wenzelm@34701
    65
            }))
wenzelm@34701
    66
      }
wenzelm@34717
    67
      if (stopped) root.add(new DefaultMutableTreeNode("<parser stopped>"))
immler@34475
    68
    }
wenzelm@34717
    69
    else root.add(new DefaultMutableTreeNode("<buffer inactive>"))
wenzelm@34417
    70
wenzelm@34417
    71
    data
wenzelm@34417
    72
  }
wenzelm@34417
    73
immler@34393
    74
wenzelm@34417
    75
  /* completion */
wenzelm@34417
    76
wenzelm@34417
    77
  override def supportsCompletion = true
wenzelm@34417
    78
  override def canCompleteAnywhere = true
wenzelm@34417
    79
wenzelm@34609
    80
  override def complete(pane: EditPane, caret: Int): SideKickCompletion =
wenzelm@34609
    81
  {
immler@34475
    82
    val buffer = pane.getBuffer
wenzelm@34612
    83
wenzelm@34612
    84
    val line = buffer.getLineOfOffset(caret)
wenzelm@34612
    85
    val start = buffer.getLineStartOffset(line)
wenzelm@34612
    86
    val text = buffer.getSegment(start, caret - start)
wenzelm@34609
    87
wenzelm@34612
    88
    val completion =
wenzelm@34720
    89
      Isabelle.prover_setup(buffer).map(_.prover.completion()).getOrElse(Isabelle.completion)
immler@34475
    90
wenzelm@34612
    91
    completion.complete(text) match {
wenzelm@34612
    92
      case None => null
wenzelm@34612
    93
      case Some((word, cs)) =>
wenzelm@34625
    94
        val ds =
wenzelm@34738
    95
          if (Isabelle_Encoding.is_active(buffer))
wenzelm@34625
    96
            cs.map(Isabelle.system.symbols.decode(_)).sort(Completion.length_ord _)
wenzelm@34625
    97
          else cs
wenzelm@34625
    98
        new SideKickCompletion(pane.getView, word, ds.toArray.asInstanceOf[Array[Object]]) { }
wenzelm@34611
    99
    }
wenzelm@34609
   100
  }
immler@34475
   101
immler@34393
   102
}