src/Tools/jEdit/src/isabelle_sidekick.scala
author wenzelm
Wed Jun 08 17:42:07 2011 +0200 (2011-06-08)
changeset 43282 5d294220ca43
parent 40792 src/Tools/jEdit/src/jedit/isabelle_sidekick.scala@1d71a45590e4
child 43661 39fdbd814c7f
permissions -rw-r--r--
moved sources -- eliminated Netbeans artifact of jedit package directory;
wenzelm@43282
     1
/*  Title:      Tools/jEdit/src/isabelle_sidekick.scala
wenzelm@36760
     2
    Author:     Fabian Immler, TU Munich
wenzelm@36760
     3
    Author:     Makarius
wenzelm@36760
     4
wenzelm@36760
     5
SideKick parsers for Isabelle proof documents.
wenzelm@36760
     6
*/
immler@34393
     7
wenzelm@34426
     8
package isabelle.jedit
immler@34393
     9
wenzelm@34760
    10
wenzelm@36015
    11
import isabelle._
wenzelm@36015
    12
immler@34475
    13
import scala.collection.Set
immler@34475
    14
import scala.collection.immutable.TreeSet
wenzelm@34417
    15
immler@34393
    16
import javax.swing.tree.DefaultMutableTreeNode
wenzelm@34701
    17
import javax.swing.text.Position
wenzelm@34701
    18
import javax.swing.Icon
wenzelm@34417
    19
wenzelm@34609
    20
import org.gjt.sp.jedit.{Buffer, EditPane, TextUtilities, View}
wenzelm@34417
    21
import errorlist.DefaultErrorSource
wenzelm@34701
    22
import sidekick.{SideKickParser, SideKickParsedData, SideKickCompletion, IAsset}
wenzelm@34701
    23
immler@34393
    24
wenzelm@36738
    25
object Isabelle_Sidekick
wenzelm@36738
    26
{
wenzelm@40477
    27
  def int_to_pos(offset: Text.Offset): Position =
wenzelm@36738
    28
    new Position { def getOffset = offset; override def toString = offset.toString }
wenzelm@40452
    29
wenzelm@40477
    30
  class Asset(name: String, start: Text.Offset, end: Text.Offset) extends IAsset
wenzelm@40452
    31
  {
wenzelm@40452
    32
    protected var _name = name
wenzelm@40452
    33
    protected var _start = int_to_pos(start)
wenzelm@40452
    34
    protected var _end = int_to_pos(end)
wenzelm@40452
    35
    override def getIcon: Icon = null
wenzelm@40452
    36
    override def getShortString: String = _name
wenzelm@40452
    37
    override def getLongString: String = _name
wenzelm@40452
    38
    override def getName: String = _name
wenzelm@40452
    39
    override def setName(name: String) = _name = name
wenzelm@40452
    40
    override def getStart: Position = _start
wenzelm@40452
    41
    override def setStart(start: Position) = _start = start
wenzelm@40452
    42
    override def getEnd: Position = _end
wenzelm@40452
    43
    override def setEnd(end: Position) = _end = end
wenzelm@40452
    44
    override def toString = _name
wenzelm@40452
    45
  }
wenzelm@36738
    46
}
wenzelm@36738
    47
wenzelm@36738
    48
wenzelm@36759
    49
abstract class Isabelle_Sidekick(name: String) extends SideKickParser(name)
wenzelm@34625
    50
{
wenzelm@34417
    51
  /* parsing */
wenzelm@34417
    52
wenzelm@36759
    53
  @volatile protected var stopped = false
wenzelm@34503
    54
  override def stop() = { stopped = true }
immler@34401
    55
wenzelm@36759
    56
  def parser(data: SideKickParsedData, model: Document_Model): Unit
wenzelm@36759
    57
wenzelm@34625
    58
  def parse(buffer: Buffer, error_source: DefaultErrorSource): SideKickParsedData =
wenzelm@34625
    59
  {
wenzelm@34417
    60
    stopped = false
wenzelm@34625
    61
wenzelm@38640
    62
    // FIXME lock buffer (!??)
wenzelm@34417
    63
    val data = new SideKickParsedData(buffer.getName)
wenzelm@34717
    64
    val root = data.root
wenzelm@40452
    65
    data.getAsset(root).setEnd(Isabelle_Sidekick.int_to_pos(buffer.getLength))
immler@34475
    66
wenzelm@34789
    67
    Swing_Thread.now { Document_Model(buffer) } match {
wenzelm@34784
    68
      case Some(model) =>
wenzelm@36759
    69
        parser(data, model)
wenzelm@34777
    70
        if (stopped) root.add(new DefaultMutableTreeNode("<parser stopped>"))
wenzelm@34777
    71
      case None => root.add(new DefaultMutableTreeNode("<buffer inactive>"))
immler@34475
    72
    }
wenzelm@34417
    73
    data
wenzelm@34417
    74
  }
wenzelm@34417
    75
wenzelm@36738
    76
wenzelm@34417
    77
  /* completion */
wenzelm@34417
    78
wenzelm@34417
    79
  override def supportsCompletion = true
wenzelm@34417
    80
  override def canCompleteAnywhere = true
wenzelm@34417
    81
wenzelm@40477
    82
  override def complete(pane: EditPane, caret: Text.Offset): SideKickCompletion =
wenzelm@34609
    83
  {
immler@34475
    84
    val buffer = pane.getBuffer
wenzelm@39624
    85
    Isabelle.swing_buffer_lock(buffer) {
wenzelm@39624
    86
      Document_Model(buffer) match {
wenzelm@39624
    87
        case None => null
wenzelm@39624
    88
        case Some(model) =>
wenzelm@39624
    89
          val line = buffer.getLineOfOffset(caret)
wenzelm@39624
    90
          val start = buffer.getLineStartOffset(line)
wenzelm@39624
    91
          val text = buffer.getSegment(start, caret - start)
immler@34475
    92
wenzelm@39624
    93
          val completion = model.session.current_syntax().completion
wenzelm@39624
    94
          completion.complete(text) match {
wenzelm@39624
    95
            case None => null
wenzelm@39624
    96
            case Some((word, cs)) =>
wenzelm@39624
    97
              val ds =
wenzelm@39624
    98
                (if (Isabelle_Encoding.is_active(buffer))
wenzelm@39624
    99
                  cs.map(Isabelle.system.symbols.decode(_)).sortWith(_ < _)
wenzelm@39624
   100
                 else cs).filter(_ != word)
wenzelm@39624
   101
              if (ds.isEmpty) null
wenzelm@39624
   102
              else new SideKickCompletion(
wenzelm@39624
   103
                pane.getView, word, ds.toArray.asInstanceOf[Array[Object]]) { }
wenzelm@39624
   104
          }
wenzelm@39624
   105
      }
wenzelm@34611
   106
    }
wenzelm@34609
   107
  }
immler@34393
   108
}
wenzelm@36738
   109
wenzelm@36738
   110
wenzelm@36759
   111
class Isabelle_Sidekick_Default extends Isabelle_Sidekick("isabelle")
wenzelm@36759
   112
{
wenzelm@40455
   113
  import Thy_Syntax.Structure
wenzelm@40455
   114
wenzelm@36759
   115
  def parser(data: SideKickParsedData, model: Document_Model)
wenzelm@36759
   116
  {
wenzelm@40455
   117
    val syntax = model.session.current_syntax()
wenzelm@40455
   118
wenzelm@40477
   119
    def make_tree(offset: Text.Offset, entry: Structure.Entry): List[DefaultMutableTreeNode] =
wenzelm@40455
   120
      entry match {
wenzelm@40455
   121
        case Structure.Block(name, body) =>
wenzelm@40455
   122
          val node =
wenzelm@40455
   123
            new DefaultMutableTreeNode(
wenzelm@40475
   124
              new Isabelle_Sidekick.Asset(Library.first_line(name), offset, offset + entry.length))
wenzelm@40455
   125
          (offset /: body)((i, e) =>
wenzelm@40455
   126
            {
wenzelm@40455
   127
              make_tree(i, e) foreach (nd => node.add(nd))
wenzelm@40455
   128
              i + e.length
wenzelm@40455
   129
            })
wenzelm@40455
   130
          List(node)
wenzelm@40455
   131
        case Structure.Atom(command)
wenzelm@40458
   132
        if command.is_command && syntax.heading_level(command).isEmpty =>
wenzelm@40455
   133
          val node =
wenzelm@40455
   134
            new DefaultMutableTreeNode(
wenzelm@40455
   135
              new Isabelle_Sidekick.Asset(command.name, offset, offset + entry.length))
wenzelm@40455
   136
          List(node)
wenzelm@40455
   137
        case _ => Nil
wenzelm@40455
   138
      }
wenzelm@40455
   139
wenzelm@40474
   140
    val text = Isabelle.buffer_text(model.buffer)
wenzelm@40792
   141
    val structure = Structure.parse(syntax, "theory " + model.thy_name, text)
wenzelm@40455
   142
wenzelm@40455
   143
    make_tree(0, structure) foreach (node => data.root.add(node))
wenzelm@36759
   144
  }
wenzelm@36759
   145
}
wenzelm@36738
   146
wenzelm@36738
   147
wenzelm@36759
   148
class Isabelle_Sidekick_Raw extends Isabelle_Sidekick("isabelle-raw")
wenzelm@36759
   149
{
wenzelm@36759
   150
  def parser(data: SideKickParsedData, model: Document_Model)
wenzelm@36759
   151
  {
wenzelm@36759
   152
    val root = data.root
wenzelm@38223
   153
    val snapshot = Swing_Thread.now { model.snapshot() }  // FIXME cover all nodes (!??)
wenzelm@38569
   154
    for ((command, command_start) <- snapshot.node.command_range() if !stopped) {
wenzelm@38658
   155
      snapshot.state(command).root_markup.swing_tree(root)((info: Text.Info[Any]) =>
wenzelm@36759
   156
          {
wenzelm@38663
   157
            val range = info.range + command_start
wenzelm@38577
   158
            val content = command.source(info.range).replace('\n', ' ')
wenzelm@38663
   159
            val info_text =
wenzelm@38663
   160
              info.info match {
wenzelm@38663
   161
                case elem @ XML.Elem(_, _) =>
wenzelm@38663
   162
                  Pretty.formatted(List(elem), margin = 40).mkString("\n")
wenzelm@38663
   163
                case x => x.toString
wenzelm@38663
   164
              }
wenzelm@36738
   165
wenzelm@40452
   166
            new DefaultMutableTreeNode(
wenzelm@40452
   167
              new Isabelle_Sidekick.Asset(command.toString, range.start, range.stop) {
wenzelm@40452
   168
                override def getShortString: String = content
wenzelm@40452
   169
                override def getLongString: String = info_text
wenzelm@40452
   170
                override def toString = "\"" + content + "\" " + range.toString
wenzelm@40452
   171
              })
wenzelm@38479
   172
          })
wenzelm@36759
   173
    }
wenzelm@36759
   174
  }
wenzelm@36759
   175
}
wenzelm@36738
   176