src/Tools/jEdit/src/jedit/isabelle_sidekick.scala
author wenzelm
Wed, 30 Dec 2009 21:57:29 +0100
changeset 34819 86cb7f8e5a0d
parent 34802 006331f2b128
child 34823 2f3ea37c5958
permissions -rw-r--r--
tuned signature;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
34393
f0e1608a774f basic tree structure for sidekick
immler@in.tum.de
parents:
diff changeset
     1
/*
34417
bce2f2ea9819 misc tuning and adaption according to original IsabelleParser --
wenzelm
parents: 34408
diff changeset
     2
 * SideKick parser for Isabelle proof documents
34393
f0e1608a774f basic tree structure for sidekick
immler@in.tum.de
parents:
diff changeset
     3
 *
34407
aad6834ba380 added some headers and comments;
wenzelm
parents: 34406
diff changeset
     4
 * @author Fabian Immler, TU Munich
34417
bce2f2ea9819 misc tuning and adaption according to original IsabelleParser --
wenzelm
parents: 34408
diff changeset
     5
 * @author Makarius
34393
f0e1608a774f basic tree structure for sidekick
immler@in.tum.de
parents:
diff changeset
     6
 */
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
34475
f963335dbc6b implemented IsabelleSideKickParser.complete
immler@in.tum.de
parents: 34440
diff changeset
    11
import scala.collection.Set
f963335dbc6b implemented IsabelleSideKickParser.complete
immler@in.tum.de
parents: 34440
diff changeset
    12
import scala.collection.immutable.TreeSet
34417
bce2f2ea9819 misc tuning and adaption according to original IsabelleParser --
wenzelm
parents: 34408
diff changeset
    13
34393
f0e1608a774f basic tree structure for sidekick
immler@in.tum.de
parents:
diff changeset
    14
import javax.swing.tree.DefaultMutableTreeNode
34701
80b0add08eef IsabelleSideKickParser: incorporate former MarkupNode.markup2default_node, observe stopped flag;
wenzelm
parents: 34669
diff changeset
    15
import javax.swing.text.Position
80b0add08eef IsabelleSideKickParser: incorporate former MarkupNode.markup2default_node, observe stopped flag;
wenzelm
parents: 34669
diff changeset
    16
import javax.swing.Icon
34417
bce2f2ea9819 misc tuning and adaption according to original IsabelleParser --
wenzelm
parents: 34408
diff changeset
    17
34609
7ca1ef2f150d simplified and reactivated SideKickCompletion, cf. org.gjt.sp.jedit.gui.CompleteWord;
wenzelm
parents: 34562
diff changeset
    18
import org.gjt.sp.jedit.{Buffer, EditPane, TextUtilities, View}
34417
bce2f2ea9819 misc tuning and adaption according to original IsabelleParser --
wenzelm
parents: 34408
diff changeset
    19
import errorlist.DefaultErrorSource
34701
80b0add08eef IsabelleSideKickParser: incorporate former MarkupNode.markup2default_node, observe stopped flag;
wenzelm
parents: 34669
diff changeset
    20
import sidekick.{SideKickParser, SideKickParsedData, SideKickCompletion, IAsset}
80b0add08eef IsabelleSideKickParser: incorporate former MarkupNode.markup2default_node, observe stopped flag;
wenzelm
parents: 34669
diff changeset
    21
34760
dc7f5e0d9d27 misc modernization of names;
wenzelm
parents: 34759
diff changeset
    22
import isabelle.proofdocument.{Command, Markup_Node, Proof_Document}
34417
bce2f2ea9819 misc tuning and adaption according to original IsabelleParser --
wenzelm
parents: 34408
diff changeset
    23
34393
f0e1608a774f basic tree structure for sidekick
immler@in.tum.de
parents:
diff changeset
    24
34760
dc7f5e0d9d27 misc modernization of names;
wenzelm
parents: 34759
diff changeset
    25
class Isabelle_Sidekick extends SideKickParser("isabelle")
34625
799a40faa4f1 completion: decode symbols only if isabelle encoding is active (to prevent unicode chars written back to file);
wenzelm
parents: 34612
diff changeset
    26
{
34417
bce2f2ea9819 misc tuning and adaption according to original IsabelleParser --
wenzelm
parents: 34408
diff changeset
    27
  /* parsing */
bce2f2ea9819 misc tuning and adaption according to original IsabelleParser --
wenzelm
parents: 34408
diff changeset
    28
34625
799a40faa4f1 completion: decode symbols only if isabelle encoding is active (to prevent unicode chars written back to file);
wenzelm
parents: 34612
diff changeset
    29
  @volatile private var stopped = false
34503
7d0726f19d04 tuned whitespace;
wenzelm
parents: 34485
diff changeset
    30
  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
    31
34625
799a40faa4f1 completion: decode symbols only if isabelle encoding is active (to prevent unicode chars written back to file);
wenzelm
parents: 34612
diff changeset
    32
  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
    33
  {
34717
3f32e08bbb6c sidekick root data: set buffer length to avoid crash of initial caret move;
wenzelm
parents: 34705
diff changeset
    34
    implicit def int_to_pos(offset: Int): Position =
3f32e08bbb6c sidekick root data: set buffer length to avoid crash of initial caret move;
wenzelm
parents: 34705
diff changeset
    35
      new Position { def getOffset = offset; override def toString = offset.toString }
3f32e08bbb6c sidekick root data: set buffer length to avoid crash of initial caret move;
wenzelm
parents: 34705
diff changeset
    36
34417
bce2f2ea9819 misc tuning and adaption according to original IsabelleParser --
wenzelm
parents: 34408
diff changeset
    37
    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
    38
34789
30528e68f774 some explicit Swing_Thread guards;
wenzelm
parents: 34788
diff changeset
    39
    // FIXME lock buffer !??
34417
bce2f2ea9819 misc tuning and adaption according to original IsabelleParser --
wenzelm
parents: 34408
diff changeset
    40
    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
    41
    val root = data.root
3f32e08bbb6c sidekick root data: set buffer length to avoid crash of initial caret move;
wenzelm
parents: 34705
diff changeset
    42
    data.getAsset(root).setEnd(buffer.getLength)
34475
f963335dbc6b implemented IsabelleSideKickParser.complete
immler@in.tum.de
parents: 34440
diff changeset
    43
34789
30528e68f774 some explicit Swing_Thread guards;
wenzelm
parents: 34788
diff changeset
    44
    Swing_Thread.now { Document_Model(buffer) } match {
34784
02959dcea756 split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents: 34777
diff changeset
    45
      case Some(model) =>
02959dcea756 split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents: 34777
diff changeset
    46
        val document = model.current_document()
34777
91d6089cef88 class Session models full session, with or without prover process (cf. heaps, browser_info);
wenzelm
parents: 34760
diff changeset
    47
        for (command <- document.commands if !stopped) {
91d6089cef88 class Session models full session, with or without prover process (cf. heaps, browser_info);
wenzelm
parents: 34760
diff changeset
    48
          root.add(command.markup_root(document).swing_tree((node: Markup_Node) =>
91d6089cef88 class Session models full session, with or without prover process (cf. heaps, browser_info);
wenzelm
parents: 34760
diff changeset
    49
              {
91d6089cef88 class Session models full session, with or without prover process (cf. heaps, browser_info);
wenzelm
parents: 34760
diff changeset
    50
                val content = command.content(node.start, node.stop)
91d6089cef88 class Session models full session, with or without prover process (cf. heaps, browser_info);
wenzelm
parents: 34760
diff changeset
    51
                val command_start = command.start(document)
91d6089cef88 class Session models full session, with or without prover process (cf. heaps, browser_info);
wenzelm
parents: 34760
diff changeset
    52
                val id = command.id
34705
cd2cdf3b33b9 MarkupNode: removed id;
wenzelm
parents: 34704
diff changeset
    53
34777
91d6089cef88 class Session models full session, with or without prover process (cf. heaps, browser_info);
wenzelm
parents: 34760
diff changeset
    54
                new DefaultMutableTreeNode(new IAsset {
91d6089cef88 class Session models full session, with or without prover process (cf. heaps, browser_info);
wenzelm
parents: 34760
diff changeset
    55
                  override def getIcon: Icon = null
91d6089cef88 class Session models full session, with or without prover process (cf. heaps, browser_info);
wenzelm
parents: 34760
diff changeset
    56
                  override def getShortString: String = content
91d6089cef88 class Session models full session, with or without prover process (cf. heaps, browser_info);
wenzelm
parents: 34760
diff changeset
    57
                  override def getLongString: String = node.info.toString
91d6089cef88 class Session models full session, with or without prover process (cf. heaps, browser_info);
wenzelm
parents: 34760
diff changeset
    58
                  override def getName: String = id
91d6089cef88 class Session models full session, with or without prover process (cf. heaps, browser_info);
wenzelm
parents: 34760
diff changeset
    59
                  override def setName(name: String) = ()
91d6089cef88 class Session models full session, with or without prover process (cf. heaps, browser_info);
wenzelm
parents: 34760
diff changeset
    60
                  override def setStart(start: Position) = ()
91d6089cef88 class Session models full session, with or without prover process (cf. heaps, browser_info);
wenzelm
parents: 34760
diff changeset
    61
                  override def getStart: Position = command_start + node.start
91d6089cef88 class Session models full session, with or without prover process (cf. heaps, browser_info);
wenzelm
parents: 34760
diff changeset
    62
                  override def setEnd(end: Position) = ()
91d6089cef88 class Session models full session, with or without prover process (cf. heaps, browser_info);
wenzelm
parents: 34760
diff changeset
    63
                  override def getEnd: Position = command_start + node.stop
91d6089cef88 class Session models full session, with or without prover process (cf. heaps, browser_info);
wenzelm
parents: 34760
diff changeset
    64
                  override def toString = id + ": " + content + "[" + getStart + " - " + getEnd + "]"
91d6089cef88 class Session models full session, with or without prover process (cf. heaps, browser_info);
wenzelm
parents: 34760
diff changeset
    65
                })
91d6089cef88 class Session models full session, with or without prover process (cf. heaps, browser_info);
wenzelm
parents: 34760
diff changeset
    66
              }))
91d6089cef88 class Session models full session, with or without prover process (cf. heaps, browser_info);
wenzelm
parents: 34760
diff changeset
    67
        }
91d6089cef88 class Session models full session, with or without prover process (cf. heaps, browser_info);
wenzelm
parents: 34760
diff changeset
    68
        if (stopped) root.add(new DefaultMutableTreeNode("<parser stopped>"))
91d6089cef88 class Session models full session, with or without prover process (cf. heaps, browser_info);
wenzelm
parents: 34760
diff changeset
    69
      case None => root.add(new DefaultMutableTreeNode("<buffer inactive>"))
34475
f963335dbc6b implemented IsabelleSideKickParser.complete
immler@in.tum.de
parents: 34440
diff changeset
    70
    }
34417
bce2f2ea9819 misc tuning and adaption according to original IsabelleParser --
wenzelm
parents: 34408
diff changeset
    71
    data
bce2f2ea9819 misc tuning and adaption according to original IsabelleParser --
wenzelm
parents: 34408
diff changeset
    72
  }
bce2f2ea9819 misc tuning and adaption according to original IsabelleParser --
wenzelm
parents: 34408
diff changeset
    73
34777
91d6089cef88 class Session models full session, with or without prover process (cf. heaps, browser_info);
wenzelm
parents: 34760
diff changeset
    74
  
34417
bce2f2ea9819 misc tuning and adaption according to original IsabelleParser --
wenzelm
parents: 34408
diff changeset
    75
  /* completion */
bce2f2ea9819 misc tuning and adaption according to original IsabelleParser --
wenzelm
parents: 34408
diff changeset
    76
bce2f2ea9819 misc tuning and adaption according to original IsabelleParser --
wenzelm
parents: 34408
diff changeset
    77
  override def supportsCompletion = true
bce2f2ea9819 misc tuning and adaption according to original IsabelleParser --
wenzelm
parents: 34408
diff changeset
    78
  override def canCompleteAnywhere = true
bce2f2ea9819 misc tuning and adaption according to original IsabelleParser --
wenzelm
parents: 34408
diff changeset
    79
34609
7ca1ef2f150d simplified and reactivated SideKickCompletion, cf. org.gjt.sp.jedit.gui.CompleteWord;
wenzelm
parents: 34562
diff changeset
    80
  override def complete(pane: EditPane, caret: Int): SideKickCompletion =
7ca1ef2f150d simplified and reactivated SideKickCompletion, cf. org.gjt.sp.jedit.gui.CompleteWord;
wenzelm
parents: 34562
diff changeset
    81
  {
34475
f963335dbc6b implemented IsabelleSideKickParser.complete
immler@in.tum.de
parents: 34440
diff changeset
    82
    val buffer = pane.getBuffer
34612
5a03dc7a19e1 fall back on Isabelle system completion (symbols only);
wenzelm
parents: 34611
diff changeset
    83
5a03dc7a19e1 fall back on Isabelle system completion (symbols only);
wenzelm
parents: 34611
diff changeset
    84
    val line = buffer.getLineOfOffset(caret)
5a03dc7a19e1 fall back on Isabelle system completion (symbols only);
wenzelm
parents: 34611
diff changeset
    85
    val start = buffer.getLineStartOffset(line)
5a03dc7a19e1 fall back on Isabelle system completion (symbols only);
wenzelm
parents: 34611
diff changeset
    86
    val text = buffer.getSegment(start, caret - start)
34609
7ca1ef2f150d simplified and reactivated SideKickCompletion, cf. org.gjt.sp.jedit.gui.CompleteWord;
wenzelm
parents: 34562
diff changeset
    87
34819
86cb7f8e5a0d tuned signature;
wenzelm
parents: 34802
diff changeset
    88
    val completion = Isabelle.session.current_syntax.completion
34475
f963335dbc6b implemented IsabelleSideKickParser.complete
immler@in.tum.de
parents: 34440
diff changeset
    89
34612
5a03dc7a19e1 fall back on Isabelle system completion (symbols only);
wenzelm
parents: 34611
diff changeset
    90
    completion.complete(text) match {
5a03dc7a19e1 fall back on Isabelle system completion (symbols only);
wenzelm
parents: 34611
diff changeset
    91
      case None => null
5a03dc7a19e1 fall back on Isabelle system completion (symbols only);
wenzelm
parents: 34611
diff changeset
    92
      case Some((word, cs)) =>
34625
799a40faa4f1 completion: decode symbols only if isabelle encoding is active (to prevent unicode chars written back to file);
wenzelm
parents: 34612
diff changeset
    93
        val ds =
34738
80408ffc84a8 tuned file name;
wenzelm
parents: 34720
diff changeset
    94
          if (Isabelle_Encoding.is_active(buffer))
34796
e65352f12421 sort completions by plain string order;
wenzelm
parents: 34789
diff changeset
    95
            cs.map(Isabelle.system.symbols.decode(_)).sort(_ < _)
34625
799a40faa4f1 completion: decode symbols only if isabelle encoding is active (to prevent unicode chars written back to file);
wenzelm
parents: 34612
diff changeset
    96
          else cs
799a40faa4f1 completion: decode symbols only if isabelle encoding is active (to prevent unicode chars written back to file);
wenzelm
parents: 34612
diff changeset
    97
        new SideKickCompletion(pane.getView, word, ds.toArray.asInstanceOf[Array[Object]]) { }
34611
b40e43d70ae9 use isabelle.Completion;
wenzelm
parents: 34609
diff changeset
    98
    }
34609
7ca1ef2f150d simplified and reactivated SideKickCompletion, cf. org.gjt.sp.jedit.gui.CompleteWord;
wenzelm
parents: 34562
diff changeset
    99
  }
34475
f963335dbc6b implemented IsabelleSideKickParser.complete
immler@in.tum.de
parents: 34440
diff changeset
   100
34393
f0e1608a774f basic tree structure for sidekick
immler@in.tum.de
parents:
diff changeset
   101
}