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 */ |
|
7 |
|
8 package isabelle.jedit |
|
9 |
|
10 |
|
11 import isabelle._ |
|
12 |
|
13 import scala.collection.Set |
|
14 import scala.collection.immutable.TreeSet |
|
15 |
|
16 import javax.swing.tree.DefaultMutableTreeNode |
|
17 import javax.swing.text.Position |
|
18 import javax.swing.Icon |
|
19 |
|
20 import org.gjt.sp.jedit.{Buffer, EditPane, TextUtilities, View} |
|
21 import errorlist.DefaultErrorSource |
|
22 import sidekick.{SideKickParser, SideKickParsedData, SideKickCompletion, IAsset} |
|
23 |
|
24 |
|
25 object Isabelle_Sidekick |
|
26 { |
|
27 def int_to_pos(offset: Text.Offset): Position = |
|
28 new Position { def getOffset = offset; override def toString = offset.toString } |
|
29 |
|
30 class Asset(name: String, start: Text.Offset, end: Text.Offset) extends IAsset |
|
31 { |
|
32 protected var _name = name |
|
33 protected var _start = int_to_pos(start) |
|
34 protected var _end = int_to_pos(end) |
|
35 override def getIcon: Icon = null |
|
36 override def getShortString: String = _name |
|
37 override def getLongString: String = _name |
|
38 override def getName: String = _name |
|
39 override def setName(name: String) = _name = name |
|
40 override def getStart: Position = _start |
|
41 override def setStart(start: Position) = _start = start |
|
42 override def getEnd: Position = _end |
|
43 override def setEnd(end: Position) = _end = end |
|
44 override def toString = _name |
|
45 } |
|
46 } |
|
47 |
|
48 |
|
49 abstract class Isabelle_Sidekick(name: String) extends SideKickParser(name) |
|
50 { |
|
51 /* parsing */ |
|
52 |
|
53 @volatile protected var stopped = false |
|
54 override def stop() = { stopped = true } |
|
55 |
|
56 def parser(data: SideKickParsedData, model: Document_Model): Unit |
|
57 |
|
58 def parse(buffer: Buffer, error_source: DefaultErrorSource): SideKickParsedData = |
|
59 { |
|
60 stopped = false |
|
61 |
|
62 // FIXME lock buffer (!??) |
|
63 val data = new SideKickParsedData(buffer.getName) |
|
64 val root = data.root |
|
65 data.getAsset(root).setEnd(Isabelle_Sidekick.int_to_pos(buffer.getLength)) |
|
66 |
|
67 Swing_Thread.now { Document_Model(buffer) } match { |
|
68 case Some(model) => |
|
69 parser(data, model) |
|
70 if (stopped) root.add(new DefaultMutableTreeNode("<parser stopped>")) |
|
71 case None => root.add(new DefaultMutableTreeNode("<buffer inactive>")) |
|
72 } |
|
73 data |
|
74 } |
|
75 |
|
76 |
|
77 /* completion */ |
|
78 |
|
79 override def supportsCompletion = true |
|
80 override def canCompleteAnywhere = true |
|
81 |
|
82 override def complete(pane: EditPane, caret: Text.Offset): SideKickCompletion = |
|
83 { |
|
84 val buffer = pane.getBuffer |
|
85 Isabelle.swing_buffer_lock(buffer) { |
|
86 Document_Model(buffer) match { |
|
87 case None => null |
|
88 case Some(model) => |
|
89 val line = buffer.getLineOfOffset(caret) |
|
90 val start = buffer.getLineStartOffset(line) |
|
91 val text = buffer.getSegment(start, caret - start) |
|
92 |
|
93 val completion = model.session.current_syntax().completion |
|
94 completion.complete(text) match { |
|
95 case None => null |
|
96 case Some((word, cs)) => |
|
97 val ds = |
|
98 (if (Isabelle_Encoding.is_active(buffer)) |
|
99 cs.map(Isabelle.system.symbols.decode(_)).sortWith(_ < _) |
|
100 else cs).filter(_ != word) |
|
101 if (ds.isEmpty) null |
|
102 else new SideKickCompletion( |
|
103 pane.getView, word, ds.toArray.asInstanceOf[Array[Object]]) { } |
|
104 } |
|
105 } |
|
106 } |
|
107 } |
|
108 } |
|
109 |
|
110 |
|
111 class Isabelle_Sidekick_Default extends Isabelle_Sidekick("isabelle") |
|
112 { |
|
113 import Thy_Syntax.Structure |
|
114 |
|
115 def parser(data: SideKickParsedData, model: Document_Model) |
|
116 { |
|
117 val syntax = model.session.current_syntax() |
|
118 |
|
119 def make_tree(offset: Text.Offset, entry: Structure.Entry): List[DefaultMutableTreeNode] = |
|
120 entry match { |
|
121 case Structure.Block(name, body) => |
|
122 val node = |
|
123 new DefaultMutableTreeNode( |
|
124 new Isabelle_Sidekick.Asset(Library.first_line(name), offset, offset + entry.length)) |
|
125 (offset /: body)((i, e) => |
|
126 { |
|
127 make_tree(i, e) foreach (nd => node.add(nd)) |
|
128 i + e.length |
|
129 }) |
|
130 List(node) |
|
131 case Structure.Atom(command) |
|
132 if command.is_command && syntax.heading_level(command).isEmpty => |
|
133 val node = |
|
134 new DefaultMutableTreeNode( |
|
135 new Isabelle_Sidekick.Asset(command.name, offset, offset + entry.length)) |
|
136 List(node) |
|
137 case _ => Nil |
|
138 } |
|
139 |
|
140 val text = Isabelle.buffer_text(model.buffer) |
|
141 val structure = Structure.parse(syntax, "theory " + model.thy_name, text) |
|
142 |
|
143 make_tree(0, structure) foreach (node => data.root.add(node)) |
|
144 } |
|
145 } |
|
146 |
|
147 |
|
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 |
|
153 val snapshot = Swing_Thread.now { model.snapshot() } // FIXME cover all nodes (!??) |
|
154 for ((command, command_start) <- snapshot.node.command_range() if !stopped) { |
|
155 snapshot.state(command).root_markup.swing_tree(root)((info: Text.Info[Any]) => |
|
156 { |
|
157 val range = info.range + command_start |
|
158 val content = command.source(info.range).replace('\n', ' ') |
|
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 } |
|
165 |
|
166 new DefaultMutableTreeNode( |
|
167 new Isabelle_Sidekick.Asset(command.toString, range.start, range.stop) { |
|
168 override def getShortString: String = content |
|
169 override def getLongString: String = info_text |
|
170 override def toString = "\"" + content + "\" " + range.toString |
|
171 }) |
|
172 }) |
|
173 } |
|
174 } |
|
175 } |
|
176 |
|