src/Tools/jEdit/src/isabelle_sidekick.scala
changeset 43282 5d294220ca43
parent 40792 1d71a45590e4
child 43661 39fdbd814c7f
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/Tools/jEdit/src/isabelle_sidekick.scala	Wed Jun 08 17:42:07 2011 +0200
     1.3 @@ -0,0 +1,176 @@
     1.4 +/*  Title:      Tools/jEdit/src/isabelle_sidekick.scala
     1.5 +    Author:     Fabian Immler, TU Munich
     1.6 +    Author:     Makarius
     1.7 +
     1.8 +SideKick parsers for Isabelle proof documents.
     1.9 +*/
    1.10 +
    1.11 +package isabelle.jedit
    1.12 +
    1.13 +
    1.14 +import isabelle._
    1.15 +
    1.16 +import scala.collection.Set
    1.17 +import scala.collection.immutable.TreeSet
    1.18 +
    1.19 +import javax.swing.tree.DefaultMutableTreeNode
    1.20 +import javax.swing.text.Position
    1.21 +import javax.swing.Icon
    1.22 +
    1.23 +import org.gjt.sp.jedit.{Buffer, EditPane, TextUtilities, View}
    1.24 +import errorlist.DefaultErrorSource
    1.25 +import sidekick.{SideKickParser, SideKickParsedData, SideKickCompletion, IAsset}
    1.26 +
    1.27 +
    1.28 +object Isabelle_Sidekick
    1.29 +{
    1.30 +  def int_to_pos(offset: Text.Offset): Position =
    1.31 +    new Position { def getOffset = offset; override def toString = offset.toString }
    1.32 +
    1.33 +  class Asset(name: String, start: Text.Offset, end: Text.Offset) extends IAsset
    1.34 +  {
    1.35 +    protected var _name = name
    1.36 +    protected var _start = int_to_pos(start)
    1.37 +    protected var _end = int_to_pos(end)
    1.38 +    override def getIcon: Icon = null
    1.39 +    override def getShortString: String = _name
    1.40 +    override def getLongString: String = _name
    1.41 +    override def getName: String = _name
    1.42 +    override def setName(name: String) = _name = name
    1.43 +    override def getStart: Position = _start
    1.44 +    override def setStart(start: Position) = _start = start
    1.45 +    override def getEnd: Position = _end
    1.46 +    override def setEnd(end: Position) = _end = end
    1.47 +    override def toString = _name
    1.48 +  }
    1.49 +}
    1.50 +
    1.51 +
    1.52 +abstract class Isabelle_Sidekick(name: String) extends SideKickParser(name)
    1.53 +{
    1.54 +  /* parsing */
    1.55 +
    1.56 +  @volatile protected var stopped = false
    1.57 +  override def stop() = { stopped = true }
    1.58 +
    1.59 +  def parser(data: SideKickParsedData, model: Document_Model): Unit
    1.60 +
    1.61 +  def parse(buffer: Buffer, error_source: DefaultErrorSource): SideKickParsedData =
    1.62 +  {
    1.63 +    stopped = false
    1.64 +
    1.65 +    // FIXME lock buffer (!??)
    1.66 +    val data = new SideKickParsedData(buffer.getName)
    1.67 +    val root = data.root
    1.68 +    data.getAsset(root).setEnd(Isabelle_Sidekick.int_to_pos(buffer.getLength))
    1.69 +
    1.70 +    Swing_Thread.now { Document_Model(buffer) } match {
    1.71 +      case Some(model) =>
    1.72 +        parser(data, model)
    1.73 +        if (stopped) root.add(new DefaultMutableTreeNode("<parser stopped>"))
    1.74 +      case None => root.add(new DefaultMutableTreeNode("<buffer inactive>"))
    1.75 +    }
    1.76 +    data
    1.77 +  }
    1.78 +
    1.79 +
    1.80 +  /* completion */
    1.81 +
    1.82 +  override def supportsCompletion = true
    1.83 +  override def canCompleteAnywhere = true
    1.84 +
    1.85 +  override def complete(pane: EditPane, caret: Text.Offset): SideKickCompletion =
    1.86 +  {
    1.87 +    val buffer = pane.getBuffer
    1.88 +    Isabelle.swing_buffer_lock(buffer) {
    1.89 +      Document_Model(buffer) match {
    1.90 +        case None => null
    1.91 +        case Some(model) =>
    1.92 +          val line = buffer.getLineOfOffset(caret)
    1.93 +          val start = buffer.getLineStartOffset(line)
    1.94 +          val text = buffer.getSegment(start, caret - start)
    1.95 +
    1.96 +          val completion = model.session.current_syntax().completion
    1.97 +          completion.complete(text) match {
    1.98 +            case None => null
    1.99 +            case Some((word, cs)) =>
   1.100 +              val ds =
   1.101 +                (if (Isabelle_Encoding.is_active(buffer))
   1.102 +                  cs.map(Isabelle.system.symbols.decode(_)).sortWith(_ < _)
   1.103 +                 else cs).filter(_ != word)
   1.104 +              if (ds.isEmpty) null
   1.105 +              else new SideKickCompletion(
   1.106 +                pane.getView, word, ds.toArray.asInstanceOf[Array[Object]]) { }
   1.107 +          }
   1.108 +      }
   1.109 +    }
   1.110 +  }
   1.111 +}
   1.112 +
   1.113 +
   1.114 +class Isabelle_Sidekick_Default extends Isabelle_Sidekick("isabelle")
   1.115 +{
   1.116 +  import Thy_Syntax.Structure
   1.117 +
   1.118 +  def parser(data: SideKickParsedData, model: Document_Model)
   1.119 +  {
   1.120 +    val syntax = model.session.current_syntax()
   1.121 +
   1.122 +    def make_tree(offset: Text.Offset, entry: Structure.Entry): List[DefaultMutableTreeNode] =
   1.123 +      entry match {
   1.124 +        case Structure.Block(name, body) =>
   1.125 +          val node =
   1.126 +            new DefaultMutableTreeNode(
   1.127 +              new Isabelle_Sidekick.Asset(Library.first_line(name), offset, offset + entry.length))
   1.128 +          (offset /: body)((i, e) =>
   1.129 +            {
   1.130 +              make_tree(i, e) foreach (nd => node.add(nd))
   1.131 +              i + e.length
   1.132 +            })
   1.133 +          List(node)
   1.134 +        case Structure.Atom(command)
   1.135 +        if command.is_command && syntax.heading_level(command).isEmpty =>
   1.136 +          val node =
   1.137 +            new DefaultMutableTreeNode(
   1.138 +              new Isabelle_Sidekick.Asset(command.name, offset, offset + entry.length))
   1.139 +          List(node)
   1.140 +        case _ => Nil
   1.141 +      }
   1.142 +
   1.143 +    val text = Isabelle.buffer_text(model.buffer)
   1.144 +    val structure = Structure.parse(syntax, "theory " + model.thy_name, text)
   1.145 +
   1.146 +    make_tree(0, structure) foreach (node => data.root.add(node))
   1.147 +  }
   1.148 +}
   1.149 +
   1.150 +
   1.151 +class Isabelle_Sidekick_Raw extends Isabelle_Sidekick("isabelle-raw")
   1.152 +{
   1.153 +  def parser(data: SideKickParsedData, model: Document_Model)
   1.154 +  {
   1.155 +    val root = data.root
   1.156 +    val snapshot = Swing_Thread.now { model.snapshot() }  // FIXME cover all nodes (!??)
   1.157 +    for ((command, command_start) <- snapshot.node.command_range() if !stopped) {
   1.158 +      snapshot.state(command).root_markup.swing_tree(root)((info: Text.Info[Any]) =>
   1.159 +          {
   1.160 +            val range = info.range + command_start
   1.161 +            val content = command.source(info.range).replace('\n', ' ')
   1.162 +            val info_text =
   1.163 +              info.info match {
   1.164 +                case elem @ XML.Elem(_, _) =>
   1.165 +                  Pretty.formatted(List(elem), margin = 40).mkString("\n")
   1.166 +                case x => x.toString
   1.167 +              }
   1.168 +
   1.169 +            new DefaultMutableTreeNode(
   1.170 +              new Isabelle_Sidekick.Asset(command.toString, range.start, range.stop) {
   1.171 +                override def getShortString: String = content
   1.172 +                override def getLongString: String = info_text
   1.173 +                override def toString = "\"" + content + "\" " + range.toString
   1.174 +              })
   1.175 +          })
   1.176 +    }
   1.177 +  }
   1.178 +}
   1.179 +