src/Tools/jEdit/src/isabelle_sidekick.scala
author wenzelm
Tue, 07 Aug 2012 22:25:17 +0200
changeset 48718 73e6c22e2d94
parent 48717 622251b2b0f1
child 48826 b19ba23e70c5
permissions -rw-r--r--
more structural parsing for minor modes; tuned signatures;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
43282
5d294220ca43 moved sources -- eliminated Netbeans artifact of jedit package directory;
wenzelm
parents: 40792
diff changeset
     1
/*  Title:      Tools/jEdit/src/isabelle_sidekick.scala
36760
b82a698ef6c9 tuned headers;
wenzelm
parents: 36759
diff changeset
     2
    Author:     Fabian Immler, TU Munich
b82a698ef6c9 tuned headers;
wenzelm
parents: 36759
diff changeset
     3
    Author:     Makarius
b82a698ef6c9 tuned headers;
wenzelm
parents: 36759
diff changeset
     4
b82a698ef6c9 tuned headers;
wenzelm
parents: 36759
diff changeset
     5
SideKick parsers for Isabelle proof documents.
b82a698ef6c9 tuned headers;
wenzelm
parents: 36759
diff changeset
     6
*/
34393
f0e1608a774f basic tree structure for sidekick
immler@in.tum.de
parents:
diff changeset
     7
34426
81f93e0f13b4 renamed isabelle.prover.IsabelleSKParser to isabelle.jedit.IsabelleSideKickParser;
wenzelm
parents: 34417
diff changeset
     8
package isabelle.jedit
34393
f0e1608a774f basic tree structure for sidekick
immler@in.tum.de
parents:
diff changeset
     9
34760
dc7f5e0d9d27 misc modernization of names;
wenzelm
parents: 34759
diff changeset
    10
36015
6111de7c916a adapted to Scala 2.8.0 Beta 1;
wenzelm
parents: 35004
diff changeset
    11
import isabelle._
6111de7c916a adapted to Scala 2.8.0 Beta 1;
wenzelm
parents: 35004
diff changeset
    12
34475
f963335dbc6b implemented IsabelleSideKickParser.complete
immler@in.tum.de
parents: 34440
diff changeset
    13
import scala.collection.Set
f963335dbc6b implemented IsabelleSideKickParser.complete
immler@in.tum.de
parents: 34440
diff changeset
    14
import scala.collection.immutable.TreeSet
34417
bce2f2ea9819 misc tuning and adaption according to original IsabelleParser --
wenzelm
parents: 34408
diff changeset
    15
47589
b9e2ed4b1579 custom ListCellRenderer with text area font ensures that symbols are displayed reliably;
wenzelm
parents: 47539
diff changeset
    16
import java.awt.Component
34393
f0e1608a774f basic tree structure for sidekick
immler@in.tum.de
parents:
diff changeset
    17
import javax.swing.tree.DefaultMutableTreeNode
34701
80b0add08eef IsabelleSideKickParser: incorporate former MarkupNode.markup2default_node, observe stopped flag;
wenzelm
parents: 34669
diff changeset
    18
import javax.swing.text.Position
47589
b9e2ed4b1579 custom ListCellRenderer with text area font ensures that symbols are displayed reliably;
wenzelm
parents: 47539
diff changeset
    19
import javax.swing.{Icon, DefaultListCellRenderer, ListCellRenderer, JList}
34417
bce2f2ea9819 misc tuning and adaption according to original IsabelleParser --
wenzelm
parents: 34408
diff changeset
    20
34609
7ca1ef2f150d simplified and reactivated SideKickCompletion, cf. org.gjt.sp.jedit.gui.CompleteWord;
wenzelm
parents: 34562
diff changeset
    21
import org.gjt.sp.jedit.{Buffer, EditPane, TextUtilities, View}
34417
bce2f2ea9819 misc tuning and adaption according to original IsabelleParser --
wenzelm
parents: 34408
diff changeset
    22
import errorlist.DefaultErrorSource
47589
b9e2ed4b1579 custom ListCellRenderer with text area font ensures that symbols are displayed reliably;
wenzelm
parents: 47539
diff changeset
    23
import sidekick.{SideKickParser, SideKickParsedData, SideKickCompletion,
b9e2ed4b1579 custom ListCellRenderer with text area font ensures that symbols are displayed reliably;
wenzelm
parents: 47539
diff changeset
    24
  SideKickCompletionPopup, IAsset}
34701
80b0add08eef IsabelleSideKickParser: incorporate former MarkupNode.markup2default_node, observe stopped flag;
wenzelm
parents: 34669
diff changeset
    25
34393
f0e1608a774f basic tree structure for sidekick
immler@in.tum.de
parents:
diff changeset
    26
36738
dce592144219 support several sidekick parsers -- very basic default parser;
wenzelm
parents: 36737
diff changeset
    27
object Isabelle_Sidekick
dce592144219 support several sidekick parsers -- very basic default parser;
wenzelm
parents: 36737
diff changeset
    28
{
40477
wenzelm
parents: 40475
diff changeset
    29
  def int_to_pos(offset: Text.Offset): Position =
36738
dce592144219 support several sidekick parsers -- very basic default parser;
wenzelm
parents: 36737
diff changeset
    30
    new Position { def getOffset = offset; override def toString = offset.toString }
40452
45e7c2889d2f misc tuning and simplification, using Isabelle_Sidekick.Asset (not sidekick.Asset, which is dynamically dispatched to slightly different semantics);
wenzelm
parents: 39624
diff changeset
    31
40477
wenzelm
parents: 40475
diff changeset
    32
  class Asset(name: String, start: Text.Offset, end: Text.Offset) extends IAsset
40452
45e7c2889d2f misc tuning and simplification, using Isabelle_Sidekick.Asset (not sidekick.Asset, which is dynamically dispatched to slightly different semantics);
wenzelm
parents: 39624
diff changeset
    33
  {
45e7c2889d2f misc tuning and simplification, using Isabelle_Sidekick.Asset (not sidekick.Asset, which is dynamically dispatched to slightly different semantics);
wenzelm
parents: 39624
diff changeset
    34
    protected var _name = name
45e7c2889d2f misc tuning and simplification, using Isabelle_Sidekick.Asset (not sidekick.Asset, which is dynamically dispatched to slightly different semantics);
wenzelm
parents: 39624
diff changeset
    35
    protected var _start = int_to_pos(start)
45e7c2889d2f misc tuning and simplification, using Isabelle_Sidekick.Asset (not sidekick.Asset, which is dynamically dispatched to slightly different semantics);
wenzelm
parents: 39624
diff changeset
    36
    protected var _end = int_to_pos(end)
45e7c2889d2f misc tuning and simplification, using Isabelle_Sidekick.Asset (not sidekick.Asset, which is dynamically dispatched to slightly different semantics);
wenzelm
parents: 39624
diff changeset
    37
    override def getIcon: Icon = null
45e7c2889d2f misc tuning and simplification, using Isabelle_Sidekick.Asset (not sidekick.Asset, which is dynamically dispatched to slightly different semantics);
wenzelm
parents: 39624
diff changeset
    38
    override def getShortString: String = _name
45e7c2889d2f misc tuning and simplification, using Isabelle_Sidekick.Asset (not sidekick.Asset, which is dynamically dispatched to slightly different semantics);
wenzelm
parents: 39624
diff changeset
    39
    override def getLongString: String = _name
45e7c2889d2f misc tuning and simplification, using Isabelle_Sidekick.Asset (not sidekick.Asset, which is dynamically dispatched to slightly different semantics);
wenzelm
parents: 39624
diff changeset
    40
    override def getName: String = _name
45e7c2889d2f misc tuning and simplification, using Isabelle_Sidekick.Asset (not sidekick.Asset, which is dynamically dispatched to slightly different semantics);
wenzelm
parents: 39624
diff changeset
    41
    override def setName(name: String) = _name = name
45e7c2889d2f misc tuning and simplification, using Isabelle_Sidekick.Asset (not sidekick.Asset, which is dynamically dispatched to slightly different semantics);
wenzelm
parents: 39624
diff changeset
    42
    override def getStart: Position = _start
45e7c2889d2f misc tuning and simplification, using Isabelle_Sidekick.Asset (not sidekick.Asset, which is dynamically dispatched to slightly different semantics);
wenzelm
parents: 39624
diff changeset
    43
    override def setStart(start: Position) = _start = start
45e7c2889d2f misc tuning and simplification, using Isabelle_Sidekick.Asset (not sidekick.Asset, which is dynamically dispatched to slightly different semantics);
wenzelm
parents: 39624
diff changeset
    44
    override def getEnd: Position = _end
45e7c2889d2f misc tuning and simplification, using Isabelle_Sidekick.Asset (not sidekick.Asset, which is dynamically dispatched to slightly different semantics);
wenzelm
parents: 39624
diff changeset
    45
    override def setEnd(end: Position) = _end = end
45e7c2889d2f misc tuning and simplification, using Isabelle_Sidekick.Asset (not sidekick.Asset, which is dynamically dispatched to slightly different semantics);
wenzelm
parents: 39624
diff changeset
    46
    override def toString = _name
45e7c2889d2f misc tuning and simplification, using Isabelle_Sidekick.Asset (not sidekick.Asset, which is dynamically dispatched to slightly different semantics);
wenzelm
parents: 39624
diff changeset
    47
  }
36738
dce592144219 support several sidekick parsers -- very basic default parser;
wenzelm
parents: 36737
diff changeset
    48
}
dce592144219 support several sidekick parsers -- very basic default parser;
wenzelm
parents: 36737
diff changeset
    49
dce592144219 support several sidekick parsers -- very basic default parser;
wenzelm
parents: 36737
diff changeset
    50
48717
622251b2b0f1 clarified Sidekick configuration, including minor modes;
wenzelm
parents: 47749
diff changeset
    51
class Isabelle_Sidekick(name: String, get_syntax: => Option[Outer_Syntax])
622251b2b0f1 clarified Sidekick configuration, including minor modes;
wenzelm
parents: 47749
diff changeset
    52
  extends SideKickParser(name)
34625
799a40faa4f1 completion: decode symbols only if isabelle encoding is active (to prevent unicode chars written back to file);
wenzelm
parents: 34612
diff changeset
    53
{
34417
bce2f2ea9819 misc tuning and adaption according to original IsabelleParser --
wenzelm
parents: 34408
diff changeset
    54
  /* parsing */
bce2f2ea9819 misc tuning and adaption according to original IsabelleParser --
wenzelm
parents: 34408
diff changeset
    55
36759
wenzelm
parents: 36738
diff changeset
    56
  @volatile protected var stopped = false
34503
7d0726f19d04 tuned whitespace;
wenzelm
parents: 34485
diff changeset
    57
  override def stop() = { stopped = true }
34401
44241a37b74a structure of markup-tree in scala, keep track of swing-nodes in background
immler@in.tum.de
parents: 34393
diff changeset
    58
48717
622251b2b0f1 clarified Sidekick configuration, including minor modes;
wenzelm
parents: 47749
diff changeset
    59
  def parser(buffer: Buffer, syntax: Outer_Syntax, data: SideKickParsedData): Boolean = false
36759
wenzelm
parents: 36738
diff changeset
    60
34625
799a40faa4f1 completion: decode symbols only if isabelle encoding is active (to prevent unicode chars written back to file);
wenzelm
parents: 34612
diff changeset
    61
  def parse(buffer: Buffer, error_source: DefaultErrorSource): SideKickParsedData =
799a40faa4f1 completion: decode symbols only if isabelle encoding is active (to prevent unicode chars written back to file);
wenzelm
parents: 34612
diff changeset
    62
  {
34417
bce2f2ea9819 misc tuning and adaption according to original IsabelleParser --
wenzelm
parents: 34408
diff changeset
    63
    stopped = false
34625
799a40faa4f1 completion: decode symbols only if isabelle encoding is active (to prevent unicode chars written back to file);
wenzelm
parents: 34612
diff changeset
    64
38640
105d1f112da5 sporadic locking of jEdit buffer;
wenzelm
parents: 38577
diff changeset
    65
    // FIXME lock buffer (!??)
34417
bce2f2ea9819 misc tuning and adaption according to original IsabelleParser --
wenzelm
parents: 34408
diff changeset
    66
    val data = new SideKickParsedData(buffer.getName)
34717
3f32e08bbb6c sidekick root data: set buffer length to avoid crash of initial caret move;
wenzelm
parents: 34705
diff changeset
    67
    val root = data.root
40452
45e7c2889d2f misc tuning and simplification, using Isabelle_Sidekick.Asset (not sidekick.Asset, which is dynamically dispatched to slightly different semantics);
wenzelm
parents: 39624
diff changeset
    68
    data.getAsset(root).setEnd(Isabelle_Sidekick.int_to_pos(buffer.getLength))
34475
f963335dbc6b implemented IsabelleSideKickParser.complete
immler@in.tum.de
parents: 34440
diff changeset
    69
48717
622251b2b0f1 clarified Sidekick configuration, including minor modes;
wenzelm
parents: 47749
diff changeset
    70
    val syntax = get_syntax
622251b2b0f1 clarified Sidekick configuration, including minor modes;
wenzelm
parents: 47749
diff changeset
    71
    val ok =
622251b2b0f1 clarified Sidekick configuration, including minor modes;
wenzelm
parents: 47749
diff changeset
    72
      if (syntax.isDefined) {
622251b2b0f1 clarified Sidekick configuration, including minor modes;
wenzelm
parents: 47749
diff changeset
    73
        val ok = parser(buffer, syntax.get, data)
622251b2b0f1 clarified Sidekick configuration, including minor modes;
wenzelm
parents: 47749
diff changeset
    74
        if (stopped) { root.add(new DefaultMutableTreeNode("<stopped>")); true }
622251b2b0f1 clarified Sidekick configuration, including minor modes;
wenzelm
parents: 47749
diff changeset
    75
        else ok
622251b2b0f1 clarified Sidekick configuration, including minor modes;
wenzelm
parents: 47749
diff changeset
    76
      }
622251b2b0f1 clarified Sidekick configuration, including minor modes;
wenzelm
parents: 47749
diff changeset
    77
      else false
622251b2b0f1 clarified Sidekick configuration, including minor modes;
wenzelm
parents: 47749
diff changeset
    78
    if (!ok) root.add(new DefaultMutableTreeNode("<ignored>"))
622251b2b0f1 clarified Sidekick configuration, including minor modes;
wenzelm
parents: 47749
diff changeset
    79
34417
bce2f2ea9819 misc tuning and adaption according to original IsabelleParser --
wenzelm
parents: 34408
diff changeset
    80
    data
bce2f2ea9819 misc tuning and adaption according to original IsabelleParser --
wenzelm
parents: 34408
diff changeset
    81
  }
bce2f2ea9819 misc tuning and adaption according to original IsabelleParser --
wenzelm
parents: 34408
diff changeset
    82
36738
dce592144219 support several sidekick parsers -- very basic default parser;
wenzelm
parents: 36737
diff changeset
    83
34417
bce2f2ea9819 misc tuning and adaption according to original IsabelleParser --
wenzelm
parents: 34408
diff changeset
    84
  /* completion */
bce2f2ea9819 misc tuning and adaption according to original IsabelleParser --
wenzelm
parents: 34408
diff changeset
    85
bce2f2ea9819 misc tuning and adaption according to original IsabelleParser --
wenzelm
parents: 34408
diff changeset
    86
  override def supportsCompletion = true
bce2f2ea9819 misc tuning and adaption according to original IsabelleParser --
wenzelm
parents: 34408
diff changeset
    87
  override def canCompleteAnywhere = true
bce2f2ea9819 misc tuning and adaption according to original IsabelleParser --
wenzelm
parents: 34408
diff changeset
    88
40477
wenzelm
parents: 40475
diff changeset
    89
  override def complete(pane: EditPane, caret: Text.Offset): SideKickCompletion =
34609
7ca1ef2f150d simplified and reactivated SideKickCompletion, cf. org.gjt.sp.jedit.gui.CompleteWord;
wenzelm
parents: 34562
diff changeset
    90
  {
46920
5f44c8bea84e more explicit indication of swing thread context;
wenzelm
parents: 46208
diff changeset
    91
    Swing_Thread.assert()
5f44c8bea84e more explicit indication of swing thread context;
wenzelm
parents: 46208
diff changeset
    92
34475
f963335dbc6b implemented IsabelleSideKickParser.complete
immler@in.tum.de
parents: 34440
diff changeset
    93
    val buffer = pane.getBuffer
46920
5f44c8bea84e more explicit indication of swing thread context;
wenzelm
parents: 46208
diff changeset
    94
    Isabelle.buffer_lock(buffer) {
48717
622251b2b0f1 clarified Sidekick configuration, including minor modes;
wenzelm
parents: 47749
diff changeset
    95
      get_syntax match {
39624
57496c868dcc tuned Isabelle_Sidekick.complete: lock buffer, depend on document model;
wenzelm
parents: 38663
diff changeset
    96
        case None => null
48717
622251b2b0f1 clarified Sidekick configuration, including minor modes;
wenzelm
parents: 47749
diff changeset
    97
        case Some(syntax) =>
39624
57496c868dcc tuned Isabelle_Sidekick.complete: lock buffer, depend on document model;
wenzelm
parents: 38663
diff changeset
    98
          val line = buffer.getLineOfOffset(caret)
57496c868dcc tuned Isabelle_Sidekick.complete: lock buffer, depend on document model;
wenzelm
parents: 38663
diff changeset
    99
          val start = buffer.getLineStartOffset(line)
57496c868dcc tuned Isabelle_Sidekick.complete: lock buffer, depend on document model;
wenzelm
parents: 38663
diff changeset
   100
          val text = buffer.getSegment(start, caret - start)
34475
f963335dbc6b implemented IsabelleSideKickParser.complete
immler@in.tum.de
parents: 34440
diff changeset
   101
48717
622251b2b0f1 clarified Sidekick configuration, including minor modes;
wenzelm
parents: 47749
diff changeset
   102
          syntax.completion.complete(text) match {
39624
57496c868dcc tuned Isabelle_Sidekick.complete: lock buffer, depend on document model;
wenzelm
parents: 38663
diff changeset
   103
            case None => null
57496c868dcc tuned Isabelle_Sidekick.complete: lock buffer, depend on document model;
wenzelm
parents: 38663
diff changeset
   104
            case Some((word, cs)) =>
57496c868dcc tuned Isabelle_Sidekick.complete: lock buffer, depend on document model;
wenzelm
parents: 38663
diff changeset
   105
              val ds =
57496c868dcc tuned Isabelle_Sidekick.complete: lock buffer, depend on document model;
wenzelm
parents: 38663
diff changeset
   106
                (if (Isabelle_Encoding.is_active(buffer))
45900
793bf5fa5fbf prefer sorting from Scala library;
wenzelm
parents: 45455
diff changeset
   107
                  cs.map(Symbol.decode(_)).sorted
39624
57496c868dcc tuned Isabelle_Sidekick.complete: lock buffer, depend on document model;
wenzelm
parents: 38663
diff changeset
   108
                 else cs).filter(_ != word)
57496c868dcc tuned Isabelle_Sidekick.complete: lock buffer, depend on document model;
wenzelm
parents: 38663
diff changeset
   109
              if (ds.isEmpty) null
47589
b9e2ed4b1579 custom ListCellRenderer with text area font ensures that symbols are displayed reliably;
wenzelm
parents: 47539
diff changeset
   110
              else
b9e2ed4b1579 custom ListCellRenderer with text area font ensures that symbols are displayed reliably;
wenzelm
parents: 47539
diff changeset
   111
                new SideKickCompletion(pane.getView, word, ds.toArray.asInstanceOf[Array[Object]]) {
b9e2ed4b1579 custom ListCellRenderer with text area font ensures that symbols are displayed reliably;
wenzelm
parents: 47539
diff changeset
   112
                  override def getRenderer() =
47749
936df5d02dc9 reactivated ListCellRenderer for Java 6 (cf. b9e2ed4b1579, 0ddac15782e4, de249b5ae6e2);
wenzelm
parents: 47591
diff changeset
   113
                    new ListCellRenderer {
936df5d02dc9 reactivated ListCellRenderer for Java 6 (cf. b9e2ed4b1579, 0ddac15782e4, de249b5ae6e2);
wenzelm
parents: 47591
diff changeset
   114
                      val default_renderer = new DefaultListCellRenderer
47589
b9e2ed4b1579 custom ListCellRenderer with text area font ensures that symbols are displayed reliably;
wenzelm
parents: 47539
diff changeset
   115
b9e2ed4b1579 custom ListCellRenderer with text area font ensures that symbols are displayed reliably;
wenzelm
parents: 47539
diff changeset
   116
                      override def getListCellRendererComponent(
47749
936df5d02dc9 reactivated ListCellRenderer for Java 6 (cf. b9e2ed4b1579, 0ddac15782e4, de249b5ae6e2);
wenzelm
parents: 47591
diff changeset
   117
                          list: JList, value: Any, index: Int,
47589
b9e2ed4b1579 custom ListCellRenderer with text area font ensures that symbols are displayed reliably;
wenzelm
parents: 47539
diff changeset
   118
                          selected: Boolean, focus: Boolean): Component =
b9e2ed4b1579 custom ListCellRenderer with text area font ensures that symbols are displayed reliably;
wenzelm
parents: 47539
diff changeset
   119
                      {
b9e2ed4b1579 custom ListCellRenderer with text area font ensures that symbols are displayed reliably;
wenzelm
parents: 47539
diff changeset
   120
                        val renderer: Component =
b9e2ed4b1579 custom ListCellRenderer with text area font ensures that symbols are displayed reliably;
wenzelm
parents: 47539
diff changeset
   121
                          default_renderer.getListCellRendererComponent(
b9e2ed4b1579 custom ListCellRenderer with text area font ensures that symbols are displayed reliably;
wenzelm
parents: 47539
diff changeset
   122
                            list, value, index, selected, focus)
b9e2ed4b1579 custom ListCellRenderer with text area font ensures that symbols are displayed reliably;
wenzelm
parents: 47539
diff changeset
   123
                        renderer.setFont(pane.getTextArea.getPainter.getFont)
b9e2ed4b1579 custom ListCellRenderer with text area font ensures that symbols are displayed reliably;
wenzelm
parents: 47539
diff changeset
   124
                        renderer
b9e2ed4b1579 custom ListCellRenderer with text area font ensures that symbols are displayed reliably;
wenzelm
parents: 47539
diff changeset
   125
                      }
b9e2ed4b1579 custom ListCellRenderer with text area font ensures that symbols are displayed reliably;
wenzelm
parents: 47539
diff changeset
   126
                    }
b9e2ed4b1579 custom ListCellRenderer with text area font ensures that symbols are displayed reliably;
wenzelm
parents: 47539
diff changeset
   127
                }
39624
57496c868dcc tuned Isabelle_Sidekick.complete: lock buffer, depend on document model;
wenzelm
parents: 38663
diff changeset
   128
          }
57496c868dcc tuned Isabelle_Sidekick.complete: lock buffer, depend on document model;
wenzelm
parents: 38663
diff changeset
   129
      }
34611
b40e43d70ae9 use isabelle.Completion;
wenzelm
parents: 34609
diff changeset
   130
    }
34609
7ca1ef2f150d simplified and reactivated SideKickCompletion, cf. org.gjt.sp.jedit.gui.CompleteWord;
wenzelm
parents: 34562
diff changeset
   131
  }
34393
f0e1608a774f basic tree structure for sidekick
immler@in.tum.de
parents:
diff changeset
   132
}
36738
dce592144219 support several sidekick parsers -- very basic default parser;
wenzelm
parents: 36737
diff changeset
   133
dce592144219 support several sidekick parsers -- very basic default parser;
wenzelm
parents: 36737
diff changeset
   134
48718
73e6c22e2d94 more structural parsing for minor modes;
wenzelm
parents: 48717
diff changeset
   135
class Isabelle_Sidekick_Structure(
73e6c22e2d94 more structural parsing for minor modes;
wenzelm
parents: 48717
diff changeset
   136
    name: String,
73e6c22e2d94 more structural parsing for minor modes;
wenzelm
parents: 48717
diff changeset
   137
    get_syntax: => Option[Outer_Syntax],
73e6c22e2d94 more structural parsing for minor modes;
wenzelm
parents: 48717
diff changeset
   138
    node_name: Buffer => Option[Document.Node.Name])
73e6c22e2d94 more structural parsing for minor modes;
wenzelm
parents: 48717
diff changeset
   139
  extends Isabelle_Sidekick(name, get_syntax)
36759
wenzelm
parents: 36738
diff changeset
   140
{
40455
e035dad8eca2 default Sidekick parser based on section headings;
wenzelm
parents: 40452
diff changeset
   141
  import Thy_Syntax.Structure
e035dad8eca2 default Sidekick parser based on section headings;
wenzelm
parents: 40452
diff changeset
   142
48717
622251b2b0f1 clarified Sidekick configuration, including minor modes;
wenzelm
parents: 47749
diff changeset
   143
  override def parser(buffer: Buffer, syntax: Outer_Syntax, data: SideKickParsedData): Boolean =
36759
wenzelm
parents: 36738
diff changeset
   144
  {
40477
wenzelm
parents: 40475
diff changeset
   145
    def make_tree(offset: Text.Offset, entry: Structure.Entry): List[DefaultMutableTreeNode] =
40455
e035dad8eca2 default Sidekick parser based on section headings;
wenzelm
parents: 40452
diff changeset
   146
      entry match {
e035dad8eca2 default Sidekick parser based on section headings;
wenzelm
parents: 40452
diff changeset
   147
        case Structure.Block(name, body) =>
e035dad8eca2 default Sidekick parser based on section headings;
wenzelm
parents: 40452
diff changeset
   148
          val node =
e035dad8eca2 default Sidekick parser based on section headings;
wenzelm
parents: 40452
diff changeset
   149
            new DefaultMutableTreeNode(
40475
8a57ff2c2600 Sidekick block asset: show first line only;
wenzelm
parents: 40474
diff changeset
   150
              new Isabelle_Sidekick.Asset(Library.first_line(name), offset, offset + entry.length))
40455
e035dad8eca2 default Sidekick parser based on section headings;
wenzelm
parents: 40452
diff changeset
   151
          (offset /: body)((i, e) =>
e035dad8eca2 default Sidekick parser based on section headings;
wenzelm
parents: 40452
diff changeset
   152
            {
e035dad8eca2 default Sidekick parser based on section headings;
wenzelm
parents: 40452
diff changeset
   153
              make_tree(i, e) foreach (nd => node.add(nd))
e035dad8eca2 default Sidekick parser based on section headings;
wenzelm
parents: 40452
diff changeset
   154
              i + e.length
e035dad8eca2 default Sidekick parser based on section headings;
wenzelm
parents: 40452
diff changeset
   155
            })
e035dad8eca2 default Sidekick parser based on section headings;
wenzelm
parents: 40452
diff changeset
   156
          List(node)
e035dad8eca2 default Sidekick parser based on section headings;
wenzelm
parents: 40452
diff changeset
   157
        case Structure.Atom(command)
40458
12c8c64203b3 treat main theory commands like headings, and nest anything else inside;
wenzelm
parents: 40455
diff changeset
   158
        if command.is_command && syntax.heading_level(command).isEmpty =>
40455
e035dad8eca2 default Sidekick parser based on section headings;
wenzelm
parents: 40452
diff changeset
   159
          val node =
e035dad8eca2 default Sidekick parser based on section headings;
wenzelm
parents: 40452
diff changeset
   160
            new DefaultMutableTreeNode(
e035dad8eca2 default Sidekick parser based on section headings;
wenzelm
parents: 40452
diff changeset
   161
              new Isabelle_Sidekick.Asset(command.name, offset, offset + entry.length))
e035dad8eca2 default Sidekick parser based on section headings;
wenzelm
parents: 40452
diff changeset
   162
          List(node)
e035dad8eca2 default Sidekick parser based on section headings;
wenzelm
parents: 40452
diff changeset
   163
        case _ => Nil
e035dad8eca2 default Sidekick parser based on section headings;
wenzelm
parents: 40452
diff changeset
   164
      }
e035dad8eca2 default Sidekick parser based on section headings;
wenzelm
parents: 40452
diff changeset
   165
48718
73e6c22e2d94 more structural parsing for minor modes;
wenzelm
parents: 48717
diff changeset
   166
    node_name(buffer) match {
73e6c22e2d94 more structural parsing for minor modes;
wenzelm
parents: 48717
diff changeset
   167
      case Some(name) =>
48717
622251b2b0f1 clarified Sidekick configuration, including minor modes;
wenzelm
parents: 47749
diff changeset
   168
        val text = Isabelle.buffer_text(buffer)
48718
73e6c22e2d94 more structural parsing for minor modes;
wenzelm
parents: 48717
diff changeset
   169
        val structure = Structure.parse(syntax, name, text)
48717
622251b2b0f1 clarified Sidekick configuration, including minor modes;
wenzelm
parents: 47749
diff changeset
   170
        make_tree(0, structure) foreach (node => data.root.add(node))
622251b2b0f1 clarified Sidekick configuration, including minor modes;
wenzelm
parents: 47749
diff changeset
   171
        true
622251b2b0f1 clarified Sidekick configuration, including minor modes;
wenzelm
parents: 47749
diff changeset
   172
      case None => false
622251b2b0f1 clarified Sidekick configuration, including minor modes;
wenzelm
parents: 47749
diff changeset
   173
    }
36759
wenzelm
parents: 36738
diff changeset
   174
  }
wenzelm
parents: 36738
diff changeset
   175
}
36738
dce592144219 support several sidekick parsers -- very basic default parser;
wenzelm
parents: 36737
diff changeset
   176
dce592144219 support several sidekick parsers -- very basic default parser;
wenzelm
parents: 36737
diff changeset
   177
48718
73e6c22e2d94 more structural parsing for minor modes;
wenzelm
parents: 48717
diff changeset
   178
class Isabelle_Sidekick_Default extends Isabelle_Sidekick_Structure(
73e6c22e2d94 more structural parsing for minor modes;
wenzelm
parents: 48717
diff changeset
   179
  "isabelle", Isabelle.session.get_recent_syntax, Isabelle.buffer_node_name)
48717
622251b2b0f1 clarified Sidekick configuration, including minor modes;
wenzelm
parents: 47749
diff changeset
   180
622251b2b0f1 clarified Sidekick configuration, including minor modes;
wenzelm
parents: 47749
diff changeset
   181
48718
73e6c22e2d94 more structural parsing for minor modes;
wenzelm
parents: 48717
diff changeset
   182
class Isabelle_Sidekick_Options extends Isabelle_Sidekick_Structure(
73e6c22e2d94 more structural parsing for minor modes;
wenzelm
parents: 48717
diff changeset
   183
  "isabelle-options", Some(Options.options_syntax), Isabelle.buffer_node_dummy)
73e6c22e2d94 more structural parsing for minor modes;
wenzelm
parents: 48717
diff changeset
   184
73e6c22e2d94 more structural parsing for minor modes;
wenzelm
parents: 48717
diff changeset
   185
73e6c22e2d94 more structural parsing for minor modes;
wenzelm
parents: 48717
diff changeset
   186
class Isabelle_Sidekick_Root extends Isabelle_Sidekick_Structure(
73e6c22e2d94 more structural parsing for minor modes;
wenzelm
parents: 48717
diff changeset
   187
  "isabelle-root", Some(Build.root_syntax), Isabelle.buffer_node_dummy)
48717
622251b2b0f1 clarified Sidekick configuration, including minor modes;
wenzelm
parents: 47749
diff changeset
   188
622251b2b0f1 clarified Sidekick configuration, including minor modes;
wenzelm
parents: 47749
diff changeset
   189
622251b2b0f1 clarified Sidekick configuration, including minor modes;
wenzelm
parents: 47749
diff changeset
   190
class Isabelle_Sidekick_Raw
622251b2b0f1 clarified Sidekick configuration, including minor modes;
wenzelm
parents: 47749
diff changeset
   191
  extends Isabelle_Sidekick("isabelle-raw", Isabelle.session.get_recent_syntax)
36759
wenzelm
parents: 36738
diff changeset
   192
{
48717
622251b2b0f1 clarified Sidekick configuration, including minor modes;
wenzelm
parents: 47749
diff changeset
   193
  override def parser(buffer: Buffer, syntax: Outer_Syntax, data: SideKickParsedData): Boolean =
36759
wenzelm
parents: 36738
diff changeset
   194
  {
48717
622251b2b0f1 clarified Sidekick configuration, including minor modes;
wenzelm
parents: 47749
diff changeset
   195
    Swing_Thread.now { Document_Model(buffer).map(_.snapshot) } match {
622251b2b0f1 clarified Sidekick configuration, including minor modes;
wenzelm
parents: 47749
diff changeset
   196
      case Some(snapshot) =>
622251b2b0f1 clarified Sidekick configuration, including minor modes;
wenzelm
parents: 47749
diff changeset
   197
        val root = data.root
622251b2b0f1 clarified Sidekick configuration, including minor modes;
wenzelm
parents: 47749
diff changeset
   198
        for ((command, command_start) <- snapshot.node.command_range() if !stopped) {
622251b2b0f1 clarified Sidekick configuration, including minor modes;
wenzelm
parents: 47749
diff changeset
   199
          snapshot.state.command_state(snapshot.version, command).markup
622251b2b0f1 clarified Sidekick configuration, including minor modes;
wenzelm
parents: 47749
diff changeset
   200
            .swing_tree(root)((info: Text.Info[List[XML.Elem]]) =>
622251b2b0f1 clarified Sidekick configuration, including minor modes;
wenzelm
parents: 47749
diff changeset
   201
              {
622251b2b0f1 clarified Sidekick configuration, including minor modes;
wenzelm
parents: 47749
diff changeset
   202
                val range = info.range + command_start
622251b2b0f1 clarified Sidekick configuration, including minor modes;
wenzelm
parents: 47749
diff changeset
   203
                val content = command.source(info.range).replace('\n', ' ')
622251b2b0f1 clarified Sidekick configuration, including minor modes;
wenzelm
parents: 47749
diff changeset
   204
                val info_text =
622251b2b0f1 clarified Sidekick configuration, including minor modes;
wenzelm
parents: 47749
diff changeset
   205
                  Pretty.formatted(Library.separate(Pretty.FBreak, info.info), margin = 40).mkString
36738
dce592144219 support several sidekick parsers -- very basic default parser;
wenzelm
parents: 36737
diff changeset
   206
48717
622251b2b0f1 clarified Sidekick configuration, including minor modes;
wenzelm
parents: 47749
diff changeset
   207
                new DefaultMutableTreeNode(
622251b2b0f1 clarified Sidekick configuration, including minor modes;
wenzelm
parents: 47749
diff changeset
   208
                  new Isabelle_Sidekick.Asset(command.toString, range.start, range.stop) {
622251b2b0f1 clarified Sidekick configuration, including minor modes;
wenzelm
parents: 47749
diff changeset
   209
                    override def getShortString: String = content
622251b2b0f1 clarified Sidekick configuration, including minor modes;
wenzelm
parents: 47749
diff changeset
   210
                    override def getLongString: String = info_text
622251b2b0f1 clarified Sidekick configuration, including minor modes;
wenzelm
parents: 47749
diff changeset
   211
                    override def toString = quote(content) + " " + range.toString
622251b2b0f1 clarified Sidekick configuration, including minor modes;
wenzelm
parents: 47749
diff changeset
   212
                  })
40452
45e7c2889d2f misc tuning and simplification, using Isabelle_Sidekick.Asset (not sidekick.Asset, which is dynamically dispatched to slightly different semantics);
wenzelm
parents: 39624
diff changeset
   213
              })
48717
622251b2b0f1 clarified Sidekick configuration, including minor modes;
wenzelm
parents: 47749
diff changeset
   214
        }
622251b2b0f1 clarified Sidekick configuration, including minor modes;
wenzelm
parents: 47749
diff changeset
   215
        true
622251b2b0f1 clarified Sidekick configuration, including minor modes;
wenzelm
parents: 47749
diff changeset
   216
      case None => false
36759
wenzelm
parents: 36738
diff changeset
   217
    }
wenzelm
parents: 36738
diff changeset
   218
  }
wenzelm
parents: 36738
diff changeset
   219
}
36738
dce592144219 support several sidekick parsers -- very basic default parser;
wenzelm
parents: 36737
diff changeset
   220