src/Tools/jEdit/src/isabelle_sidekick.scala
author wenzelm
Sun Oct 05 18:14:26 2014 +0200 (2014-10-05 ago)
changeset 58546 72e2b2a609c4
parent 58542 19e062fbfea0
child 58706 70a947611792
permissions -rw-r--r--
clarified modules;
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@34393
    13
import javax.swing.tree.DefaultMutableTreeNode
wenzelm@34701
    14
import javax.swing.text.Position
wenzelm@53274
    15
import javax.swing.Icon
wenzelm@34417
    16
wenzelm@53274
    17
import org.gjt.sp.jedit.Buffer
wenzelm@53274
    18
import sidekick.{SideKickParser, SideKickParsedData, IAsset}
wenzelm@34701
    19
immler@34393
    20
wenzelm@36738
    21
object Isabelle_Sidekick
wenzelm@36738
    22
{
wenzelm@40477
    23
  def int_to_pos(offset: Text.Offset): Position =
wenzelm@57912
    24
    new Position { def getOffset = offset; override def toString: String = offset.toString }
wenzelm@40452
    25
wenzelm@58526
    26
  def root_data(buffer: Buffer): SideKickParsedData =
wenzelm@58526
    27
  {
wenzelm@58526
    28
    val data = new SideKickParsedData(buffer.getName)
wenzelm@58526
    29
    data.getAsset(data.root).setEnd(int_to_pos(buffer.getLength))
wenzelm@58526
    30
    data
wenzelm@58526
    31
  }
wenzelm@58526
    32
wenzelm@40477
    33
  class Asset(name: String, start: Text.Offset, end: Text.Offset) extends IAsset
wenzelm@40452
    34
  {
wenzelm@40452
    35
    protected var _name = name
wenzelm@40452
    36
    protected var _start = int_to_pos(start)
wenzelm@40452
    37
    protected var _end = int_to_pos(end)
wenzelm@40452
    38
    override def getIcon: Icon = null
wenzelm@53973
    39
    override def getShortString: String =
wenzelm@55825
    40
      "<html><span style=\"font-family: " + Font_Info.main_family() + ";\">" +
wenzelm@53985
    41
      HTML.encode(_name) + "</span></html>"
wenzelm@40452
    42
    override def getLongString: String = _name
wenzelm@40452
    43
    override def getName: String = _name
wenzelm@40452
    44
    override def setName(name: String) = _name = name
wenzelm@40452
    45
    override def getStart: Position = _start
wenzelm@40452
    46
    override def setStart(start: Position) = _start = start
wenzelm@40452
    47
    override def getEnd: Position = _end
wenzelm@40452
    48
    override def setEnd(end: Position) = _end = end
wenzelm@57912
    49
    override def toString: String = _name
wenzelm@40452
    50
  }
wenzelm@51618
    51
wenzelm@51618
    52
  def swing_markup_tree(tree: Markup_Tree, parent: DefaultMutableTreeNode,
wenzelm@51618
    53
    swing_node: Text.Info[List[XML.Elem]] => DefaultMutableTreeNode)
wenzelm@51618
    54
  {
wenzelm@51618
    55
    for ((_, entry) <- tree.branches) {
wenzelm@51618
    56
      val node = swing_node(Text.Info(entry.range, entry.markup))
wenzelm@51618
    57
      swing_markup_tree(entry.subtree, node, swing_node)
wenzelm@51618
    58
      parent.add(node)
wenzelm@51618
    59
    }
wenzelm@51618
    60
  }
wenzelm@36738
    61
}
wenzelm@36738
    62
wenzelm@36738
    63
wenzelm@53274
    64
class Isabelle_Sidekick(name: String) extends SideKickParser(name)
wenzelm@34625
    65
{
wenzelm@53274
    66
  override def supportsCompletion = false
wenzelm@53274
    67
wenzelm@53274
    68
wenzelm@34417
    69
  /* parsing */
wenzelm@34417
    70
wenzelm@36759
    71
  @volatile protected var stopped = false
wenzelm@34503
    72
  override def stop() = { stopped = true }
immler@34401
    73
wenzelm@48717
    74
  def parser(buffer: Buffer, syntax: Outer_Syntax, data: SideKickParsedData): Boolean = false
wenzelm@36759
    75
wenzelm@53274
    76
  def parse(buffer: Buffer, error_source: errorlist.DefaultErrorSource): SideKickParsedData =
wenzelm@34625
    77
  {
wenzelm@34417
    78
    stopped = false
wenzelm@34625
    79
wenzelm@38640
    80
    // FIXME lock buffer (!??)
wenzelm@58526
    81
    val data = Isabelle_Sidekick.root_data(buffer)
wenzelm@53274
    82
    val syntax = Isabelle.mode_syntax(name)
wenzelm@48717
    83
    val ok =
wenzelm@48717
    84
      if (syntax.isDefined) {
wenzelm@48717
    85
        val ok = parser(buffer, syntax.get, data)
wenzelm@58526
    86
        if (stopped) { data.root.add(new DefaultMutableTreeNode("<stopped>")); true }
wenzelm@48717
    87
        else ok
wenzelm@48717
    88
      }
wenzelm@48717
    89
      else false
wenzelm@58526
    90
    if (!ok) data.root.add(new DefaultMutableTreeNode("<ignored>"))
wenzelm@48717
    91
wenzelm@34417
    92
    data
wenzelm@34417
    93
  }
immler@34393
    94
}
wenzelm@36738
    95
wenzelm@36738
    96
wenzelm@48718
    97
class Isabelle_Sidekick_Structure(
wenzelm@48718
    98
    name: String,
wenzelm@48718
    99
    node_name: Buffer => Option[Document.Node.Name])
wenzelm@53274
   100
  extends Isabelle_Sidekick(name)
wenzelm@36759
   101
{
wenzelm@48717
   102
  override def parser(buffer: Buffer, syntax: Outer_Syntax, data: SideKickParsedData): Boolean =
wenzelm@36759
   103
  {
wenzelm@57900
   104
    def make_tree(offset: Text.Offset, entry: Thy_Structure.Entry): List[DefaultMutableTreeNode] =
wenzelm@40455
   105
      entry match {
wenzelm@57900
   106
        case Thy_Structure.Block(name, body) =>
wenzelm@40455
   107
          val node =
wenzelm@40455
   108
            new DefaultMutableTreeNode(
wenzelm@40475
   109
              new Isabelle_Sidekick.Asset(Library.first_line(name), offset, offset + entry.length))
wenzelm@40455
   110
          (offset /: body)((i, e) =>
wenzelm@40455
   111
            {
wenzelm@40455
   112
              make_tree(i, e) foreach (nd => node.add(nd))
wenzelm@40455
   113
              i + e.length
wenzelm@40455
   114
            })
wenzelm@40455
   115
          List(node)
wenzelm@57900
   116
        case Thy_Structure.Atom(command)
wenzelm@57904
   117
        if command.is_proper && syntax.heading_level(command).isEmpty =>
wenzelm@40455
   118
          val node =
wenzelm@40455
   119
            new DefaultMutableTreeNode(
wenzelm@40455
   120
              new Isabelle_Sidekick.Asset(command.name, offset, offset + entry.length))
wenzelm@40455
   121
          List(node)
wenzelm@40455
   122
        case _ => Nil
wenzelm@40455
   123
      }
wenzelm@40455
   124
wenzelm@48718
   125
    node_name(buffer) match {
wenzelm@48718
   126
      case Some(name) =>
wenzelm@49406
   127
        val text = JEdit_Lib.buffer_text(buffer)
wenzelm@57900
   128
        val structure = Thy_Structure.parse(syntax, name, text)
wenzelm@48717
   129
        make_tree(0, structure) foreach (node => data.root.add(node))
wenzelm@48717
   130
        true
wenzelm@48717
   131
      case None => false
wenzelm@48717
   132
    }
wenzelm@36759
   133
  }
wenzelm@36759
   134
}
wenzelm@36738
   135
wenzelm@36738
   136
wenzelm@53274
   137
class Isabelle_Sidekick_Default extends
wenzelm@56208
   138
  Isabelle_Sidekick_Structure("isabelle", PIDE.resources.theory_node_name)
wenzelm@48717
   139
wenzelm@48717
   140
wenzelm@53274
   141
class Isabelle_Sidekick_Options extends
wenzelm@54515
   142
  Isabelle_Sidekick_Structure("isabelle-options", _ => Some(Document.Node.Name("options")))
wenzelm@48718
   143
wenzelm@48718
   144
wenzelm@53274
   145
class Isabelle_Sidekick_Root extends
wenzelm@54515
   146
  Isabelle_Sidekick_Structure("isabelle-root", _ => Some(Document.Node.Name("ROOT")))
wenzelm@48717
   147
wenzelm@48717
   148
wenzelm@53281
   149
class Isabelle_Sidekick_Markup extends Isabelle_Sidekick("isabelle-markup")
wenzelm@36759
   150
{
wenzelm@48717
   151
  override def parser(buffer: Buffer, syntax: Outer_Syntax, data: SideKickParsedData): Boolean =
wenzelm@36759
   152
  {
wenzelm@55513
   153
    val opt_snapshot =
wenzelm@57612
   154
      GUI_Thread.now {
wenzelm@55513
   155
        Document_Model(buffer) match {
wenzelm@55513
   156
          case Some(model) if model.is_theory => Some(model.snapshot)
wenzelm@55513
   157
          case _ => None
wenzelm@55513
   158
        }
wenzelm@55513
   159
      }
wenzelm@55513
   160
    opt_snapshot match {
wenzelm@55513
   161
      case Some(snapshot) =>
wenzelm@56373
   162
        for ((command, command_start) <- snapshot.node.command_iterator() if !stopped) {
wenzelm@55650
   163
          val markup =
wenzelm@56301
   164
            snapshot.state.command_markup(
wenzelm@56301
   165
              snapshot.version, command, Command.Markup_Index.markup,
wenzelm@56743
   166
                command.range, Markup.Elements.full)
wenzelm@58526
   167
          Isabelle_Sidekick.swing_markup_tree(markup, data.root,
wenzelm@58526
   168
            (info: Text.Info[List[XML.Elem]]) =>
wenzelm@48717
   169
              {
wenzelm@48717
   170
                val range = info.range + command_start
wenzelm@48717
   171
                val content = command.source(info.range).replace('\n', ' ')
wenzelm@48717
   172
                val info_text =
wenzelm@51493
   173
                  Pretty.formatted(Library.separate(Pretty.FBreak, info.info), margin = 40.0)
wenzelm@51493
   174
                    .mkString
wenzelm@36738
   175
wenzelm@48717
   176
                new DefaultMutableTreeNode(
wenzelm@48717
   177
                  new Isabelle_Sidekick.Asset(command.toString, range.start, range.stop) {
wenzelm@48717
   178
                    override def getShortString: String = content
wenzelm@48717
   179
                    override def getLongString: String = info_text
wenzelm@57912
   180
                    override def toString: String = quote(content) + " " + range.toString
wenzelm@48717
   181
                  })
wenzelm@40452
   182
              })
wenzelm@48717
   183
        }
wenzelm@48717
   184
        true
wenzelm@55513
   185
      case None => false
wenzelm@36759
   186
    }
wenzelm@36759
   187
  }
wenzelm@36759
   188
}
wenzelm@36738
   189
wenzelm@52539
   190
wenzelm@53274
   191
class Isabelle_Sidekick_News extends Isabelle_Sidekick("isabelle-news")
wenzelm@52539
   192
{
wenzelm@53274
   193
  private val Heading1 = """^New in (.*)\w*$""".r
wenzelm@53274
   194
  private val Heading2 = """^\*\*\*\w*(.*)\w*\*\*\*\w*$""".r
wenzelm@52539
   195
wenzelm@52539
   196
  private def make_node(s: String, start: Text.Offset, stop: Text.Offset): DefaultMutableTreeNode =
wenzelm@52539
   197
    new DefaultMutableTreeNode(new Isabelle_Sidekick.Asset(s, start, stop))
wenzelm@52539
   198
wenzelm@52539
   199
  override def parser(buffer: Buffer, syntax: Outer_Syntax, data: SideKickParsedData): Boolean =
wenzelm@52539
   200
  {
wenzelm@52539
   201
    var offset = 0
wenzelm@58542
   202
    var end_offset = 0
wenzelm@58542
   203
wenzelm@58542
   204
    var start1: Option[(Int, String, Vector[DefaultMutableTreeNode])] = None
wenzelm@58542
   205
    var start2: Option[(Int, String)] = None
wenzelm@58542
   206
wenzelm@58542
   207
    def close1: Unit =
wenzelm@58542
   208
      start1 match {
wenzelm@58542
   209
        case Some((start_offset, s, body)) =>
wenzelm@58542
   210
          val node = make_node(s, start_offset, end_offset)
wenzelm@58542
   211
          body.foreach(node.add(_))
wenzelm@58542
   212
          data.root.add(node)
wenzelm@58542
   213
          start1 = None
wenzelm@58542
   214
        case None =>
wenzelm@58542
   215
      }
wenzelm@58542
   216
wenzelm@58542
   217
    def close2: Unit =
wenzelm@58542
   218
      start2 match {
wenzelm@58542
   219
        case Some((start_offset, s)) =>
wenzelm@58542
   220
          start1 match {
wenzelm@58542
   221
            case Some((start_offset1, s1, body)) =>
wenzelm@58542
   222
              val node = make_node(s, start_offset, end_offset)
wenzelm@58542
   223
              start1 = Some((start_offset1, s1, body :+ node))
wenzelm@58542
   224
            case None =>
wenzelm@58542
   225
          }
wenzelm@58542
   226
          start2 = None
wenzelm@58542
   227
        case None =>
wenzelm@58542
   228
      }
wenzelm@52539
   229
wenzelm@52539
   230
    for (line <- split_lines(JEdit_Lib.buffer_text(buffer)) if !stopped) {
wenzelm@52539
   231
      line match {
wenzelm@58542
   232
        case Heading1(s) => close2; close1; start1 = Some((offset, s, Vector()))
wenzelm@58542
   233
        case Heading2(s) => close2; start2 = Some((offset, s))
wenzelm@52539
   234
        case _ =>
wenzelm@52539
   235
      }
wenzelm@52539
   236
      offset += line.length + 1
wenzelm@58542
   237
      if (!line.forall(Character.isSpaceChar(_))) end_offset = offset
wenzelm@52539
   238
    }
wenzelm@58542
   239
    if (!stopped) { close2; close1 }
wenzelm@52539
   240
wenzelm@52539
   241
    true
wenzelm@52539
   242
  }
wenzelm@52539
   243
}
wenzelm@52539
   244