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