author | wenzelm |
Thu, 16 Oct 2014 21:24:42 +0200 | |
changeset 58696 | 6b7445774ce3 |
parent 58694 | 983e98da2a42 |
child 58697 | 5bc1d6c4a499 |
permissions | -rw-r--r-- |
58545
30b75b7958d6
citation tooltip/hyperlink based on open buffers with .bib files;
wenzelm
parents:
diff
changeset
|
1 |
/* Title: Tools/jEdit/src/bibtex_jedit.scala |
30b75b7958d6
citation tooltip/hyperlink based on open buffers with .bib files;
wenzelm
parents:
diff
changeset
|
2 |
Author: Makarius |
30b75b7958d6
citation tooltip/hyperlink based on open buffers with .bib files;
wenzelm
parents:
diff
changeset
|
3 |
|
30b75b7958d6
citation tooltip/hyperlink based on open buffers with .bib files;
wenzelm
parents:
diff
changeset
|
4 |
BibTeX support in Isabelle/jEdit. |
30b75b7958d6
citation tooltip/hyperlink based on open buffers with .bib files;
wenzelm
parents:
diff
changeset
|
5 |
*/ |
30b75b7958d6
citation tooltip/hyperlink based on open buffers with .bib files;
wenzelm
parents:
diff
changeset
|
6 |
|
30b75b7958d6
citation tooltip/hyperlink based on open buffers with .bib files;
wenzelm
parents:
diff
changeset
|
7 |
package isabelle.jedit |
30b75b7958d6
citation tooltip/hyperlink based on open buffers with .bib files;
wenzelm
parents:
diff
changeset
|
8 |
|
30b75b7958d6
citation tooltip/hyperlink based on open buffers with .bib files;
wenzelm
parents:
diff
changeset
|
9 |
|
30b75b7958d6
citation tooltip/hyperlink based on open buffers with .bib files;
wenzelm
parents:
diff
changeset
|
10 |
import isabelle._ |
30b75b7958d6
citation tooltip/hyperlink based on open buffers with .bib files;
wenzelm
parents:
diff
changeset
|
11 |
|
30b75b7958d6
citation tooltip/hyperlink based on open buffers with .bib files;
wenzelm
parents:
diff
changeset
|
12 |
|
58547 | 13 |
import scala.collection.mutable |
14 |
||
58548 | 15 |
import java.awt.event.{ActionListener, ActionEvent} |
16 |
||
58546 | 17 |
import javax.swing.text.Segment |
18 |
import javax.swing.tree.DefaultMutableTreeNode |
|
58548 | 19 |
import javax.swing.{JMenu, JMenuItem} |
58546 | 20 |
|
58545
30b75b7958d6
citation tooltip/hyperlink based on open buffers with .bib files;
wenzelm
parents:
diff
changeset
|
21 |
import org.gjt.sp.jedit.Buffer |
58548 | 22 |
import org.gjt.sp.jedit.textarea.{JEditTextArea, TextArea} |
58546 | 23 |
import org.gjt.sp.jedit.syntax.{Token => JEditToken, TokenMarker, TokenHandler, ParserRuleSet} |
24 |
||
25 |
import sidekick.{SideKickParser, SideKickParsedData} |
|
58545
30b75b7958d6
citation tooltip/hyperlink based on open buffers with .bib files;
wenzelm
parents:
diff
changeset
|
26 |
|
30b75b7958d6
citation tooltip/hyperlink based on open buffers with .bib files;
wenzelm
parents:
diff
changeset
|
27 |
|
30b75b7958d6
citation tooltip/hyperlink based on open buffers with .bib files;
wenzelm
parents:
diff
changeset
|
28 |
object Bibtex_JEdit |
30b75b7958d6
citation tooltip/hyperlink based on open buffers with .bib files;
wenzelm
parents:
diff
changeset
|
29 |
{ |
58546 | 30 |
/** buffer model **/ |
31 |
||
58592 | 32 |
/* file type */ |
33 |
||
58546 | 34 |
def check(buffer: Buffer): Boolean = |
35 |
JEdit_Lib.buffer_name(buffer).endsWith(".bib") |
|
58545
30b75b7958d6
citation tooltip/hyperlink based on open buffers with .bib files;
wenzelm
parents:
diff
changeset
|
36 |
|
58592 | 37 |
|
38 |
/* parse entries */ |
|
39 |
||
58547 | 40 |
def parse_buffer_entries(buffer: Buffer): List[(String, Text.Offset)] = |
41 |
{ |
|
42 |
val chunks = |
|
43 |
try { Bibtex.parse(JEdit_Lib.buffer_text(buffer)) } |
|
44 |
catch { case ERROR(msg) => Output.warning(msg); Nil } |
|
45 |
||
46 |
val result = new mutable.ListBuffer[(String, Text.Offset)] |
|
47 |
var offset = 0 |
|
48 |
for (chunk <- chunks) { |
|
49 |
if (chunk.name != "" && !chunk.is_command) result += ((chunk.name, offset)) |
|
50 |
offset += chunk.source.length |
|
51 |
} |
|
52 |
result.toList |
|
53 |
} |
|
54 |
||
58592 | 55 |
|
56 |
/* retrieve entries */ |
|
57 |
||
58545
30b75b7958d6
citation tooltip/hyperlink based on open buffers with .bib files;
wenzelm
parents:
diff
changeset
|
58 |
def entries_iterator(): Iterator[(String, Buffer, Text.Offset)] = |
30b75b7958d6
citation tooltip/hyperlink based on open buffers with .bib files;
wenzelm
parents:
diff
changeset
|
59 |
for { |
30b75b7958d6
citation tooltip/hyperlink based on open buffers with .bib files;
wenzelm
parents:
diff
changeset
|
60 |
buffer <- JEdit_Lib.jedit_buffers() |
30b75b7958d6
citation tooltip/hyperlink based on open buffers with .bib files;
wenzelm
parents:
diff
changeset
|
61 |
model <- PIDE.document_model(buffer).iterator |
30b75b7958d6
citation tooltip/hyperlink based on open buffers with .bib files;
wenzelm
parents:
diff
changeset
|
62 |
(name, offset) <- model.bibtex_entries.iterator |
30b75b7958d6
citation tooltip/hyperlink based on open buffers with .bib files;
wenzelm
parents:
diff
changeset
|
63 |
} yield (name, buffer, offset) |
58546 | 64 |
|
65 |
||
58592 | 66 |
/* completion */ |
67 |
||
68 |
def complete(name: String): List[String] = |
|
69 |
{ |
|
70 |
val name1 = name.toLowerCase |
|
71 |
(for ((entry, _, _) <- entries_iterator() if entry.toLowerCase.containsSlice(name1)) |
|
72 |
yield entry).toList |
|
73 |
} |
|
74 |
||
75 |
def completion( |
|
76 |
history: Completion.History, |
|
77 |
text_area: JEditTextArea, |
|
78 |
rendering: Rendering): Option[Completion.Result] = |
|
79 |
{ |
|
80 |
for { |
|
81 |
Text.Info(r, name) <- rendering.citation(JEdit_Lib.before_caret_range(text_area, rendering)) |
|
82 |
original <- JEdit_Lib.try_get_text(text_area.getBuffer, r) |
|
83 |
orig = Library.perhaps_unquote(original) |
|
84 |
entries = complete(name).filter(_ != orig) |
|
85 |
if !entries.isEmpty |
|
86 |
items = |
|
87 |
entries.map({ |
|
88 |
case entry => |
|
89 |
val full_name = Long_Name.qualify(Markup.CITATION, entry) |
|
90 |
val description = List(entry, "(BibTeX entry)") |
|
91 |
val replacement = quote(entry) |
|
92 |
Completion.Item(r, original, full_name, description, replacement, 0, false) |
|
93 |
}).sorted(history.ordering).take(PIDE.options.int("completion_limit")) |
|
94 |
} yield Completion.Result(r, original, false, items) |
|
95 |
} |
|
96 |
||
97 |
||
58546 | 98 |
|
58548 | 99 |
/** context menu **/ |
100 |
||
101 |
def context_menu(text_area0: JEditTextArea): List[JMenuItem] = |
|
102 |
{ |
|
103 |
text_area0 match { |
|
104 |
case text_area: TextArea => |
|
105 |
text_area.getBuffer match { |
|
106 |
case buffer: Buffer |
|
107 |
if (check(buffer) && buffer.isEditable) => |
|
108 |
val menu = new JMenu("BibTeX entries") |
|
109 |
for (entry <- Bibtex.entries) { |
|
110 |
val item = new JMenuItem(entry.kind) |
|
111 |
item.addActionListener(new ActionListener { |
|
112 |
def actionPerformed(evt: ActionEvent): Unit = |
|
113 |
Isabelle.insert_line_padding(text_area, entry.template) |
|
114 |
}) |
|
115 |
menu.add(item) |
|
116 |
} |
|
117 |
List(menu) |
|
118 |
case _ => Nil |
|
119 |
} |
|
120 |
case _ => Nil |
|
121 |
} |
|
122 |
} |
|
123 |
||
124 |
||
125 |
||
58546 | 126 |
/** token markup **/ |
127 |
||
128 |
/* token style */ |
|
129 |
||
130 |
private def token_style(context: String, token: Bibtex.Token): Byte = |
|
131 |
token.kind match { |
|
132 |
case Bibtex.Token.Kind.COMMAND => JEditToken.KEYWORD2 |
|
133 |
case Bibtex.Token.Kind.ENTRY => JEditToken.KEYWORD1 |
|
134 |
case Bibtex.Token.Kind.KEYWORD => JEditToken.OPERATOR |
|
135 |
case Bibtex.Token.Kind.NAT => JEditToken.LITERAL2 |
|
136 |
case Bibtex.Token.Kind.STRING => JEditToken.LITERAL1 |
|
137 |
case Bibtex.Token.Kind.NAME => JEditToken.LABEL |
|
138 |
case Bibtex.Token.Kind.IDENT => |
|
139 |
if (Bibtex.is_month(token.source)) JEditToken.LITERAL3 |
|
140 |
else |
|
141 |
Bibtex.get_entry(context) match { |
|
142 |
case Some(entry) if entry.is_required(token.source) => JEditToken.KEYWORD3 |
|
143 |
case Some(entry) if entry.is_optional(token.source) => JEditToken.KEYWORD4 |
|
144 |
case _ => JEditToken.DIGIT |
|
145 |
} |
|
146 |
case Bibtex.Token.Kind.SPACE => JEditToken.NULL |
|
147 |
case Bibtex.Token.Kind.COMMENT => JEditToken.COMMENT1 |
|
148 |
case Bibtex.Token.Kind.ERROR => JEditToken.INVALID |
|
149 |
} |
|
150 |
||
151 |
||
152 |
/* line context */ |
|
153 |
||
154 |
private val context_rules = new ParserRuleSet("bibtex", "MAIN") |
|
155 |
||
156 |
private class Line_Context(context: Option[Bibtex.Line_Context]) |
|
58696 | 157 |
extends Token_Markup.Generic_Line_Context[Bibtex.Line_Context]( |
158 |
context_rules, context, Outer_Syntax.Line_Nesting.init) |
|
58546 | 159 |
|
160 |
||
161 |
/* token marker */ |
|
162 |
||
163 |
class Token_Marker extends TokenMarker |
|
164 |
{ |
|
165 |
override def markTokens(context: TokenMarker.LineContext, |
|
166 |
handler: TokenHandler, raw_line: Segment): TokenMarker.LineContext = |
|
167 |
{ |
|
168 |
val line_ctxt = |
|
169 |
context match { |
|
170 |
case c: Line_Context => c.context |
|
58589 | 171 |
case _ => Some(Bibtex.Ignored) |
58546 | 172 |
} |
173 |
val line = if (raw_line == null) new Segment else raw_line |
|
174 |
||
58595
127f192b755c
more defensive error handling -- token marker must not crash;
wenzelm
parents:
58592
diff
changeset
|
175 |
def no_markup = |
127f192b755c
more defensive error handling -- token marker must not crash;
wenzelm
parents:
58592
diff
changeset
|
176 |
{ |
127f192b755c
more defensive error handling -- token marker must not crash;
wenzelm
parents:
58592
diff
changeset
|
177 |
val styled_token = (JEditToken.NULL, line.subSequence(0, line.count).toString) |
127f192b755c
more defensive error handling -- token marker must not crash;
wenzelm
parents:
58592
diff
changeset
|
178 |
(List(styled_token), new Line_Context(None)) |
127f192b755c
more defensive error handling -- token marker must not crash;
wenzelm
parents:
58592
diff
changeset
|
179 |
} |
127f192b755c
more defensive error handling -- token marker must not crash;
wenzelm
parents:
58592
diff
changeset
|
180 |
|
58546 | 181 |
val context1 = |
182 |
{ |
|
183 |
val (styled_tokens, context1) = |
|
184 |
line_ctxt match { |
|
185 |
case Some(ctxt) => |
|
58595
127f192b755c
more defensive error handling -- token marker must not crash;
wenzelm
parents:
58592
diff
changeset
|
186 |
try { |
127f192b755c
more defensive error handling -- token marker must not crash;
wenzelm
parents:
58592
diff
changeset
|
187 |
val (chunks, ctxt1) = Bibtex.parse_line(line, ctxt) |
127f192b755c
more defensive error handling -- token marker must not crash;
wenzelm
parents:
58592
diff
changeset
|
188 |
val styled_tokens = |
127f192b755c
more defensive error handling -- token marker must not crash;
wenzelm
parents:
58592
diff
changeset
|
189 |
for { chunk <- chunks; tok <- chunk.tokens } |
127f192b755c
more defensive error handling -- token marker must not crash;
wenzelm
parents:
58592
diff
changeset
|
190 |
yield (token_style(chunk.kind, tok), tok.source) |
127f192b755c
more defensive error handling -- token marker must not crash;
wenzelm
parents:
58592
diff
changeset
|
191 |
(styled_tokens, new Line_Context(Some(ctxt1))) |
127f192b755c
more defensive error handling -- token marker must not crash;
wenzelm
parents:
58592
diff
changeset
|
192 |
} |
127f192b755c
more defensive error handling -- token marker must not crash;
wenzelm
parents:
58592
diff
changeset
|
193 |
catch { case ERROR(msg) => Output.warning(msg); no_markup } |
127f192b755c
more defensive error handling -- token marker must not crash;
wenzelm
parents:
58592
diff
changeset
|
194 |
case None => no_markup |
58546 | 195 |
} |
196 |
||
197 |
var offset = 0 |
|
198 |
for ((style, token) <- styled_tokens) { |
|
199 |
val length = token.length |
|
200 |
val end_offset = offset + length |
|
201 |
||
202 |
if ((offset until end_offset).exists(i => line.charAt(i) == '\t')) { |
|
203 |
for (i <- offset until end_offset) |
|
204 |
handler.handleToken(line, style, i, 1, context1) |
|
205 |
} |
|
206 |
else handler.handleToken(line, style, offset, length, context1) |
|
207 |
||
208 |
offset += length |
|
209 |
} |
|
210 |
handler.handleToken(line, JEditToken.END, line.count, 0, context1) |
|
211 |
context1 |
|
212 |
} |
|
213 |
val context2 = context1.intern |
|
214 |
handler.setLineContext(context2) |
|
215 |
context2 |
|
216 |
} |
|
217 |
} |
|
218 |
||
219 |
||
220 |
||
221 |
/** Sidekick parser **/ |
|
222 |
||
223 |
class Sidekick_Parser extends SideKickParser("bibtex") |
|
224 |
{ |
|
225 |
override def supportsCompletion = false |
|
226 |
||
227 |
private class Asset( |
|
228 |
label: String, label_html: String, start: Text.Offset, stop: Text.Offset, source: String) |
|
229 |
extends Isabelle_Sidekick.Asset(label, start, stop) { |
|
230 |
override def getShortString: String = label_html |
|
231 |
override def getLongString: String = source |
|
232 |
} |
|
233 |
||
234 |
def parse(buffer: Buffer, error_source: errorlist.DefaultErrorSource): SideKickParsedData = |
|
235 |
{ |
|
236 |
val data = Isabelle_Sidekick.root_data(buffer) |
|
237 |
||
238 |
try { |
|
239 |
var offset = 0 |
|
240 |
for (chunk <- Bibtex.parse(JEdit_Lib.buffer_text(buffer))) { |
|
241 |
val kind = chunk.kind |
|
242 |
val name = chunk.name |
|
243 |
val source = chunk.source |
|
244 |
if (kind != "") { |
|
245 |
val label = kind + (if (name == "") "" else " " + name) |
|
246 |
val label_html = |
|
247 |
"<html><b>" + kind + "</b>" + (if (name == "") "" else " " + name) + "</html>" |
|
248 |
val asset = new Asset(label, label_html, offset, offset + source.size, source) |
|
249 |
data.root.add(new DefaultMutableTreeNode(asset)) |
|
250 |
} |
|
251 |
offset += source.size |
|
252 |
} |
|
253 |
data |
|
254 |
} |
|
58595
127f192b755c
more defensive error handling -- token marker must not crash;
wenzelm
parents:
58592
diff
changeset
|
255 |
catch { case ERROR(msg) => Output.warning(msg); null } |
58546 | 256 |
} |
257 |
} |
|
58545
30b75b7958d6
citation tooltip/hyperlink based on open buffers with .bib files;
wenzelm
parents:
diff
changeset
|
258 |
} |
30b75b7958d6
citation tooltip/hyperlink based on open buffers with .bib files;
wenzelm
parents:
diff
changeset
|
259 |