src/Tools/jEdit/src/isabelle_sidekick.scala
author wenzelm
Wed, 08 Jun 2011 21:40:54 +0200
changeset 43286 a319da4fbfb0
parent 43282 5d294220ca43
child 43661 39fdbd814c7f
permissions -rw-r--r--
simplified directory structure;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
43282
5d294220ca43 moved sources -- eliminated Netbeans artifact of jedit package directory;
wenzelm
parents: 40792
diff changeset
     1
/*  Title:      Tools/jEdit/src/isabelle_sidekick.scala
36760
b82a698ef6c9 tuned headers;
wenzelm
parents: 36759
diff changeset
     2
    Author:     Fabian Immler, TU Munich
b82a698ef6c9 tuned headers;
wenzelm
parents: 36759
diff changeset
     3
    Author:     Makarius
b82a698ef6c9 tuned headers;
wenzelm
parents: 36759
diff changeset
     4
b82a698ef6c9 tuned headers;
wenzelm
parents: 36759
diff changeset
     5
SideKick parsers for Isabelle proof documents.
b82a698ef6c9 tuned headers;
wenzelm
parents: 36759
diff changeset
     6
*/
34393
f0e1608a774f basic tree structure for sidekick
immler@in.tum.de
parents:
diff changeset
     7
34426
81f93e0f13b4 renamed isabelle.prover.IsabelleSKParser to isabelle.jedit.IsabelleSideKickParser;
wenzelm
parents: 34417
diff changeset
     8
package isabelle.jedit
34393
f0e1608a774f basic tree structure for sidekick
immler@in.tum.de
parents:
diff changeset
     9
34760
dc7f5e0d9d27 misc modernization of names;
wenzelm
parents: 34759
diff changeset
    10
36015
6111de7c916a adapted to Scala 2.8.0 Beta 1;
wenzelm
parents: 35004
diff changeset
    11
import isabelle._
6111de7c916a adapted to Scala 2.8.0 Beta 1;
wenzelm
parents: 35004
diff changeset
    12
34475
f963335dbc6b implemented IsabelleSideKickParser.complete
immler@in.tum.de
parents: 34440
diff changeset
    13
import scala.collection.Set
f963335dbc6b implemented IsabelleSideKickParser.complete
immler@in.tum.de
parents: 34440
diff changeset
    14
import scala.collection.immutable.TreeSet
34417
bce2f2ea9819 misc tuning and adaption according to original IsabelleParser --
wenzelm
parents: 34408
diff changeset
    15
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
{
40477
wenzelm
parents: 40475
diff changeset
    27
  def int_to_pos(offset: Text.Offset): Position =
36738
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 }
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
    29
40477
wenzelm
parents: 40475
diff changeset
    30
  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
    31
  {
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
    32
    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
    33
    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
    34
    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
    35
    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
    36
    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
    37
    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
    38
    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
    39
    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
    40
    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
    41
    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
    42
    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
    43
    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
    44
    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
    45
  }
36738
dce592144219 support several sidekick parsers -- very basic default parser;
wenzelm
parents: 36737
diff changeset
    46
}
dce592144219 support several sidekick parsers -- very basic default parser;
wenzelm
parents: 36737
diff changeset
    47
dce592144219 support several sidekick parsers -- very basic default parser;
wenzelm
parents: 36737
diff changeset
    48
36759
wenzelm
parents: 36738
diff changeset
    49
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
    50
{
34417
bce2f2ea9819 misc tuning and adaption according to original IsabelleParser --
wenzelm
parents: 34408
diff changeset
    51
  /* parsing */
bce2f2ea9819 misc tuning and adaption according to original IsabelleParser --
wenzelm
parents: 34408
diff changeset
    52
36759
wenzelm
parents: 36738
diff changeset
    53
  @volatile protected var stopped = false
34503
7d0726f19d04 tuned whitespace;
wenzelm
parents: 34485
diff changeset
    54
  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
    55
36759
wenzelm
parents: 36738
diff changeset
    56
  def parser(data: SideKickParsedData, model: Document_Model): Unit
wenzelm
parents: 36738
diff changeset
    57
34625
799a40faa4f1 completion: decode symbols only if isabelle encoding is active (to prevent unicode chars written back to file);
wenzelm
parents: 34612
diff changeset
    58
  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
    59
  {
34417
bce2f2ea9819 misc tuning and adaption according to original IsabelleParser --
wenzelm
parents: 34408
diff changeset
    60
    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
    61
38640
105d1f112da5 sporadic locking of jEdit buffer;
wenzelm
parents: 38577
diff changeset
    62
    // FIXME lock buffer (!??)
34417
bce2f2ea9819 misc tuning and adaption according to original IsabelleParser --
wenzelm
parents: 34408
diff changeset
    63
    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
    64
    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
    65
    data.getAsset(root).setEnd(Isabelle_Sidekick.int_to_pos(buffer.getLength))
34475
f963335dbc6b implemented IsabelleSideKickParser.complete
immler@in.tum.de
parents: 34440
diff changeset
    66
34789
30528e68f774 some explicit Swing_Thread guards;
wenzelm
parents: 34788
diff changeset
    67
    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
    68
      case Some(model) =>
36759
wenzelm
parents: 36738
diff changeset
    69
        parser(data, model)
34777
91d6089cef88 class Session models full session, with or without prover process (cf. heaps, browser_info);
wenzelm
parents: 34760
diff changeset
    70
        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
    71
      case None => root.add(new DefaultMutableTreeNode("<buffer inactive>"))
34475
f963335dbc6b implemented IsabelleSideKickParser.complete
immler@in.tum.de
parents: 34440
diff changeset
    72
    }
34417
bce2f2ea9819 misc tuning and adaption according to original IsabelleParser --
wenzelm
parents: 34408
diff changeset
    73
    data
bce2f2ea9819 misc tuning and adaption according to original IsabelleParser --
wenzelm
parents: 34408
diff changeset
    74
  }
bce2f2ea9819 misc tuning and adaption according to original IsabelleParser --
wenzelm
parents: 34408
diff changeset
    75
36738
dce592144219 support several sidekick parsers -- very basic default parser;
wenzelm
parents: 36737
diff changeset
    76
34417
bce2f2ea9819 misc tuning and adaption according to original IsabelleParser --
wenzelm
parents: 34408
diff changeset
    77
  /* completion */
bce2f2ea9819 misc tuning and adaption according to original IsabelleParser --
wenzelm
parents: 34408
diff changeset
    78
bce2f2ea9819 misc tuning and adaption according to original IsabelleParser --
wenzelm
parents: 34408
diff changeset
    79
  override def supportsCompletion = true
bce2f2ea9819 misc tuning and adaption according to original IsabelleParser --
wenzelm
parents: 34408
diff changeset
    80
  override def canCompleteAnywhere = true
bce2f2ea9819 misc tuning and adaption according to original IsabelleParser --
wenzelm
parents: 34408
diff changeset
    81
40477
wenzelm
parents: 40475
diff changeset
    82
  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
    83
  {
34475
f963335dbc6b implemented IsabelleSideKickParser.complete
immler@in.tum.de
parents: 34440
diff changeset
    84
    val buffer = pane.getBuffer
39624
57496c868dcc tuned Isabelle_Sidekick.complete: lock buffer, depend on document model;
wenzelm
parents: 38663
diff changeset
    85
    Isabelle.swing_buffer_lock(buffer) {
57496c868dcc tuned Isabelle_Sidekick.complete: lock buffer, depend on document model;
wenzelm
parents: 38663
diff changeset
    86
      Document_Model(buffer) match {
57496c868dcc tuned Isabelle_Sidekick.complete: lock buffer, depend on document model;
wenzelm
parents: 38663
diff changeset
    87
        case None => null
57496c868dcc tuned Isabelle_Sidekick.complete: lock buffer, depend on document model;
wenzelm
parents: 38663
diff changeset
    88
        case Some(model) =>
57496c868dcc tuned Isabelle_Sidekick.complete: lock buffer, depend on document model;
wenzelm
parents: 38663
diff changeset
    89
          val line = buffer.getLineOfOffset(caret)
57496c868dcc tuned Isabelle_Sidekick.complete: lock buffer, depend on document model;
wenzelm
parents: 38663
diff changeset
    90
          val start = buffer.getLineStartOffset(line)
57496c868dcc tuned Isabelle_Sidekick.complete: lock buffer, depend on document model;
wenzelm
parents: 38663
diff changeset
    91
          val text = buffer.getSegment(start, caret - start)
34475
f963335dbc6b implemented IsabelleSideKickParser.complete
immler@in.tum.de
parents: 34440
diff changeset
    92
39624
57496c868dcc tuned Isabelle_Sidekick.complete: lock buffer, depend on document model;
wenzelm
parents: 38663
diff changeset
    93
          val completion = model.session.current_syntax().completion
57496c868dcc tuned Isabelle_Sidekick.complete: lock buffer, depend on document model;
wenzelm
parents: 38663
diff changeset
    94
          completion.complete(text) match {
57496c868dcc tuned Isabelle_Sidekick.complete: lock buffer, depend on document model;
wenzelm
parents: 38663
diff changeset
    95
            case None => null
57496c868dcc tuned Isabelle_Sidekick.complete: lock buffer, depend on document model;
wenzelm
parents: 38663
diff changeset
    96
            case Some((word, cs)) =>
57496c868dcc tuned Isabelle_Sidekick.complete: lock buffer, depend on document model;
wenzelm
parents: 38663
diff changeset
    97
              val ds =
57496c868dcc tuned Isabelle_Sidekick.complete: lock buffer, depend on document model;
wenzelm
parents: 38663
diff changeset
    98
                (if (Isabelle_Encoding.is_active(buffer))
57496c868dcc tuned Isabelle_Sidekick.complete: lock buffer, depend on document model;
wenzelm
parents: 38663
diff changeset
    99
                  cs.map(Isabelle.system.symbols.decode(_)).sortWith(_ < _)
57496c868dcc tuned Isabelle_Sidekick.complete: lock buffer, depend on document model;
wenzelm
parents: 38663
diff changeset
   100
                 else cs).filter(_ != word)
57496c868dcc tuned Isabelle_Sidekick.complete: lock buffer, depend on document model;
wenzelm
parents: 38663
diff changeset
   101
              if (ds.isEmpty) null
57496c868dcc tuned Isabelle_Sidekick.complete: lock buffer, depend on document model;
wenzelm
parents: 38663
diff changeset
   102
              else new SideKickCompletion(
57496c868dcc tuned Isabelle_Sidekick.complete: lock buffer, depend on document model;
wenzelm
parents: 38663
diff changeset
   103
                pane.getView, word, ds.toArray.asInstanceOf[Array[Object]]) { }
57496c868dcc tuned Isabelle_Sidekick.complete: lock buffer, depend on document model;
wenzelm
parents: 38663
diff changeset
   104
          }
57496c868dcc tuned Isabelle_Sidekick.complete: lock buffer, depend on document model;
wenzelm
parents: 38663
diff changeset
   105
      }
34611
b40e43d70ae9 use isabelle.Completion;
wenzelm
parents: 34609
diff changeset
   106
    }
34609
7ca1ef2f150d simplified and reactivated SideKickCompletion, cf. org.gjt.sp.jedit.gui.CompleteWord;
wenzelm
parents: 34562
diff changeset
   107
  }
34393
f0e1608a774f basic tree structure for sidekick
immler@in.tum.de
parents:
diff changeset
   108
}
36738
dce592144219 support several sidekick parsers -- very basic default parser;
wenzelm
parents: 36737
diff changeset
   109
dce592144219 support several sidekick parsers -- very basic default parser;
wenzelm
parents: 36737
diff changeset
   110
36759
wenzelm
parents: 36738
diff changeset
   111
class Isabelle_Sidekick_Default extends Isabelle_Sidekick("isabelle")
wenzelm
parents: 36738
diff changeset
   112
{
40455
e035dad8eca2 default Sidekick parser based on section headings;
wenzelm
parents: 40452
diff changeset
   113
  import Thy_Syntax.Structure
e035dad8eca2 default Sidekick parser based on section headings;
wenzelm
parents: 40452
diff changeset
   114
36759
wenzelm
parents: 36738
diff changeset
   115
  def parser(data: SideKickParsedData, model: Document_Model)
wenzelm
parents: 36738
diff changeset
   116
  {
40455
e035dad8eca2 default Sidekick parser based on section headings;
wenzelm
parents: 40452
diff changeset
   117
    val syntax = model.session.current_syntax()
e035dad8eca2 default Sidekick parser based on section headings;
wenzelm
parents: 40452
diff changeset
   118
40477
wenzelm
parents: 40475
diff changeset
   119
    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
   120
      entry match {
e035dad8eca2 default Sidekick parser based on section headings;
wenzelm
parents: 40452
diff changeset
   121
        case Structure.Block(name, body) =>
e035dad8eca2 default Sidekick parser based on section headings;
wenzelm
parents: 40452
diff changeset
   122
          val node =
e035dad8eca2 default Sidekick parser based on section headings;
wenzelm
parents: 40452
diff changeset
   123
            new DefaultMutableTreeNode(
40475
8a57ff2c2600 Sidekick block asset: show first line only;
wenzelm
parents: 40474
diff changeset
   124
              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
   125
          (offset /: body)((i, e) =>
e035dad8eca2 default Sidekick parser based on section headings;
wenzelm
parents: 40452
diff changeset
   126
            {
e035dad8eca2 default Sidekick parser based on section headings;
wenzelm
parents: 40452
diff changeset
   127
              make_tree(i, e) foreach (nd => node.add(nd))
e035dad8eca2 default Sidekick parser based on section headings;
wenzelm
parents: 40452
diff changeset
   128
              i + e.length
e035dad8eca2 default Sidekick parser based on section headings;
wenzelm
parents: 40452
diff changeset
   129
            })
e035dad8eca2 default Sidekick parser based on section headings;
wenzelm
parents: 40452
diff changeset
   130
          List(node)
e035dad8eca2 default Sidekick parser based on section headings;
wenzelm
parents: 40452
diff changeset
   131
        case Structure.Atom(command)
40458
12c8c64203b3 treat main theory commands like headings, and nest anything else inside;
wenzelm
parents: 40455
diff changeset
   132
        if command.is_command && syntax.heading_level(command).isEmpty =>
40455
e035dad8eca2 default Sidekick parser based on section headings;
wenzelm
parents: 40452
diff changeset
   133
          val node =
e035dad8eca2 default Sidekick parser based on section headings;
wenzelm
parents: 40452
diff changeset
   134
            new DefaultMutableTreeNode(
e035dad8eca2 default Sidekick parser based on section headings;
wenzelm
parents: 40452
diff changeset
   135
              new Isabelle_Sidekick.Asset(command.name, offset, offset + entry.length))
e035dad8eca2 default Sidekick parser based on section headings;
wenzelm
parents: 40452
diff changeset
   136
          List(node)
e035dad8eca2 default Sidekick parser based on section headings;
wenzelm
parents: 40452
diff changeset
   137
        case _ => Nil
e035dad8eca2 default Sidekick parser based on section headings;
wenzelm
parents: 40452
diff changeset
   138
      }
e035dad8eca2 default Sidekick parser based on section headings;
wenzelm
parents: 40452
diff changeset
   139
40474
576b88b1dce9 added buffer_text convenience, with explicit locking;
wenzelm
parents: 40458
diff changeset
   140
    val text = Isabelle.buffer_text(model.buffer)
40792
1d71a45590e4 tuned signature;
wenzelm
parents: 40477
diff changeset
   141
    val structure = Structure.parse(syntax, "theory " + model.thy_name, text)
40455
e035dad8eca2 default Sidekick parser based on section headings;
wenzelm
parents: 40452
diff changeset
   142
e035dad8eca2 default Sidekick parser based on section headings;
wenzelm
parents: 40452
diff changeset
   143
    make_tree(0, structure) foreach (node => data.root.add(node))
36759
wenzelm
parents: 36738
diff changeset
   144
  }
wenzelm
parents: 36738
diff changeset
   145
}
36738
dce592144219 support several sidekick parsers -- very basic default parser;
wenzelm
parents: 36737
diff changeset
   146
dce592144219 support several sidekick parsers -- very basic default parser;
wenzelm
parents: 36737
diff changeset
   147
36759
wenzelm
parents: 36738
diff changeset
   148
class Isabelle_Sidekick_Raw extends Isabelle_Sidekick("isabelle-raw")
wenzelm
parents: 36738
diff changeset
   149
{
wenzelm
parents: 36738
diff changeset
   150
  def parser(data: SideKickParsedData, model: Document_Model)
wenzelm
parents: 36738
diff changeset
   151
  {
wenzelm
parents: 36738
diff changeset
   152
    val root = data.root
38223
2a368e8e0a80 more explicit treatment of Swing thread context;
wenzelm
parents: 38152
diff changeset
   153
    val snapshot = Swing_Thread.now { model.snapshot() }  // FIXME cover all nodes (!??)
38569
9d480f6a2589 tuned signatures;
wenzelm
parents: 38564
diff changeset
   154
    for ((command, command_start) <- snapshot.node.command_range() if !stopped) {
38658
20d82e98bcd7 tuned root markup;
wenzelm
parents: 38640
diff changeset
   155
      snapshot.state(command).root_markup.swing_tree(root)((info: Text.Info[Any]) =>
36759
wenzelm
parents: 36738
diff changeset
   156
          {
38663
fcd56e6a04b9 tuned raw Sidekick output;
wenzelm
parents: 38658
diff changeset
   157
            val range = info.range + command_start
38577
4e4d3ea3725a renamed Markup_Tree.Node to Text.Info;
wenzelm
parents: 38569
diff changeset
   158
            val content = command.source(info.range).replace('\n', ' ')
38663
fcd56e6a04b9 tuned raw Sidekick output;
wenzelm
parents: 38658
diff changeset
   159
            val info_text =
fcd56e6a04b9 tuned raw Sidekick output;
wenzelm
parents: 38658
diff changeset
   160
              info.info match {
fcd56e6a04b9 tuned raw Sidekick output;
wenzelm
parents: 38658
diff changeset
   161
                case elem @ XML.Elem(_, _) =>
fcd56e6a04b9 tuned raw Sidekick output;
wenzelm
parents: 38658
diff changeset
   162
                  Pretty.formatted(List(elem), margin = 40).mkString("\n")
fcd56e6a04b9 tuned raw Sidekick output;
wenzelm
parents: 38658
diff changeset
   163
                case x => x.toString
fcd56e6a04b9 tuned raw Sidekick output;
wenzelm
parents: 38658
diff changeset
   164
              }
36738
dce592144219 support several sidekick parsers -- very basic default parser;
wenzelm
parents: 36737
diff changeset
   165
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
   166
            new DefaultMutableTreeNode(
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
   167
              new Isabelle_Sidekick.Asset(command.toString, range.start, range.stop) {
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
   168
                override def getShortString: String = content
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
   169
                override def getLongString: String = info_text
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
   170
                override def toString = "\"" + content + "\" " + range.toString
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
   171
              })
38479
e628da370072 more efficient Markup_Tree, based on branches sorted by quasi-order;
wenzelm
parents: 38426
diff changeset
   172
          })
36759
wenzelm
parents: 36738
diff changeset
   173
    }
wenzelm
parents: 36738
diff changeset
   174
  }
wenzelm
parents: 36738
diff changeset
   175
}
36738
dce592144219 support several sidekick parsers -- very basic default parser;
wenzelm
parents: 36737
diff changeset
   176