src/Tools/jEdit/src/jedit/isabelle_sidekick.scala
author wenzelm
Sun Aug 15 22:48:56 2010 +0200 (2010-08-15)
changeset 38426 2858ec7b6dd8
parent 38417 b8922ae21111
child 38479 e628da370072
permissions -rw-r--r--
specific types Text.Offset and Text.Range;
minor tuning;
wenzelm@36760
     1
/*  Title:      Tools/jEdit/src/jedit/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@36738
    27
  implicit def int_to_pos(offset: Int): Position =
wenzelm@36738
    28
    new Position { def getOffset = offset; override def toString = offset.toString }
wenzelm@36738
    29
}
wenzelm@36738
    30
wenzelm@36738
    31
wenzelm@36759
    32
abstract class Isabelle_Sidekick(name: String) extends SideKickParser(name)
wenzelm@34625
    33
{
wenzelm@34417
    34
  /* parsing */
wenzelm@34417
    35
wenzelm@36759
    36
  @volatile protected var stopped = false
wenzelm@34503
    37
  override def stop() = { stopped = true }
immler@34401
    38
wenzelm@36759
    39
  def parser(data: SideKickParsedData, model: Document_Model): Unit
wenzelm@36759
    40
wenzelm@34625
    41
  def parse(buffer: Buffer, error_source: DefaultErrorSource): SideKickParsedData =
wenzelm@34625
    42
  {
wenzelm@36738
    43
    import Isabelle_Sidekick.int_to_pos
wenzelm@34717
    44
wenzelm@34417
    45
    stopped = false
wenzelm@34625
    46
wenzelm@34789
    47
    // FIXME lock buffer !??
wenzelm@34417
    48
    val data = new SideKickParsedData(buffer.getName)
wenzelm@34717
    49
    val root = data.root
wenzelm@34717
    50
    data.getAsset(root).setEnd(buffer.getLength)
immler@34475
    51
wenzelm@34789
    52
    Swing_Thread.now { Document_Model(buffer) } match {
wenzelm@34784
    53
      case Some(model) =>
wenzelm@36759
    54
        parser(data, model)
wenzelm@34777
    55
        if (stopped) root.add(new DefaultMutableTreeNode("<parser stopped>"))
wenzelm@34777
    56
      case None => root.add(new DefaultMutableTreeNode("<buffer inactive>"))
immler@34475
    57
    }
wenzelm@34417
    58
    data
wenzelm@34417
    59
  }
wenzelm@34417
    60
wenzelm@36738
    61
wenzelm@34417
    62
  /* completion */
wenzelm@34417
    63
wenzelm@34417
    64
  override def supportsCompletion = true
wenzelm@34417
    65
  override def canCompleteAnywhere = true
wenzelm@34417
    66
wenzelm@34609
    67
  override def complete(pane: EditPane, caret: Int): SideKickCompletion =
wenzelm@34609
    68
  {
immler@34475
    69
    val buffer = pane.getBuffer
wenzelm@34612
    70
wenzelm@34612
    71
    val line = buffer.getLineOfOffset(caret)
wenzelm@34612
    72
    val start = buffer.getLineStartOffset(line)
wenzelm@34612
    73
    val text = buffer.getSegment(start, caret - start)
wenzelm@34609
    74
wenzelm@34819
    75
    val completion = Isabelle.session.current_syntax.completion
immler@34475
    76
wenzelm@34612
    77
    completion.complete(text) match {
wenzelm@34612
    78
      case None => null
wenzelm@34612
    79
      case Some((word, cs)) =>
wenzelm@34625
    80
        val ds =
wenzelm@35004
    81
          (if (Isabelle_Encoding.is_active(buffer))
wenzelm@34796
    82
            cs.map(Isabelle.system.symbols.decode(_)).sort(_ < _)
wenzelm@35004
    83
           else cs).filter(_ != word)
wenzelm@35004
    84
        if (ds.isEmpty) null
wenzelm@35004
    85
        else new SideKickCompletion(pane.getView, word, ds.toArray.asInstanceOf[Array[Object]]) { }
wenzelm@34611
    86
    }
wenzelm@34609
    87
  }
immler@34393
    88
}
wenzelm@36738
    89
wenzelm@36738
    90
wenzelm@36759
    91
class Isabelle_Sidekick_Default extends Isabelle_Sidekick("isabelle")
wenzelm@36759
    92
{
wenzelm@36759
    93
  def parser(data: SideKickParsedData, model: Document_Model)
wenzelm@36759
    94
  {
wenzelm@36759
    95
    import Isabelle_Sidekick.int_to_pos
wenzelm@36738
    96
wenzelm@36759
    97
    val root = data.root
wenzelm@38417
    98
    val snapshot = Swing_Thread.now { model.snapshot() }  // FIXME cover all nodes (!??)
wenzelm@36759
    99
    for {
wenzelm@38417
   100
      (command, command_start) <- snapshot.node.command_range(0)
wenzelm@36762
   101
      if command.is_command && !stopped
wenzelm@36759
   102
    }
wenzelm@36759
   103
    {
wenzelm@36759
   104
      val name = command.name
wenzelm@36759
   105
      val node =
wenzelm@36759
   106
        new DefaultMutableTreeNode(new IAsset {
wenzelm@36759
   107
          override def getIcon: Icon = null
wenzelm@36759
   108
          override def getShortString: String = name
wenzelm@36759
   109
          override def getLongString: String = name
wenzelm@36759
   110
          override def getName: String = name
wenzelm@36759
   111
          override def setName(name: String) = ()
wenzelm@36759
   112
          override def setStart(start: Position) = ()
wenzelm@36759
   113
          override def getStart: Position = command_start
wenzelm@36759
   114
          override def setEnd(end: Position) = ()
wenzelm@36759
   115
          override def getEnd: Position = command_start + command.length
wenzelm@38417
   116
          override def toString = name})
wenzelm@36759
   117
      root.add(node)
wenzelm@36759
   118
    }
wenzelm@36759
   119
  }
wenzelm@36759
   120
}
wenzelm@36738
   121
wenzelm@36738
   122
wenzelm@36759
   123
class Isabelle_Sidekick_Raw extends Isabelle_Sidekick("isabelle-raw")
wenzelm@36759
   124
{
wenzelm@36759
   125
  def parser(data: SideKickParsedData, model: Document_Model)
wenzelm@36759
   126
  {
wenzelm@36759
   127
    import Isabelle_Sidekick.int_to_pos
wenzelm@36738
   128
wenzelm@36759
   129
    val root = data.root
wenzelm@38223
   130
    val snapshot = Swing_Thread.now { model.snapshot() }  // FIXME cover all nodes (!??)
wenzelm@38152
   131
    for ((command, command_start) <- snapshot.node.command_range(0) if !stopped) {
wenzelm@38362
   132
      root.add(snapshot.state(command).markup.swing_tree((node: Markup_Node) =>
wenzelm@36759
   133
          {
wenzelm@38426
   134
            val content = command.source(node.range).replace('\n', ' ')
wenzelm@36759
   135
            val id = command.id
wenzelm@36738
   136
wenzelm@36759
   137
            new DefaultMutableTreeNode(new IAsset {
wenzelm@36759
   138
              override def getIcon: Icon = null
wenzelm@36759
   139
              override def getShortString: String = content
wenzelm@36759
   140
              override def getLongString: String = node.info.toString
wenzelm@38414
   141
              override def getName: String = Markup.Long(id)
wenzelm@36759
   142
              override def setName(name: String) = ()
wenzelm@36759
   143
              override def setStart(start: Position) = ()
wenzelm@38426
   144
              override def getStart: Position = command_start + node.range.start
wenzelm@36759
   145
              override def setEnd(end: Position) = ()
wenzelm@38426
   146
              override def getEnd: Position = command_start + node.range.stop
wenzelm@36759
   147
              override def toString = id + ": " + content + "[" + getStart + " - " + getEnd + "]"
wenzelm@36759
   148
            })
wenzelm@36759
   149
          }))
wenzelm@36759
   150
    }
wenzelm@36759
   151
  }
wenzelm@36759
   152
}
wenzelm@36738
   153