src/Tools/jEdit/src/isabelle_sidekick.scala
author wenzelm
Mon Jan 09 20:26:59 2017 +0100 (2017-01-09)
changeset 64854 f5aa712e6250
parent 64813 7283f41d05ab
child 65130 695930882487
permissions -rw-r--r--
tuned signature;
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@59183
    15
import javax.swing.{JLabel, 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@58747
    33
  class Keyword_Asset(keyword: String, text: String, range: Text.Range) extends IAsset
wenzelm@40452
    34
  {
wenzelm@59286
    35
    private val css = GUI.imitate_font_css((new JLabel).getFont, Font_Info.main_family())
wenzelm@59183
    36
wenzelm@58747
    37
    protected var _name = text
wenzelm@58747
    38
    protected var _start = int_to_pos(range.start)
wenzelm@58747
    39
    protected var _end = int_to_pos(range.stop)
wenzelm@40452
    40
    override def getIcon: Icon = null
wenzelm@53973
    41
    override def getShortString: String =
wenzelm@59933
    42
    {
wenzelm@59933
    43
      val n = keyword.length
wenzelm@59933
    44
      val s =
wenzelm@59933
    45
        _name.indexOf(keyword) match {
wenzelm@59933
    46
          case i if i >= 0 && n > 0 =>
wenzelm@62113
    47
            HTML.output(_name.substring(0, i)) +
wenzelm@62113
    48
            "<b>" + HTML.output(keyword) + "</b>" +
wenzelm@62113
    49
            HTML.output(_name.substring(i + n))
wenzelm@62113
    50
          case _ => HTML.output(_name)
wenzelm@59933
    51
        }
wenzelm@59933
    52
      "<html><span style=\"" + css + "\">" + s + "</span></html>"
wenzelm@59933
    53
    }
wenzelm@40452
    54
    override def getLongString: String = _name
wenzelm@40452
    55
    override def getName: String = _name
wenzelm@40452
    56
    override def setName(name: String) = _name = name
wenzelm@40452
    57
    override def getStart: Position = _start
wenzelm@40452
    58
    override def setStart(start: Position) = _start = start
wenzelm@40452
    59
    override def getEnd: Position = _end
wenzelm@40452
    60
    override def setEnd(end: Position) = _end = end
wenzelm@57912
    61
    override def toString: String = _name
wenzelm@40452
    62
  }
wenzelm@51618
    63
wenzelm@58747
    64
  class Asset(name: String, range: Text.Range) extends Keyword_Asset("", name, range)
wenzelm@58747
    65
wenzelm@51618
    66
  def swing_markup_tree(tree: Markup_Tree, parent: DefaultMutableTreeNode,
wenzelm@51618
    67
    swing_node: Text.Info[List[XML.Elem]] => DefaultMutableTreeNode)
wenzelm@51618
    68
  {
wenzelm@51618
    69
    for ((_, entry) <- tree.branches) {
wenzelm@51618
    70
      val node = swing_node(Text.Info(entry.range, entry.markup))
wenzelm@51618
    71
      swing_markup_tree(entry.subtree, node, swing_node)
wenzelm@51618
    72
      parent.add(node)
wenzelm@51618
    73
    }
wenzelm@51618
    74
  }
wenzelm@36738
    75
}
wenzelm@36738
    76
wenzelm@36738
    77
wenzelm@53274
    78
class Isabelle_Sidekick(name: String) extends SideKickParser(name)
wenzelm@34625
    79
{
wenzelm@53274
    80
  override def supportsCompletion = false
wenzelm@53274
    81
wenzelm@53274
    82
wenzelm@34417
    83
  /* parsing */
wenzelm@34417
    84
wenzelm@36759
    85
  @volatile protected var stopped = false
wenzelm@34503
    86
  override def stop() = { stopped = true }
immler@34401
    87
wenzelm@48717
    88
  def parser(buffer: Buffer, syntax: Outer_Syntax, data: SideKickParsedData): Boolean = false
wenzelm@36759
    89
wenzelm@53274
    90
  def parse(buffer: Buffer, error_source: errorlist.DefaultErrorSource): SideKickParsedData =
wenzelm@34625
    91
  {
wenzelm@34417
    92
    stopped = false
wenzelm@34625
    93
wenzelm@38640
    94
    // FIXME lock buffer (!??)
wenzelm@58526
    95
    val data = Isabelle_Sidekick.root_data(buffer)
wenzelm@60272
    96
    val syntax = Isabelle.buffer_syntax(buffer)
wenzelm@48717
    97
    val ok =
wenzelm@48717
    98
      if (syntax.isDefined) {
wenzelm@48717
    99
        val ok = parser(buffer, syntax.get, data)
wenzelm@58526
   100
        if (stopped) { data.root.add(new DefaultMutableTreeNode("<stopped>")); true }
wenzelm@48717
   101
        else ok
wenzelm@48717
   102
      }
wenzelm@48717
   103
      else false
wenzelm@58526
   104
    if (!ok) data.root.add(new DefaultMutableTreeNode("<ignored>"))
wenzelm@48717
   105
wenzelm@34417
   106
    data
wenzelm@34417
   107
  }
immler@34393
   108
}
wenzelm@36738
   109
wenzelm@36738
   110
wenzelm@48718
   111
class Isabelle_Sidekick_Structure(
wenzelm@48718
   112
    name: String,
wenzelm@63606
   113
    node_name: Buffer => Option[Document.Node.Name],
wenzelm@63606
   114
    parse: (Outer_Syntax, Document.Node.Name, CharSequence) => List[Document_Structure.Document])
wenzelm@53274
   115
  extends Isabelle_Sidekick(name)
wenzelm@36759
   116
{
wenzelm@48717
   117
  override def parser(buffer: Buffer, syntax: Outer_Syntax, data: SideKickParsedData): Boolean =
wenzelm@36759
   118
  {
wenzelm@58743
   119
    def make_tree(
wenzelm@58743
   120
      parent: DefaultMutableTreeNode,
wenzelm@58743
   121
      offset: Text.Offset,
wenzelm@63604
   122
      documents: List[Document_Structure.Document])
wenzelm@58743
   123
    {
wenzelm@58743
   124
      (offset /: documents) { case (i, document) =>
wenzelm@58743
   125
        document match {
wenzelm@63604
   126
          case Document_Structure.Block(name, text, body) =>
wenzelm@58747
   127
            val range = Text.Range(i, i + document.length)
wenzelm@58743
   128
            val node =
wenzelm@58743
   129
              new DefaultMutableTreeNode(
wenzelm@58747
   130
                new Isabelle_Sidekick.Keyword_Asset(name, Library.first_line(text), range))
wenzelm@58743
   131
            parent.add(node)
wenzelm@58743
   132
            make_tree(node, i, body)
wenzelm@58743
   133
          case _ =>
wenzelm@58743
   134
        }
wenzelm@58743
   135
        i + document.length
wenzelm@40455
   136
      }
wenzelm@58743
   137
    }
wenzelm@40455
   138
wenzelm@48718
   139
    node_name(buffer) match {
wenzelm@48718
   140
      case Some(name) =>
wenzelm@63606
   141
        make_tree(data.root, 0, parse(syntax, name, JEdit_Lib.buffer_text(buffer)))
wenzelm@48717
   142
        true
wenzelm@63606
   143
      case None =>
wenzelm@63606
   144
        false
wenzelm@48717
   145
    }
wenzelm@36759
   146
  }
wenzelm@36759
   147
}
wenzelm@36738
   148
wenzelm@53274
   149
class Isabelle_Sidekick_Default extends
wenzelm@63606
   150
  Isabelle_Sidekick_Structure("isabelle",
wenzelm@63606
   151
    PIDE.resources.theory_node_name, Document_Structure.parse_sections _)
wenzelm@63606
   152
wenzelm@63606
   153
class Isabelle_Sidekick_Context extends
wenzelm@63606
   154
  Isabelle_Sidekick_Structure("isabelle-context",
wenzelm@63606
   155
    PIDE.resources.theory_node_name, Document_Structure.parse_blocks _)
wenzelm@48717
   156
wenzelm@53274
   157
class Isabelle_Sidekick_Options extends
wenzelm@63606
   158
  Isabelle_Sidekick_Structure("isabelle-options",
wenzelm@63606
   159
    _ => Some(Document.Node.Name("options")), Document_Structure.parse_sections _)
wenzelm@48718
   160
wenzelm@53274
   161
class Isabelle_Sidekick_Root extends
wenzelm@63606
   162
  Isabelle_Sidekick_Structure("isabelle-root",
wenzelm@63606
   163
    _ => Some(Document.Node.Name("ROOT")), Document_Structure.parse_sections _)
wenzelm@48717
   164
wenzelm@63610
   165
class Isabelle_Sidekick_ML extends
wenzelm@63610
   166
  Isabelle_Sidekick_Structure("isabelle-ml",
wenzelm@63610
   167
    buffer => Some(PIDE.resources.node_name(buffer)),
wenzelm@63610
   168
    (_, _, text) => Document_Structure.parse_ml_sections(false, text))
wenzelm@63610
   169
wenzelm@63610
   170
class Isabelle_Sidekick_SML extends
wenzelm@63610
   171
  Isabelle_Sidekick_Structure("isabelle-sml",
wenzelm@63610
   172
    buffer => Some(PIDE.resources.node_name(buffer)),
wenzelm@63610
   173
    (_, _, text) => Document_Structure.parse_ml_sections(true, text))
wenzelm@63610
   174
wenzelm@48717
   175
wenzelm@53281
   176
class Isabelle_Sidekick_Markup extends Isabelle_Sidekick("isabelle-markup")
wenzelm@36759
   177
{
wenzelm@48717
   178
  override def parser(buffer: Buffer, syntax: Outer_Syntax, data: SideKickParsedData): Boolean =
wenzelm@36759
   179
  {
wenzelm@55513
   180
    val opt_snapshot =
wenzelm@64813
   181
      Document_Model.get(buffer) match {
wenzelm@60272
   182
        case Some(model) if model.is_theory => Some(model.snapshot)
wenzelm@60272
   183
        case _ => None
wenzelm@55513
   184
      }
wenzelm@55513
   185
    opt_snapshot match {
wenzelm@55513
   186
      case Some(snapshot) =>
wenzelm@56373
   187
        for ((command, command_start) <- snapshot.node.command_iterator() if !stopped) {
wenzelm@55650
   188
          val markup =
wenzelm@56301
   189
            snapshot.state.command_markup(
wenzelm@56301
   190
              snapshot.version, command, Command.Markup_Index.markup,
wenzelm@56743
   191
                command.range, Markup.Elements.full)
wenzelm@58526
   192
          Isabelle_Sidekick.swing_markup_tree(markup, data.root,
wenzelm@58526
   193
            (info: Text.Info[List[XML.Elem]]) =>
wenzelm@48717
   194
              {
wenzelm@48717
   195
                val range = info.range + command_start
wenzelm@48717
   196
                val content = command.source(info.range).replace('\n', ' ')
wenzelm@48717
   197
                val info_text =
wenzelm@61871
   198
                  Pretty.formatted(Library.separate(Pretty.fbrk, info.info), margin = 40.0)
wenzelm@51493
   199
                    .mkString
wenzelm@36738
   200
wenzelm@48717
   201
                new DefaultMutableTreeNode(
wenzelm@58747
   202
                  new Isabelle_Sidekick.Asset(command.toString, range) {
wenzelm@48717
   203
                    override def getShortString: String = content
wenzelm@48717
   204
                    override def getLongString: String = info_text
wenzelm@57912
   205
                    override def toString: String = quote(content) + " " + range.toString
wenzelm@48717
   206
                  })
wenzelm@40452
   207
              })
wenzelm@48717
   208
        }
wenzelm@48717
   209
        true
wenzelm@55513
   210
      case None => false
wenzelm@36759
   211
    }
wenzelm@36759
   212
  }
wenzelm@36759
   213
}
wenzelm@36738
   214
wenzelm@52539
   215
wenzelm@53274
   216
class Isabelle_Sidekick_News extends Isabelle_Sidekick("isabelle-news")
wenzelm@52539
   217
{
wenzelm@53274
   218
  private val Heading1 = """^New in (.*)\w*$""".r
wenzelm@53274
   219
  private val Heading2 = """^\*\*\*\w*(.*)\w*\*\*\*\w*$""".r
wenzelm@52539
   220
wenzelm@52539
   221
  private def make_node(s: String, start: Text.Offset, stop: Text.Offset): DefaultMutableTreeNode =
wenzelm@58747
   222
    new DefaultMutableTreeNode(new Isabelle_Sidekick.Asset(s, Text.Range(start, stop)))
wenzelm@52539
   223
wenzelm@52539
   224
  override def parser(buffer: Buffer, syntax: Outer_Syntax, data: SideKickParsedData): Boolean =
wenzelm@52539
   225
  {
wenzelm@52539
   226
    var offset = 0
wenzelm@58542
   227
    var end_offset = 0
wenzelm@58542
   228
wenzelm@58542
   229
    var start1: Option[(Int, String, Vector[DefaultMutableTreeNode])] = None
wenzelm@58542
   230
    var start2: Option[(Int, String)] = None
wenzelm@58542
   231
wenzelm@58542
   232
    def close1: Unit =
wenzelm@58542
   233
      start1 match {
wenzelm@58542
   234
        case Some((start_offset, s, body)) =>
wenzelm@58542
   235
          val node = make_node(s, start_offset, end_offset)
wenzelm@58542
   236
          body.foreach(node.add(_))
wenzelm@58542
   237
          data.root.add(node)
wenzelm@58542
   238
          start1 = None
wenzelm@58542
   239
        case None =>
wenzelm@58542
   240
      }
wenzelm@58542
   241
wenzelm@58542
   242
    def close2: Unit =
wenzelm@58542
   243
      start2 match {
wenzelm@58542
   244
        case Some((start_offset, s)) =>
wenzelm@58542
   245
          start1 match {
wenzelm@58542
   246
            case Some((start_offset1, s1, body)) =>
wenzelm@58542
   247
              val node = make_node(s, start_offset, end_offset)
wenzelm@58542
   248
              start1 = Some((start_offset1, s1, body :+ node))
wenzelm@58542
   249
            case None =>
wenzelm@58542
   250
          }
wenzelm@58542
   251
          start2 = None
wenzelm@58542
   252
        case None =>
wenzelm@58542
   253
      }
wenzelm@52539
   254
wenzelm@52539
   255
    for (line <- split_lines(JEdit_Lib.buffer_text(buffer)) if !stopped) {
wenzelm@52539
   256
      line match {
wenzelm@58542
   257
        case Heading1(s) => close2; close1; start1 = Some((offset, s, Vector()))
wenzelm@58542
   258
        case Heading2(s) => close2; start2 = Some((offset, s))
wenzelm@52539
   259
        case _ =>
wenzelm@52539
   260
      }
wenzelm@52539
   261
      offset += line.length + 1
wenzelm@58542
   262
      if (!line.forall(Character.isSpaceChar(_))) end_offset = offset
wenzelm@52539
   263
    }
wenzelm@58542
   264
    if (!stopped) { close2; close1 }
wenzelm@52539
   265
wenzelm@52539
   266
    true
wenzelm@52539
   267
  }
wenzelm@52539
   268
}
wenzelm@52539
   269