src/Tools/jEdit/src/jedit/isabelle_sidekick.scala
author wenzelm
Sat, 08 May 2010 20:58:02 +0200
changeset 36759 dc972354d77c
parent 36738 dce592144219
child 36760 b82a698ef6c9
permissions -rw-r--r--
tuned;
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
/*
36738
dce592144219 support several sidekick parsers -- very basic default parser;
wenzelm
parents: 36737
diff changeset
     2
 * SideKick parsers 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
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
34393
f0e1608a774f basic tree structure for sidekick
immler@in.tum.de
parents:
diff changeset
    16
import javax.swing.tree.DefaultMutableTreeNode
34701
80b0add08eef IsabelleSideKickParser: incorporate former MarkupNode.markup2default_node, observe stopped flag;
wenzelm
parents: 34669
diff changeset
    17
import javax.swing.text.Position
80b0add08eef IsabelleSideKickParser: incorporate former MarkupNode.markup2default_node, observe stopped flag;
wenzelm
parents: 34669
diff changeset
    18
import javax.swing.Icon
34417
bce2f2ea9819 misc tuning and adaption according to original IsabelleParser --
wenzelm
parents: 34408
diff changeset
    19
34609
7ca1ef2f150d simplified and reactivated SideKickCompletion, cf. org.gjt.sp.jedit.gui.CompleteWord;
wenzelm
parents: 34562
diff changeset
    20
import org.gjt.sp.jedit.{Buffer, EditPane, TextUtilities, View}
34417
bce2f2ea9819 misc tuning and adaption according to original IsabelleParser --
wenzelm
parents: 34408
diff changeset
    21
import errorlist.DefaultErrorSource
34701
80b0add08eef IsabelleSideKickParser: incorporate former MarkupNode.markup2default_node, observe stopped flag;
wenzelm
parents: 34669
diff changeset
    22
import sidekick.{SideKickParser, SideKickParsedData, SideKickCompletion, IAsset}
80b0add08eef IsabelleSideKickParser: incorporate former MarkupNode.markup2default_node, observe stopped flag;
wenzelm
parents: 34669
diff changeset
    23
34393
f0e1608a774f basic tree structure for sidekick
immler@in.tum.de
parents:
diff changeset
    24
36738
dce592144219 support several sidekick parsers -- very basic default parser;
wenzelm
parents: 36737
diff changeset
    25
object Isabelle_Sidekick
dce592144219 support several sidekick parsers -- very basic default parser;
wenzelm
parents: 36737
diff changeset
    26
{
dce592144219 support several sidekick parsers -- very basic default parser;
wenzelm
parents: 36737
diff changeset
    27
  implicit def int_to_pos(offset: Int): Position =
dce592144219 support several sidekick parsers -- very basic default parser;
wenzelm
parents: 36737
diff changeset
    28
    new Position { def getOffset = offset; override def toString = offset.toString }
dce592144219 support several sidekick parsers -- very basic default parser;
wenzelm
parents: 36737
diff changeset
    29
}
dce592144219 support several sidekick parsers -- very basic default parser;
wenzelm
parents: 36737
diff changeset
    30
dce592144219 support several sidekick parsers -- very basic default parser;
wenzelm
parents: 36737
diff changeset
    31
36759
wenzelm
parents: 36738
diff changeset
    32
abstract class Isabelle_Sidekick(name: String) 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
    33
{
34417
bce2f2ea9819 misc tuning and adaption according to original IsabelleParser --
wenzelm
parents: 34408
diff changeset
    34
  /* parsing */
bce2f2ea9819 misc tuning and adaption according to original IsabelleParser --
wenzelm
parents: 34408
diff changeset
    35
36759
wenzelm
parents: 36738
diff changeset
    36
  @volatile protected var stopped = false
34503
7d0726f19d04 tuned whitespace;
wenzelm
parents: 34485
diff changeset
    37
  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
    38
36759
wenzelm
parents: 36738
diff changeset
    39
  def parser(data: SideKickParsedData, model: Document_Model): Unit
wenzelm
parents: 36738
diff changeset
    40
34625
799a40faa4f1 completion: decode symbols only if isabelle encoding is active (to prevent unicode chars written back to file);
wenzelm
parents: 34612
diff changeset
    41
  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
    42
  {
36738
dce592144219 support several sidekick parsers -- very basic default parser;
wenzelm
parents: 36737
diff changeset
    43
    import Isabelle_Sidekick.int_to_pos
34717
3f32e08bbb6c sidekick root data: set buffer length to avoid crash of initial caret move;
wenzelm
parents: 34705
diff changeset
    44
34417
bce2f2ea9819 misc tuning and adaption according to original IsabelleParser --
wenzelm
parents: 34408
diff changeset
    45
    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
    46
34789
30528e68f774 some explicit Swing_Thread guards;
wenzelm
parents: 34788
diff changeset
    47
    // FIXME lock buffer !??
34417
bce2f2ea9819 misc tuning and adaption according to original IsabelleParser --
wenzelm
parents: 34408
diff changeset
    48
    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
    49
    val root = data.root
3f32e08bbb6c sidekick root data: set buffer length to avoid crash of initial caret move;
wenzelm
parents: 34705
diff changeset
    50
    data.getAsset(root).setEnd(buffer.getLength)
34475
f963335dbc6b implemented IsabelleSideKickParser.complete
immler@in.tum.de
parents: 34440
diff changeset
    51
34789
30528e68f774 some explicit Swing_Thread guards;
wenzelm
parents: 34788
diff changeset
    52
    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
    53
      case Some(model) =>
36759
wenzelm
parents: 36738
diff changeset
    54
        parser(data, model)
34777
91d6089cef88 class Session models full session, with or without prover process (cf. heaps, browser_info);
wenzelm
parents: 34760
diff changeset
    55
        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
    56
      case None => root.add(new DefaultMutableTreeNode("<buffer inactive>"))
34475
f963335dbc6b implemented IsabelleSideKickParser.complete
immler@in.tum.de
parents: 34440
diff changeset
    57
    }
34417
bce2f2ea9819 misc tuning and adaption according to original IsabelleParser --
wenzelm
parents: 34408
diff changeset
    58
    data
bce2f2ea9819 misc tuning and adaption according to original IsabelleParser --
wenzelm
parents: 34408
diff changeset
    59
  }
bce2f2ea9819 misc tuning and adaption according to original IsabelleParser --
wenzelm
parents: 34408
diff changeset
    60
36738
dce592144219 support several sidekick parsers -- very basic default parser;
wenzelm
parents: 36737
diff changeset
    61
34417
bce2f2ea9819 misc tuning and adaption according to original IsabelleParser --
wenzelm
parents: 34408
diff changeset
    62
  /* completion */
bce2f2ea9819 misc tuning and adaption according to original IsabelleParser --
wenzelm
parents: 34408
diff changeset
    63
bce2f2ea9819 misc tuning and adaption according to original IsabelleParser --
wenzelm
parents: 34408
diff changeset
    64
  override def supportsCompletion = true
bce2f2ea9819 misc tuning and adaption according to original IsabelleParser --
wenzelm
parents: 34408
diff changeset
    65
  override def canCompleteAnywhere = true
bce2f2ea9819 misc tuning and adaption according to original IsabelleParser --
wenzelm
parents: 34408
diff changeset
    66
34609
7ca1ef2f150d simplified and reactivated SideKickCompletion, cf. org.gjt.sp.jedit.gui.CompleteWord;
wenzelm
parents: 34562
diff changeset
    67
  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
    68
  {
34475
f963335dbc6b implemented IsabelleSideKickParser.complete
immler@in.tum.de
parents: 34440
diff changeset
    69
    val buffer = pane.getBuffer
34612
5a03dc7a19e1 fall back on Isabelle system completion (symbols only);
wenzelm
parents: 34611
diff changeset
    70
5a03dc7a19e1 fall back on Isabelle system completion (symbols only);
wenzelm
parents: 34611
diff changeset
    71
    val line = buffer.getLineOfOffset(caret)
5a03dc7a19e1 fall back on Isabelle system completion (symbols only);
wenzelm
parents: 34611
diff changeset
    72
    val start = buffer.getLineStartOffset(line)
5a03dc7a19e1 fall back on Isabelle system completion (symbols only);
wenzelm
parents: 34611
diff changeset
    73
    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
    74
34819
86cb7f8e5a0d tuned signature;
wenzelm
parents: 34802
diff changeset
    75
    val completion = Isabelle.session.current_syntax.completion
34475
f963335dbc6b implemented IsabelleSideKickParser.complete
immler@in.tum.de
parents: 34440
diff changeset
    76
34612
5a03dc7a19e1 fall back on Isabelle system completion (symbols only);
wenzelm
parents: 34611
diff changeset
    77
    completion.complete(text) match {
5a03dc7a19e1 fall back on Isabelle system completion (symbols only);
wenzelm
parents: 34611
diff changeset
    78
      case None => null
5a03dc7a19e1 fall back on Isabelle system completion (symbols only);
wenzelm
parents: 34611
diff changeset
    79
      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
    80
        val ds =
35004
b89a31957950 filter out identical completions only after symbols.decode -- recover completion of literal symbols (e.g. \<AA>);
wenzelm
parents: 34871
diff changeset
    81
          (if (Isabelle_Encoding.is_active(buffer))
34796
e65352f12421 sort completions by plain string order;
wenzelm
parents: 34789
diff changeset
    82
            cs.map(Isabelle.system.symbols.decode(_)).sort(_ < _)
35004
b89a31957950 filter out identical completions only after symbols.decode -- recover completion of literal symbols (e.g. \<AA>);
wenzelm
parents: 34871
diff changeset
    83
           else cs).filter(_ != word)
b89a31957950 filter out identical completions only after symbols.decode -- recover completion of literal symbols (e.g. \<AA>);
wenzelm
parents: 34871
diff changeset
    84
        if (ds.isEmpty) null
b89a31957950 filter out identical completions only after symbols.decode -- recover completion of literal symbols (e.g. \<AA>);
wenzelm
parents: 34871
diff changeset
    85
        else new SideKickCompletion(pane.getView, word, ds.toArray.asInstanceOf[Array[Object]]) { }
34611
b40e43d70ae9 use isabelle.Completion;
wenzelm
parents: 34609
diff changeset
    86
    }
34609
7ca1ef2f150d simplified and reactivated SideKickCompletion, cf. org.gjt.sp.jedit.gui.CompleteWord;
wenzelm
parents: 34562
diff changeset
    87
  }
34393
f0e1608a774f basic tree structure for sidekick
immler@in.tum.de
parents:
diff changeset
    88
}
36738
dce592144219 support several sidekick parsers -- very basic default parser;
wenzelm
parents: 36737
diff changeset
    89
dce592144219 support several sidekick parsers -- very basic default parser;
wenzelm
parents: 36737
diff changeset
    90
36759
wenzelm
parents: 36738
diff changeset
    91
class Isabelle_Sidekick_Default extends Isabelle_Sidekick("isabelle")
wenzelm
parents: 36738
diff changeset
    92
{
wenzelm
parents: 36738
diff changeset
    93
  def parser(data: SideKickParsedData, model: Document_Model)
wenzelm
parents: 36738
diff changeset
    94
  {
wenzelm
parents: 36738
diff changeset
    95
    import Isabelle_Sidekick.int_to_pos
36738
dce592144219 support several sidekick parsers -- very basic default parser;
wenzelm
parents: 36737
diff changeset
    96
36759
wenzelm
parents: 36738
diff changeset
    97
    val root = data.root
wenzelm
parents: 36738
diff changeset
    98
    val document = model.recent_document()
wenzelm
parents: 36738
diff changeset
    99
    for {
wenzelm
parents: 36738
diff changeset
   100
      (command, command_start) <- document.command_range(0)
wenzelm
parents: 36738
diff changeset
   101
      if command.is_command && !is_stopped()
wenzelm
parents: 36738
diff changeset
   102
    }
wenzelm
parents: 36738
diff changeset
   103
    {
wenzelm
parents: 36738
diff changeset
   104
      val name = command.name
wenzelm
parents: 36738
diff changeset
   105
      val node =
wenzelm
parents: 36738
diff changeset
   106
        new DefaultMutableTreeNode(new IAsset {
wenzelm
parents: 36738
diff changeset
   107
          override def getIcon: Icon = null
wenzelm
parents: 36738
diff changeset
   108
          override def getShortString: String = name
wenzelm
parents: 36738
diff changeset
   109
          override def getLongString: String = name
wenzelm
parents: 36738
diff changeset
   110
          override def getName: String = name
wenzelm
parents: 36738
diff changeset
   111
          override def setName(name: String) = ()
wenzelm
parents: 36738
diff changeset
   112
          override def setStart(start: Position) = ()
wenzelm
parents: 36738
diff changeset
   113
          override def getStart: Position = command_start
wenzelm
parents: 36738
diff changeset
   114
          override def setEnd(end: Position) = ()
wenzelm
parents: 36738
diff changeset
   115
          override def getEnd: Position = command_start + command.length
wenzelm
parents: 36738
diff changeset
   116
          override def toString = name
wenzelm
parents: 36738
diff changeset
   117
        })
wenzelm
parents: 36738
diff changeset
   118
      root.add(node)
wenzelm
parents: 36738
diff changeset
   119
    }
wenzelm
parents: 36738
diff changeset
   120
  }
wenzelm
parents: 36738
diff changeset
   121
}
36738
dce592144219 support several sidekick parsers -- very basic default parser;
wenzelm
parents: 36737
diff changeset
   122
dce592144219 support several sidekick parsers -- very basic default parser;
wenzelm
parents: 36737
diff changeset
   123
36759
wenzelm
parents: 36738
diff changeset
   124
class Isabelle_Sidekick_Raw extends Isabelle_Sidekick("isabelle-raw")
wenzelm
parents: 36738
diff changeset
   125
{
wenzelm
parents: 36738
diff changeset
   126
  def parser(data: SideKickParsedData, model: Document_Model)
wenzelm
parents: 36738
diff changeset
   127
  {
wenzelm
parents: 36738
diff changeset
   128
    import Isabelle_Sidekick.int_to_pos
36738
dce592144219 support several sidekick parsers -- very basic default parser;
wenzelm
parents: 36737
diff changeset
   129
36759
wenzelm
parents: 36738
diff changeset
   130
    val root = data.root
wenzelm
parents: 36738
diff changeset
   131
    val document = model.recent_document()
wenzelm
parents: 36738
diff changeset
   132
    for ((command, command_start) <- document.command_range(0) if !is_stopped()) {
wenzelm
parents: 36738
diff changeset
   133
      root.add(document.current_state(command).get.markup_root.swing_tree((node: Markup_Node) =>
wenzelm
parents: 36738
diff changeset
   134
          {
wenzelm
parents: 36738
diff changeset
   135
            val content = Pretty.str_of(List(XML.Text(command.source(node.start, node.stop))))
wenzelm
parents: 36738
diff changeset
   136
            val id = command.id
36738
dce592144219 support several sidekick parsers -- very basic default parser;
wenzelm
parents: 36737
diff changeset
   137
36759
wenzelm
parents: 36738
diff changeset
   138
            new DefaultMutableTreeNode(new IAsset {
wenzelm
parents: 36738
diff changeset
   139
              override def getIcon: Icon = null
wenzelm
parents: 36738
diff changeset
   140
              override def getShortString: String = content
wenzelm
parents: 36738
diff changeset
   141
              override def getLongString: String = node.info.toString
wenzelm
parents: 36738
diff changeset
   142
              override def getName: String = id
wenzelm
parents: 36738
diff changeset
   143
              override def setName(name: String) = ()
wenzelm
parents: 36738
diff changeset
   144
              override def setStart(start: Position) = ()
wenzelm
parents: 36738
diff changeset
   145
              override def getStart: Position = command_start + node.start
wenzelm
parents: 36738
diff changeset
   146
              override def setEnd(end: Position) = ()
wenzelm
parents: 36738
diff changeset
   147
              override def getEnd: Position = command_start + node.stop
wenzelm
parents: 36738
diff changeset
   148
              override def toString = id + ": " + content + "[" + getStart + " - " + getEnd + "]"
wenzelm
parents: 36738
diff changeset
   149
            })
wenzelm
parents: 36738
diff changeset
   150
          }))
wenzelm
parents: 36738
diff changeset
   151
    }
wenzelm
parents: 36738
diff changeset
   152
  }
wenzelm
parents: 36738
diff changeset
   153
}
36738
dce592144219 support several sidekick parsers -- very basic default parser;
wenzelm
parents: 36737
diff changeset
   154