19 import javax.swing.{JMenu, JMenuItem} |
19 import javax.swing.{JMenu, JMenuItem} |
20 |
20 |
21 import org.gjt.sp.jedit.Buffer |
21 import org.gjt.sp.jedit.Buffer |
22 import org.gjt.sp.jedit.textarea.{JEditTextArea, TextArea} |
22 import org.gjt.sp.jedit.textarea.{JEditTextArea, TextArea} |
23 import org.gjt.sp.jedit.syntax.{Token => JEditToken, TokenMarker, TokenHandler} |
23 import org.gjt.sp.jedit.syntax.{Token => JEditToken, TokenMarker, TokenHandler} |
24 |
|
25 import sidekick.{SideKickParser, SideKickParsedData} |
|
26 |
24 |
27 |
25 |
28 object JEdit_Bibtex |
26 object JEdit_Bibtex |
29 { |
27 { |
30 /** context menu **/ |
28 /** context menu **/ |
153 val context2 = context1.intern |
151 val context2 = context1.intern |
154 handler.setLineContext(context2) |
152 handler.setLineContext(context2) |
155 context2 |
153 context2 |
156 } |
154 } |
157 } |
155 } |
158 |
|
159 |
|
160 |
|
161 /** Sidekick parser **/ |
|
162 |
|
163 class Sidekick_Parser extends SideKickParser("bibtex") |
|
164 { |
|
165 override def supportsCompletion = false |
|
166 |
|
167 private class Asset(label: String, label_html: String, range: Text.Range, source: String) |
|
168 extends Isabelle_Sidekick.Asset(label, range) { |
|
169 override def getShortString: String = label_html |
|
170 override def getLongString: String = source |
|
171 } |
|
172 |
|
173 def parse(buffer: Buffer, error_source: errorlist.DefaultErrorSource): SideKickParsedData = |
|
174 { |
|
175 val data = Isabelle_Sidekick.root_data(buffer) |
|
176 |
|
177 try { |
|
178 var offset = 0 |
|
179 for (chunk <- Bibtex.parse(JEdit_Lib.buffer_text(buffer))) { |
|
180 val kind = chunk.kind |
|
181 val name = chunk.name |
|
182 val source = chunk.source |
|
183 if (kind != "") { |
|
184 val label = kind + (if (name == "") "" else " " + name) |
|
185 val label_html = |
|
186 "<html><b>" + HTML.output(kind) + "</b>" + |
|
187 (if (name == "") "" else " " + HTML.output(name)) + "</html>" |
|
188 val range = Text.Range(offset, offset + source.length) |
|
189 val asset = new Asset(label, label_html, range, source) |
|
190 data.root.add(new DefaultMutableTreeNode(asset)) |
|
191 } |
|
192 offset += source.length |
|
193 } |
|
194 data |
|
195 } |
|
196 catch { case ERROR(msg) => Output.warning(msg); null } |
|
197 } |
|
198 } |
|
199 } |
156 } |