src/Tools/jEdit/src/isabelle_sidekick.scala
author wenzelm
Sat, 06 Jul 2013 21:19:38 +0200
changeset 52539 7658f8d7b2dc
parent 51618 a3577cd80c41
child 53233 4b422e5d64fd
permissions -rw-r--r--
minimal jedit mode for Isabelle NEWS;
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
52539
7658f8d7b2dc minimal jedit mode for Isabelle NEWS;
wenzelm
parents: 51618
diff changeset
    15
import scala.util.matching.Regex
34417
bce2f2ea9819 misc tuning and adaption according to original IsabelleParser --
wenzelm
parents: 34408
diff changeset
    16
47589
b9e2ed4b1579 custom ListCellRenderer with text area font ensures that symbols are displayed reliably;
wenzelm
parents: 47539
diff changeset
    17
import java.awt.Component
34393
f0e1608a774f basic tree structure for sidekick
immler@in.tum.de
parents:
diff changeset
    18
import javax.swing.tree.DefaultMutableTreeNode
34701
80b0add08eef IsabelleSideKickParser: incorporate former MarkupNode.markup2default_node, observe stopped flag;
wenzelm
parents: 34669
diff changeset
    19
import javax.swing.text.Position
47589
b9e2ed4b1579 custom ListCellRenderer with text area font ensures that symbols are displayed reliably;
wenzelm
parents: 47539
diff changeset
    20
import javax.swing.{Icon, DefaultListCellRenderer, ListCellRenderer, JList}
34417
bce2f2ea9819 misc tuning and adaption according to original IsabelleParser --
wenzelm
parents: 34408
diff changeset
    21
34609
7ca1ef2f150d simplified and reactivated SideKickCompletion, cf. org.gjt.sp.jedit.gui.CompleteWord;
wenzelm
parents: 34562
diff changeset
    22
import org.gjt.sp.jedit.{Buffer, EditPane, TextUtilities, View}
34417
bce2f2ea9819 misc tuning and adaption according to original IsabelleParser --
wenzelm
parents: 34408
diff changeset
    23
import errorlist.DefaultErrorSource
50725
226a5b290c85 tuned imports;
wenzelm
parents: 50566
diff changeset
    24
import sidekick.{SideKickParser, SideKickParsedData, SideKickCompletion, 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
  }
51618
a3577cd80c41 tuned signature -- avoid intrusion of slightly odd Swing structures into pure Markup_Tree;
wenzelm
parents: 51493
diff changeset
    48
a3577cd80c41 tuned signature -- avoid intrusion of slightly odd Swing structures into pure Markup_Tree;
wenzelm
parents: 51493
diff changeset
    49
  def swing_markup_tree(tree: Markup_Tree, parent: DefaultMutableTreeNode,
a3577cd80c41 tuned signature -- avoid intrusion of slightly odd Swing structures into pure Markup_Tree;
wenzelm
parents: 51493
diff changeset
    50
    swing_node: Text.Info[List[XML.Elem]] => DefaultMutableTreeNode)
a3577cd80c41 tuned signature -- avoid intrusion of slightly odd Swing structures into pure Markup_Tree;
wenzelm
parents: 51493
diff changeset
    51
  {
a3577cd80c41 tuned signature -- avoid intrusion of slightly odd Swing structures into pure Markup_Tree;
wenzelm
parents: 51493
diff changeset
    52
    for ((_, entry) <- tree.branches) {
a3577cd80c41 tuned signature -- avoid intrusion of slightly odd Swing structures into pure Markup_Tree;
wenzelm
parents: 51493
diff changeset
    53
      val node = swing_node(Text.Info(entry.range, entry.markup))
a3577cd80c41 tuned signature -- avoid intrusion of slightly odd Swing structures into pure Markup_Tree;
wenzelm
parents: 51493
diff changeset
    54
      swing_markup_tree(entry.subtree, node, swing_node)
a3577cd80c41 tuned signature -- avoid intrusion of slightly odd Swing structures into pure Markup_Tree;
wenzelm
parents: 51493
diff changeset
    55
      parent.add(node)
a3577cd80c41 tuned signature -- avoid intrusion of slightly odd Swing structures into pure Markup_Tree;
wenzelm
parents: 51493
diff changeset
    56
    }
a3577cd80c41 tuned signature -- avoid intrusion of slightly odd Swing structures into pure Markup_Tree;
wenzelm
parents: 51493
diff changeset
    57
  }
36738
dce592144219 support several sidekick parsers -- very basic default parser;
wenzelm
parents: 36737
diff changeset
    58
}
dce592144219 support several sidekick parsers -- very basic default parser;
wenzelm
parents: 36737
diff changeset
    59
dce592144219 support several sidekick parsers -- very basic default parser;
wenzelm
parents: 36737
diff changeset
    60
48717
622251b2b0f1 clarified Sidekick configuration, including minor modes;
wenzelm
parents: 47749
diff changeset
    61
class Isabelle_Sidekick(name: String, get_syntax: => Option[Outer_Syntax])
622251b2b0f1 clarified Sidekick configuration, including minor modes;
wenzelm
parents: 47749
diff changeset
    62
  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
    63
{
34417
bce2f2ea9819 misc tuning and adaption according to original IsabelleParser --
wenzelm
parents: 34408
diff changeset
    64
  /* parsing */
bce2f2ea9819 misc tuning and adaption according to original IsabelleParser --
wenzelm
parents: 34408
diff changeset
    65
36759
wenzelm
parents: 36738
diff changeset
    66
  @volatile protected var stopped = false
34503
7d0726f19d04 tuned whitespace;
wenzelm
parents: 34485
diff changeset
    67
  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
    68
48717
622251b2b0f1 clarified Sidekick configuration, including minor modes;
wenzelm
parents: 47749
diff changeset
    69
  def parser(buffer: Buffer, syntax: Outer_Syntax, data: SideKickParsedData): Boolean = false
36759
wenzelm
parents: 36738
diff changeset
    70
34625
799a40faa4f1 completion: decode symbols only if isabelle encoding is active (to prevent unicode chars written back to file);
wenzelm
parents: 34612
diff changeset
    71
  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
    72
  {
34417
bce2f2ea9819 misc tuning and adaption according to original IsabelleParser --
wenzelm
parents: 34408
diff changeset
    73
    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
    74
38640
105d1f112da5 sporadic locking of jEdit buffer;
wenzelm
parents: 38577
diff changeset
    75
    // FIXME lock buffer (!??)
34417
bce2f2ea9819 misc tuning and adaption according to original IsabelleParser --
wenzelm
parents: 34408
diff changeset
    76
    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
    77
    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
    78
    data.getAsset(root).setEnd(Isabelle_Sidekick.int_to_pos(buffer.getLength))
34475
f963335dbc6b implemented IsabelleSideKickParser.complete
immler@in.tum.de
parents: 34440
diff changeset
    79
48717
622251b2b0f1 clarified Sidekick configuration, including minor modes;
wenzelm
parents: 47749
diff changeset
    80
    val syntax = get_syntax
622251b2b0f1 clarified Sidekick configuration, including minor modes;
wenzelm
parents: 47749
diff changeset
    81
    val ok =
622251b2b0f1 clarified Sidekick configuration, including minor modes;
wenzelm
parents: 47749
diff changeset
    82
      if (syntax.isDefined) {
622251b2b0f1 clarified Sidekick configuration, including minor modes;
wenzelm
parents: 47749
diff changeset
    83
        val ok = parser(buffer, syntax.get, data)
622251b2b0f1 clarified Sidekick configuration, including minor modes;
wenzelm
parents: 47749
diff changeset
    84
        if (stopped) { root.add(new DefaultMutableTreeNode("<stopped>")); true }
622251b2b0f1 clarified Sidekick configuration, including minor modes;
wenzelm
parents: 47749
diff changeset
    85
        else ok
622251b2b0f1 clarified Sidekick configuration, including minor modes;
wenzelm
parents: 47749
diff changeset
    86
      }
622251b2b0f1 clarified Sidekick configuration, including minor modes;
wenzelm
parents: 47749
diff changeset
    87
      else false
622251b2b0f1 clarified Sidekick configuration, including minor modes;
wenzelm
parents: 47749
diff changeset
    88
    if (!ok) root.add(new DefaultMutableTreeNode("<ignored>"))
622251b2b0f1 clarified Sidekick configuration, including minor modes;
wenzelm
parents: 47749
diff changeset
    89
34417
bce2f2ea9819 misc tuning and adaption according to original IsabelleParser --
wenzelm
parents: 34408
diff changeset
    90
    data
bce2f2ea9819 misc tuning and adaption according to original IsabelleParser --
wenzelm
parents: 34408
diff changeset
    91
  }
bce2f2ea9819 misc tuning and adaption according to original IsabelleParser --
wenzelm
parents: 34408
diff changeset
    92
36738
dce592144219 support several sidekick parsers -- very basic default parser;
wenzelm
parents: 36737
diff changeset
    93
34417
bce2f2ea9819 misc tuning and adaption according to original IsabelleParser --
wenzelm
parents: 34408
diff changeset
    94
  /* completion */
bce2f2ea9819 misc tuning and adaption according to original IsabelleParser --
wenzelm
parents: 34408
diff changeset
    95
bce2f2ea9819 misc tuning and adaption according to original IsabelleParser --
wenzelm
parents: 34408
diff changeset
    96
  override def supportsCompletion = true
bce2f2ea9819 misc tuning and adaption according to original IsabelleParser --
wenzelm
parents: 34408
diff changeset
    97
  override def canCompleteAnywhere = true
bce2f2ea9819 misc tuning and adaption according to original IsabelleParser --
wenzelm
parents: 34408
diff changeset
    98
40477
wenzelm
parents: 40475
diff changeset
    99
  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
   100
  {
46920
5f44c8bea84e more explicit indication of swing thread context;
wenzelm
parents: 46208
diff changeset
   101
    Swing_Thread.assert()
5f44c8bea84e more explicit indication of swing thread context;
wenzelm
parents: 46208
diff changeset
   102
34475
f963335dbc6b implemented IsabelleSideKickParser.complete
immler@in.tum.de
parents: 34440
diff changeset
   103
    val buffer = pane.getBuffer
49406
38db4832b210 somewhat more general JEdit_Lib;
wenzelm
parents: 48884
diff changeset
   104
    JEdit_Lib.buffer_lock(buffer) {
48717
622251b2b0f1 clarified Sidekick configuration, including minor modes;
wenzelm
parents: 47749
diff changeset
   105
      get_syntax match {
39624
57496c868dcc tuned Isabelle_Sidekick.complete: lock buffer, depend on document model;
wenzelm
parents: 38663
diff changeset
   106
        case None => null
48717
622251b2b0f1 clarified Sidekick configuration, including minor modes;
wenzelm
parents: 47749
diff changeset
   107
        case Some(syntax) =>
39624
57496c868dcc tuned Isabelle_Sidekick.complete: lock buffer, depend on document model;
wenzelm
parents: 38663
diff changeset
   108
          val line = buffer.getLineOfOffset(caret)
57496c868dcc tuned Isabelle_Sidekick.complete: lock buffer, depend on document model;
wenzelm
parents: 38663
diff changeset
   109
          val start = buffer.getLineStartOffset(line)
57496c868dcc tuned Isabelle_Sidekick.complete: lock buffer, depend on document model;
wenzelm
parents: 38663
diff changeset
   110
          val text = buffer.getSegment(start, caret - start)
34475
f963335dbc6b implemented IsabelleSideKickParser.complete
immler@in.tum.de
parents: 34440
diff changeset
   111
48717
622251b2b0f1 clarified Sidekick configuration, including minor modes;
wenzelm
parents: 47749
diff changeset
   112
          syntax.completion.complete(text) match {
39624
57496c868dcc tuned Isabelle_Sidekick.complete: lock buffer, depend on document model;
wenzelm
parents: 38663
diff changeset
   113
            case None => null
57496c868dcc tuned Isabelle_Sidekick.complete: lock buffer, depend on document model;
wenzelm
parents: 38663
diff changeset
   114
            case Some((word, cs)) =>
57496c868dcc tuned Isabelle_Sidekick.complete: lock buffer, depend on document model;
wenzelm
parents: 38663
diff changeset
   115
              val ds =
57496c868dcc tuned Isabelle_Sidekick.complete: lock buffer, depend on document model;
wenzelm
parents: 38663
diff changeset
   116
                (if (Isabelle_Encoding.is_active(buffer))
45900
793bf5fa5fbf prefer sorting from Scala library;
wenzelm
parents: 45455
diff changeset
   117
                  cs.map(Symbol.decode(_)).sorted
39624
57496c868dcc tuned Isabelle_Sidekick.complete: lock buffer, depend on document model;
wenzelm
parents: 38663
diff changeset
   118
                 else cs).filter(_ != word)
57496c868dcc tuned Isabelle_Sidekick.complete: lock buffer, depend on document model;
wenzelm
parents: 38663
diff changeset
   119
              if (ds.isEmpty) null
47589
b9e2ed4b1579 custom ListCellRenderer with text area font ensures that symbols are displayed reliably;
wenzelm
parents: 47539
diff changeset
   120
              else
b9e2ed4b1579 custom ListCellRenderer with text area font ensures that symbols are displayed reliably;
wenzelm
parents: 47539
diff changeset
   121
                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
   122
                  override def getRenderer() =
48826
b19ba23e70c5 updated to jdk-7u6 and jedit_build-20120813 -- NB: plain Isabelle/Scala still happens to work with jdk-6;
wenzelm
parents: 48718
diff changeset
   123
                    new ListCellRenderer[Any] {
b19ba23e70c5 updated to jdk-7u6 and jedit_build-20120813 -- NB: plain Isabelle/Scala still happens to work with jdk-6;
wenzelm
parents: 48718
diff changeset
   124
                      val default_renderer =
b19ba23e70c5 updated to jdk-7u6 and jedit_build-20120813 -- NB: plain Isabelle/Scala still happens to work with jdk-6;
wenzelm
parents: 48718
diff changeset
   125
                        (new DefaultListCellRenderer).asInstanceOf[ListCellRenderer[Any]]
47589
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
                      override def getListCellRendererComponent(
48826
b19ba23e70c5 updated to jdk-7u6 and jedit_build-20120813 -- NB: plain Isabelle/Scala still happens to work with jdk-6;
wenzelm
parents: 48718
diff changeset
   128
                          list: JList[_ <: Any], value: Any, index: Int,
47589
b9e2ed4b1579 custom ListCellRenderer with text area font ensures that symbols are displayed reliably;
wenzelm
parents: 47539
diff changeset
   129
                          selected: Boolean, focus: Boolean): Component =
b9e2ed4b1579 custom ListCellRenderer with text area font ensures that symbols are displayed reliably;
wenzelm
parents: 47539
diff changeset
   130
                      {
b9e2ed4b1579 custom ListCellRenderer with text area font ensures that symbols are displayed reliably;
wenzelm
parents: 47539
diff changeset
   131
                        val renderer: Component =
b9e2ed4b1579 custom ListCellRenderer with text area font ensures that symbols are displayed reliably;
wenzelm
parents: 47539
diff changeset
   132
                          default_renderer.getListCellRendererComponent(
b9e2ed4b1579 custom ListCellRenderer with text area font ensures that symbols are displayed reliably;
wenzelm
parents: 47539
diff changeset
   133
                            list, value, index, selected, focus)
b9e2ed4b1579 custom ListCellRenderer with text area font ensures that symbols are displayed reliably;
wenzelm
parents: 47539
diff changeset
   134
                        renderer.setFont(pane.getTextArea.getPainter.getFont)
b9e2ed4b1579 custom ListCellRenderer with text area font ensures that symbols are displayed reliably;
wenzelm
parents: 47539
diff changeset
   135
                        renderer
b9e2ed4b1579 custom ListCellRenderer with text area font ensures that symbols are displayed reliably;
wenzelm
parents: 47539
diff changeset
   136
                      }
b9e2ed4b1579 custom ListCellRenderer with text area font ensures that symbols are displayed reliably;
wenzelm
parents: 47539
diff changeset
   137
                    }
b9e2ed4b1579 custom ListCellRenderer with text area font ensures that symbols are displayed reliably;
wenzelm
parents: 47539
diff changeset
   138
                }
39624
57496c868dcc tuned Isabelle_Sidekick.complete: lock buffer, depend on document model;
wenzelm
parents: 38663
diff changeset
   139
          }
57496c868dcc tuned Isabelle_Sidekick.complete: lock buffer, depend on document model;
wenzelm
parents: 38663
diff changeset
   140
      }
34611
b40e43d70ae9 use isabelle.Completion;
wenzelm
parents: 34609
diff changeset
   141
    }
34609
7ca1ef2f150d simplified and reactivated SideKickCompletion, cf. org.gjt.sp.jedit.gui.CompleteWord;
wenzelm
parents: 34562
diff changeset
   142
  }
34393
f0e1608a774f basic tree structure for sidekick
immler@in.tum.de
parents:
diff changeset
   143
}
36738
dce592144219 support several sidekick parsers -- very basic default parser;
wenzelm
parents: 36737
diff changeset
   144
dce592144219 support several sidekick parsers -- very basic default parser;
wenzelm
parents: 36737
diff changeset
   145
48718
73e6c22e2d94 more structural parsing for minor modes;
wenzelm
parents: 48717
diff changeset
   146
class Isabelle_Sidekick_Structure(
73e6c22e2d94 more structural parsing for minor modes;
wenzelm
parents: 48717
diff changeset
   147
    name: String,
73e6c22e2d94 more structural parsing for minor modes;
wenzelm
parents: 48717
diff changeset
   148
    get_syntax: => Option[Outer_Syntax],
73e6c22e2d94 more structural parsing for minor modes;
wenzelm
parents: 48717
diff changeset
   149
    node_name: Buffer => Option[Document.Node.Name])
73e6c22e2d94 more structural parsing for minor modes;
wenzelm
parents: 48717
diff changeset
   150
  extends Isabelle_Sidekick(name, get_syntax)
36759
wenzelm
parents: 36738
diff changeset
   151
{
40455
e035dad8eca2 default Sidekick parser based on section headings;
wenzelm
parents: 40452
diff changeset
   152
  import Thy_Syntax.Structure
e035dad8eca2 default Sidekick parser based on section headings;
wenzelm
parents: 40452
diff changeset
   153
48717
622251b2b0f1 clarified Sidekick configuration, including minor modes;
wenzelm
parents: 47749
diff changeset
   154
  override def parser(buffer: Buffer, syntax: Outer_Syntax, data: SideKickParsedData): Boolean =
36759
wenzelm
parents: 36738
diff changeset
   155
  {
40477
wenzelm
parents: 40475
diff changeset
   156
    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
   157
      entry match {
e035dad8eca2 default Sidekick parser based on section headings;
wenzelm
parents: 40452
diff changeset
   158
        case Structure.Block(name, body) =>
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(
40475
8a57ff2c2600 Sidekick block asset: show first line only;
wenzelm
parents: 40474
diff changeset
   161
              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
   162
          (offset /: body)((i, e) =>
e035dad8eca2 default Sidekick parser based on section headings;
wenzelm
parents: 40452
diff changeset
   163
            {
e035dad8eca2 default Sidekick parser based on section headings;
wenzelm
parents: 40452
diff changeset
   164
              make_tree(i, e) foreach (nd => node.add(nd))
e035dad8eca2 default Sidekick parser based on section headings;
wenzelm
parents: 40452
diff changeset
   165
              i + e.length
e035dad8eca2 default Sidekick parser based on section headings;
wenzelm
parents: 40452
diff changeset
   166
            })
e035dad8eca2 default Sidekick parser based on section headings;
wenzelm
parents: 40452
diff changeset
   167
          List(node)
e035dad8eca2 default Sidekick parser based on section headings;
wenzelm
parents: 40452
diff changeset
   168
        case Structure.Atom(command)
40458
12c8c64203b3 treat main theory commands like headings, and nest anything else inside;
wenzelm
parents: 40455
diff changeset
   169
        if command.is_command && syntax.heading_level(command).isEmpty =>
40455
e035dad8eca2 default Sidekick parser based on section headings;
wenzelm
parents: 40452
diff changeset
   170
          val node =
e035dad8eca2 default Sidekick parser based on section headings;
wenzelm
parents: 40452
diff changeset
   171
            new DefaultMutableTreeNode(
e035dad8eca2 default Sidekick parser based on section headings;
wenzelm
parents: 40452
diff changeset
   172
              new Isabelle_Sidekick.Asset(command.name, offset, offset + entry.length))
e035dad8eca2 default Sidekick parser based on section headings;
wenzelm
parents: 40452
diff changeset
   173
          List(node)
e035dad8eca2 default Sidekick parser based on section headings;
wenzelm
parents: 40452
diff changeset
   174
        case _ => Nil
e035dad8eca2 default Sidekick parser based on section headings;
wenzelm
parents: 40452
diff changeset
   175
      }
e035dad8eca2 default Sidekick parser based on section headings;
wenzelm
parents: 40452
diff changeset
   176
48718
73e6c22e2d94 more structural parsing for minor modes;
wenzelm
parents: 48717
diff changeset
   177
    node_name(buffer) match {
73e6c22e2d94 more structural parsing for minor modes;
wenzelm
parents: 48717
diff changeset
   178
      case Some(name) =>
49406
38db4832b210 somewhat more general JEdit_Lib;
wenzelm
parents: 48884
diff changeset
   179
        val text = JEdit_Lib.buffer_text(buffer)
48718
73e6c22e2d94 more structural parsing for minor modes;
wenzelm
parents: 48717
diff changeset
   180
        val structure = Structure.parse(syntax, name, text)
48717
622251b2b0f1 clarified Sidekick configuration, including minor modes;
wenzelm
parents: 47749
diff changeset
   181
        make_tree(0, structure) foreach (node => data.root.add(node))
622251b2b0f1 clarified Sidekick configuration, including minor modes;
wenzelm
parents: 47749
diff changeset
   182
        true
622251b2b0f1 clarified Sidekick configuration, including minor modes;
wenzelm
parents: 47749
diff changeset
   183
      case None => false
622251b2b0f1 clarified Sidekick configuration, including minor modes;
wenzelm
parents: 47749
diff changeset
   184
    }
36759
wenzelm
parents: 36738
diff changeset
   185
  }
wenzelm
parents: 36738
diff changeset
   186
}
36738
dce592144219 support several sidekick parsers -- very basic default parser;
wenzelm
parents: 36737
diff changeset
   187
dce592144219 support several sidekick parsers -- very basic default parser;
wenzelm
parents: 36737
diff changeset
   188
48718
73e6c22e2d94 more structural parsing for minor modes;
wenzelm
parents: 48717
diff changeset
   189
class Isabelle_Sidekick_Default extends Isabelle_Sidekick_Structure(
50566
b43c4f660320 tuned signature: use thy_load to adapt to prover/editor specific view on sources;
wenzelm
parents: 50205
diff changeset
   190
  "isabelle", PIDE.get_recent_syntax, PIDE.thy_load.buffer_node_name)
48717
622251b2b0f1 clarified Sidekick configuration, including minor modes;
wenzelm
parents: 47749
diff changeset
   191
622251b2b0f1 clarified Sidekick configuration, including minor modes;
wenzelm
parents: 47749
diff changeset
   192
48718
73e6c22e2d94 more structural parsing for minor modes;
wenzelm
parents: 48717
diff changeset
   193
class Isabelle_Sidekick_Options extends Isabelle_Sidekick_Structure(
50566
b43c4f660320 tuned signature: use thy_load to adapt to prover/editor specific view on sources;
wenzelm
parents: 50205
diff changeset
   194
  "isabelle-options", Some(Options.options_syntax), PIDE.thy_load.buffer_node_dummy)
48718
73e6c22e2d94 more structural parsing for minor modes;
wenzelm
parents: 48717
diff changeset
   195
73e6c22e2d94 more structural parsing for minor modes;
wenzelm
parents: 48717
diff changeset
   196
73e6c22e2d94 more structural parsing for minor modes;
wenzelm
parents: 48717
diff changeset
   197
class Isabelle_Sidekick_Root extends Isabelle_Sidekick_Structure(
50566
b43c4f660320 tuned signature: use thy_load to adapt to prover/editor specific view on sources;
wenzelm
parents: 50205
diff changeset
   198
  "isabelle-root", Some(Build.root_syntax), PIDE.thy_load.buffer_node_dummy)
48717
622251b2b0f1 clarified Sidekick configuration, including minor modes;
wenzelm
parents: 47749
diff changeset
   199
622251b2b0f1 clarified Sidekick configuration, including minor modes;
wenzelm
parents: 47749
diff changeset
   200
50205
788c8263e634 renamed main plugin object to PIDE;
wenzelm
parents: 49465
diff changeset
   201
class Isabelle_Sidekick_Raw extends Isabelle_Sidekick("isabelle-raw", PIDE.get_recent_syntax)
36759
wenzelm
parents: 36738
diff changeset
   202
{
48717
622251b2b0f1 clarified Sidekick configuration, including minor modes;
wenzelm
parents: 47749
diff changeset
   203
  override def parser(buffer: Buffer, syntax: Outer_Syntax, data: SideKickParsedData): Boolean =
36759
wenzelm
parents: 36738
diff changeset
   204
  {
48717
622251b2b0f1 clarified Sidekick configuration, including minor modes;
wenzelm
parents: 47749
diff changeset
   205
    Swing_Thread.now { Document_Model(buffer).map(_.snapshot) } match {
622251b2b0f1 clarified Sidekick configuration, including minor modes;
wenzelm
parents: 47749
diff changeset
   206
      case Some(snapshot) =>
622251b2b0f1 clarified Sidekick configuration, including minor modes;
wenzelm
parents: 47749
diff changeset
   207
        val root = data.root
622251b2b0f1 clarified Sidekick configuration, including minor modes;
wenzelm
parents: 47749
diff changeset
   208
        for ((command, command_start) <- snapshot.node.command_range() if !stopped) {
51618
a3577cd80c41 tuned signature -- avoid intrusion of slightly odd Swing structures into pure Markup_Tree;
wenzelm
parents: 51493
diff changeset
   209
          Isabelle_Sidekick.swing_markup_tree(
a3577cd80c41 tuned signature -- avoid intrusion of slightly odd Swing structures into pure Markup_Tree;
wenzelm
parents: 51493
diff changeset
   210
            snapshot.state.command_state(snapshot.version, command).markup, root,
a3577cd80c41 tuned signature -- avoid intrusion of slightly odd Swing structures into pure Markup_Tree;
wenzelm
parents: 51493
diff changeset
   211
              (info: Text.Info[List[XML.Elem]]) =>
48717
622251b2b0f1 clarified Sidekick configuration, including minor modes;
wenzelm
parents: 47749
diff changeset
   212
              {
622251b2b0f1 clarified Sidekick configuration, including minor modes;
wenzelm
parents: 47749
diff changeset
   213
                val range = info.range + command_start
622251b2b0f1 clarified Sidekick configuration, including minor modes;
wenzelm
parents: 47749
diff changeset
   214
                val content = command.source(info.range).replace('\n', ' ')
622251b2b0f1 clarified Sidekick configuration, including minor modes;
wenzelm
parents: 47749
diff changeset
   215
                val info_text =
51493
59d8a1031c00 allow fractional pretty margin -- avoid premature rounding;
wenzelm
parents: 50725
diff changeset
   216
                  Pretty.formatted(Library.separate(Pretty.FBreak, info.info), margin = 40.0)
59d8a1031c00 allow fractional pretty margin -- avoid premature rounding;
wenzelm
parents: 50725
diff changeset
   217
                    .mkString
36738
dce592144219 support several sidekick parsers -- very basic default parser;
wenzelm
parents: 36737
diff changeset
   218
48717
622251b2b0f1 clarified Sidekick configuration, including minor modes;
wenzelm
parents: 47749
diff changeset
   219
                new DefaultMutableTreeNode(
622251b2b0f1 clarified Sidekick configuration, including minor modes;
wenzelm
parents: 47749
diff changeset
   220
                  new Isabelle_Sidekick.Asset(command.toString, range.start, range.stop) {
622251b2b0f1 clarified Sidekick configuration, including minor modes;
wenzelm
parents: 47749
diff changeset
   221
                    override def getShortString: String = content
622251b2b0f1 clarified Sidekick configuration, including minor modes;
wenzelm
parents: 47749
diff changeset
   222
                    override def getLongString: String = info_text
622251b2b0f1 clarified Sidekick configuration, including minor modes;
wenzelm
parents: 47749
diff changeset
   223
                    override def toString = quote(content) + " " + range.toString
622251b2b0f1 clarified Sidekick configuration, including minor modes;
wenzelm
parents: 47749
diff changeset
   224
                  })
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
   225
              })
48717
622251b2b0f1 clarified Sidekick configuration, including minor modes;
wenzelm
parents: 47749
diff changeset
   226
        }
622251b2b0f1 clarified Sidekick configuration, including minor modes;
wenzelm
parents: 47749
diff changeset
   227
        true
622251b2b0f1 clarified Sidekick configuration, including minor modes;
wenzelm
parents: 47749
diff changeset
   228
      case None => false
36759
wenzelm
parents: 36738
diff changeset
   229
    }
wenzelm
parents: 36738
diff changeset
   230
  }
wenzelm
parents: 36738
diff changeset
   231
}
36738
dce592144219 support several sidekick parsers -- very basic default parser;
wenzelm
parents: 36737
diff changeset
   232
52539
7658f8d7b2dc minimal jedit mode for Isabelle NEWS;
wenzelm
parents: 51618
diff changeset
   233
7658f8d7b2dc minimal jedit mode for Isabelle NEWS;
wenzelm
parents: 51618
diff changeset
   234
class Isabelle_Sidekick_News extends Isabelle_Sidekick("isabelle-news", Some(Outer_Syntax.empty))
7658f8d7b2dc minimal jedit mode for Isabelle NEWS;
wenzelm
parents: 51618
diff changeset
   235
{
7658f8d7b2dc minimal jedit mode for Isabelle NEWS;
wenzelm
parents: 51618
diff changeset
   236
  private val Heading1 = new Regex("""^New in (.*)\w*$""")
7658f8d7b2dc minimal jedit mode for Isabelle NEWS;
wenzelm
parents: 51618
diff changeset
   237
  private val Heading2 = new Regex("""^\*\*\*\w*(.*)\w*\*\*\*\w*$""")
7658f8d7b2dc minimal jedit mode for Isabelle NEWS;
wenzelm
parents: 51618
diff changeset
   238
7658f8d7b2dc minimal jedit mode for Isabelle NEWS;
wenzelm
parents: 51618
diff changeset
   239
  private def make_node(s: String, start: Text.Offset, stop: Text.Offset): DefaultMutableTreeNode =
7658f8d7b2dc minimal jedit mode for Isabelle NEWS;
wenzelm
parents: 51618
diff changeset
   240
    new DefaultMutableTreeNode(new Isabelle_Sidekick.Asset(s, start, stop))
7658f8d7b2dc minimal jedit mode for Isabelle NEWS;
wenzelm
parents: 51618
diff changeset
   241
7658f8d7b2dc minimal jedit mode for Isabelle NEWS;
wenzelm
parents: 51618
diff changeset
   242
  override def parser(buffer: Buffer, syntax: Outer_Syntax, data: SideKickParsedData): Boolean =
7658f8d7b2dc minimal jedit mode for Isabelle NEWS;
wenzelm
parents: 51618
diff changeset
   243
  {
7658f8d7b2dc minimal jedit mode for Isabelle NEWS;
wenzelm
parents: 51618
diff changeset
   244
    var offset = 0
7658f8d7b2dc minimal jedit mode for Isabelle NEWS;
wenzelm
parents: 51618
diff changeset
   245
7658f8d7b2dc minimal jedit mode for Isabelle NEWS;
wenzelm
parents: 51618
diff changeset
   246
    for (line <- split_lines(JEdit_Lib.buffer_text(buffer)) if !stopped) {
7658f8d7b2dc minimal jedit mode for Isabelle NEWS;
wenzelm
parents: 51618
diff changeset
   247
      line match {
7658f8d7b2dc minimal jedit mode for Isabelle NEWS;
wenzelm
parents: 51618
diff changeset
   248
        case Heading1(s) =>
7658f8d7b2dc minimal jedit mode for Isabelle NEWS;
wenzelm
parents: 51618
diff changeset
   249
          data.root.add(make_node(Library.capitalize(s), offset, offset + line.length))
7658f8d7b2dc minimal jedit mode for Isabelle NEWS;
wenzelm
parents: 51618
diff changeset
   250
        case Heading2(s) =>
7658f8d7b2dc minimal jedit mode for Isabelle NEWS;
wenzelm
parents: 51618
diff changeset
   251
          data.root.getLastChild.asInstanceOf[DefaultMutableTreeNode]
7658f8d7b2dc minimal jedit mode for Isabelle NEWS;
wenzelm
parents: 51618
diff changeset
   252
            .add(make_node(s, offset, offset + line.length))
7658f8d7b2dc minimal jedit mode for Isabelle NEWS;
wenzelm
parents: 51618
diff changeset
   253
        case _ =>
7658f8d7b2dc minimal jedit mode for Isabelle NEWS;
wenzelm
parents: 51618
diff changeset
   254
      }
7658f8d7b2dc minimal jedit mode for Isabelle NEWS;
wenzelm
parents: 51618
diff changeset
   255
      offset += line.length + 1
7658f8d7b2dc minimal jedit mode for Isabelle NEWS;
wenzelm
parents: 51618
diff changeset
   256
    }
7658f8d7b2dc minimal jedit mode for Isabelle NEWS;
wenzelm
parents: 51618
diff changeset
   257
7658f8d7b2dc minimal jedit mode for Isabelle NEWS;
wenzelm
parents: 51618
diff changeset
   258
    true
7658f8d7b2dc minimal jedit mode for Isabelle NEWS;
wenzelm
parents: 51618
diff changeset
   259
  }
7658f8d7b2dc minimal jedit mode for Isabelle NEWS;
wenzelm
parents: 51618
diff changeset
   260
7658f8d7b2dc minimal jedit mode for Isabelle NEWS;
wenzelm
parents: 51618
diff changeset
   261
  override def supportsCompletion = false
7658f8d7b2dc minimal jedit mode for Isabelle NEWS;
wenzelm
parents: 51618
diff changeset
   262
}
7658f8d7b2dc minimal jedit mode for Isabelle NEWS;
wenzelm
parents: 51618
diff changeset
   263