author | wenzelm |
Sun, 28 Nov 2010 19:35:14 +0100 | |
changeset 40792 | 1d71a45590e4 |
parent 40477 | 780c27276593 |
permissions | -rw-r--r-- |
36760 | 1 |
/* Title: Tools/jEdit/src/jedit/isabelle_sidekick.scala |
2 |
Author: Fabian Immler, TU Munich |
|
3 |
Author: Makarius |
|
4 |
||
5 |
SideKick parsers for Isabelle proof documents. |
|
6 |
*/ |
|
34393 | 7 |
|
34426
81f93e0f13b4
renamed isabelle.prover.IsabelleSKParser to isabelle.jedit.IsabelleSideKickParser;
wenzelm
parents:
34417
diff
changeset
|
8 |
package isabelle.jedit |
34393 | 9 |
|
34760 | 10 |
|
36015 | 11 |
import isabelle._ |
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 | 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 | 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 | 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 | 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 | 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 | 53 |
@volatile protected var stopped = false |
34503 | 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 | 56 |
def parser(data: SideKickParsedData, model: Document_Model): Unit |
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 | 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 | 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 | 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 | 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 | 106 |
} |
34609
7ca1ef2f150d
simplified and reactivated SideKickCompletion, cf. org.gjt.sp.jedit.gui.CompleteWord;
wenzelm
parents:
34562
diff
changeset
|
107 |
} |
34393 | 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 | 111 |
class Isabelle_Sidekick_Default extends Isabelle_Sidekick("isabelle") |
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 | 115 |
def parser(data: SideKickParsedData, model: Document_Model) |
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 | 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 | 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 | 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 | 144 |
} |
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 | 148 |
class Isabelle_Sidekick_Raw extends Isabelle_Sidekick("isabelle-raw") |
149 |
{ |
|
150 |
def parser(data: SideKickParsedData, model: Document_Model) |
|
151 |
{ |
|
152 |
val root = data.root |
|
38223 | 153 |
val snapshot = Swing_Thread.now { model.snapshot() } // FIXME cover all nodes (!??) |
38569 | 154 |
for ((command, command_start) <- snapshot.node.command_range() if !stopped) { |
38658 | 155 |
snapshot.state(command).root_markup.swing_tree(root)((info: Text.Info[Any]) => |
36759 | 156 |
{ |
38663 | 157 |
val range = info.range + command_start |
38577 | 158 |
val content = command.source(info.range).replace('\n', ' ') |
38663 | 159 |
val info_text = |
160 |
info.info match { |
|
161 |
case elem @ XML.Elem(_, _) => |
|
162 |
Pretty.formatted(List(elem), margin = 40).mkString("\n") |
|
163 |
case x => x.toString |
|
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 | 173 |
} |
174 |
} |
|
175 |
} |
|
36738
dce592144219
support several sidekick parsers -- very basic default parser;
wenzelm
parents:
36737
diff
changeset
|
176 |