author | wenzelm |
Fri, 01 Apr 2022 17:06:10 +0200 | |
changeset 75393 | 87ebf5a50283 |
parent 73987 | fc363a3b690a |
child 75435 | c8087e6bd2ce |
permissions | -rw-r--r-- |
66120 | 1 |
/* Title: Tools/jEdit/src/jedit_bibtex.scala |
58545
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} |
73617
20d0abffee99
more robust: avoid sporadic crash of JEditBuffer.tokenMarker.getMainRuleSet().getModeName();
wenzelm
parents:
67290
diff
changeset
|
23 |
import org.gjt.sp.jedit.syntax.{Token => JEditToken, TokenMarker, TokenHandler} |
58546 | 24 |
|
58545
30b75b7958d6
citation tooltip/hyperlink based on open buffers with .bib files;
wenzelm
parents:
diff
changeset
|
25 |
|
75393 | 26 |
object JEdit_Bibtex { |
58548 | 27 |
/** context menu **/ |
28 |
||
75393 | 29 |
def context_menu(text_area0: JEditTextArea): List[JMenuItem] = { |
58548 | 30 |
text_area0 match { |
31 |
case text_area: TextArea => |
|
32 |
text_area.getBuffer match { |
|
33 |
case buffer: Buffer |
|
67290 | 34 |
if (Bibtex.is_bibtex(JEdit_Lib.buffer_name(buffer)) && buffer.isEditable) => |
58548 | 35 |
val menu = new JMenu("BibTeX entries") |
66150 | 36 |
for (entry <- Bibtex.known_entries) { |
58548 | 37 |
val item = new JMenuItem(entry.kind) |
38 |
item.addActionListener(new ActionListener { |
|
39 |
def actionPerformed(evt: ActionEvent): Unit = |
|
40 |
Isabelle.insert_line_padding(text_area, entry.template) |
|
41 |
}) |
|
42 |
menu.add(item) |
|
43 |
} |
|
44 |
List(menu) |
|
45 |
case _ => Nil |
|
46 |
} |
|
47 |
case _ => Nil |
|
48 |
} |
|
49 |
} |
|
50 |
||
51 |
||
52 |
||
58546 | 53 |
/** token markup **/ |
54 |
||
55 |
/* token style */ |
|
56 |
||
57 |
private def token_style(context: String, token: Bibtex.Token): Byte = |
|
58 |
token.kind match { |
|
59 |
case Bibtex.Token.Kind.COMMAND => JEditToken.KEYWORD2 |
|
60 |
case Bibtex.Token.Kind.ENTRY => JEditToken.KEYWORD1 |
|
61 |
case Bibtex.Token.Kind.KEYWORD => JEditToken.OPERATOR |
|
62 |
case Bibtex.Token.Kind.NAT => JEditToken.LITERAL2 |
|
63 |
case Bibtex.Token.Kind.STRING => JEditToken.LITERAL1 |
|
64 |
case Bibtex.Token.Kind.NAME => JEditToken.LABEL |
|
65 |
case Bibtex.Token.Kind.IDENT => |
|
66 |
if (Bibtex.is_month(token.source)) JEditToken.LITERAL3 |
|
67 |
else |
|
68 |
Bibtex.get_entry(context) match { |
|
69 |
case Some(entry) if entry.is_required(token.source) => JEditToken.KEYWORD3 |
|
70 |
case Some(entry) if entry.is_optional(token.source) => JEditToken.KEYWORD4 |
|
71 |
case _ => JEditToken.DIGIT |
|
72 |
} |
|
73 |
case Bibtex.Token.Kind.SPACE => JEditToken.NULL |
|
74 |
case Bibtex.Token.Kind.COMMENT => JEditToken.COMMENT1 |
|
75 |
case Bibtex.Token.Kind.ERROR => JEditToken.INVALID |
|
76 |
} |
|
77 |
||
78 |
||
79 |
/* line context */ |
|
80 |
||
73617
20d0abffee99
more robust: avoid sporadic crash of JEditBuffer.tokenMarker.getMainRuleSet().getModeName();
wenzelm
parents:
67290
diff
changeset
|
81 |
private val mode_rule_set = Token_Markup.mode_rule_set("bibtex") |
58546 | 82 |
|
58699 | 83 |
private class Line_Context(val context: Option[Bibtex.Line_Context]) |
75393 | 84 |
extends TokenMarker.LineContext(mode_rule_set, null) { |
58699 | 85 |
override def hashCode: Int = context.hashCode |
86 |
override def equals(that: Any): Boolean = |
|
87 |
that match { |
|
88 |
case other: Line_Context => context == other.context |
|
89 |
case _ => false |
|
90 |
} |
|
91 |
} |
|
58546 | 92 |
|
93 |
||
94 |
/* token marker */ |
|
95 |
||
75393 | 96 |
class Token_Marker extends TokenMarker { |
73617
20d0abffee99
more robust: avoid sporadic crash of JEditBuffer.tokenMarker.getMainRuleSet().getModeName();
wenzelm
parents:
67290
diff
changeset
|
97 |
addRuleSet(mode_rule_set) |
20d0abffee99
more robust: avoid sporadic crash of JEditBuffer.tokenMarker.getMainRuleSet().getModeName();
wenzelm
parents:
67290
diff
changeset
|
98 |
|
75393 | 99 |
override def markTokens( |
100 |
context: TokenMarker.LineContext, |
|
101 |
handler: TokenHandler, |
|
102 |
raw_line: Segment |
|
103 |
): TokenMarker.LineContext = { |
|
58546 | 104 |
val line_ctxt = |
105 |
context match { |
|
106 |
case c: Line_Context => c.context |
|
58589 | 107 |
case _ => Some(Bibtex.Ignored) |
58546 | 108 |
} |
109 |
val line = if (raw_line == null) new Segment else raw_line |
|
110 |
||
75393 | 111 |
def no_markup = { |
58595
127f192b755c
more defensive error handling -- token marker must not crash;
wenzelm
parents:
58592
diff
changeset
|
112 |
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
|
113 |
(List(styled_token), new Line_Context(None)) |
127f192b755c
more defensive error handling -- token marker must not crash;
wenzelm
parents:
58592
diff
changeset
|
114 |
} |
127f192b755c
more defensive error handling -- token marker must not crash;
wenzelm
parents:
58592
diff
changeset
|
115 |
|
75393 | 116 |
val context1 = { |
58546 | 117 |
val (styled_tokens, context1) = |
118 |
line_ctxt match { |
|
119 |
case Some(ctxt) => |
|
58595
127f192b755c
more defensive error handling -- token marker must not crash;
wenzelm
parents:
58592
diff
changeset
|
120 |
try { |
127f192b755c
more defensive error handling -- token marker must not crash;
wenzelm
parents:
58592
diff
changeset
|
121 |
val (chunks, ctxt1) = Bibtex.parse_line(line, ctxt) |
127f192b755c
more defensive error handling -- token marker must not crash;
wenzelm
parents:
58592
diff
changeset
|
122 |
val styled_tokens = |
127f192b755c
more defensive error handling -- token marker must not crash;
wenzelm
parents:
58592
diff
changeset
|
123 |
for { chunk <- chunks; tok <- chunk.tokens } |
127f192b755c
more defensive error handling -- token marker must not crash;
wenzelm
parents:
58592
diff
changeset
|
124 |
yield (token_style(chunk.kind, tok), tok.source) |
127f192b755c
more defensive error handling -- token marker must not crash;
wenzelm
parents:
58592
diff
changeset
|
125 |
(styled_tokens, new Line_Context(Some(ctxt1))) |
127f192b755c
more defensive error handling -- token marker must not crash;
wenzelm
parents:
58592
diff
changeset
|
126 |
} |
127f192b755c
more defensive error handling -- token marker must not crash;
wenzelm
parents:
58592
diff
changeset
|
127 |
catch { case ERROR(msg) => Output.warning(msg); no_markup } |
127f192b755c
more defensive error handling -- token marker must not crash;
wenzelm
parents:
58592
diff
changeset
|
128 |
case None => no_markup |
58546 | 129 |
} |
130 |
||
131 |
var offset = 0 |
|
132 |
for ((style, token) <- styled_tokens) { |
|
133 |
val length = token.length |
|
134 |
val end_offset = offset + length |
|
135 |
||
136 |
if ((offset until end_offset).exists(i => line.charAt(i) == '\t')) { |
|
137 |
for (i <- offset until end_offset) |
|
138 |
handler.handleToken(line, style, i, 1, context1) |
|
139 |
} |
|
140 |
else handler.handleToken(line, style, offset, length, context1) |
|
141 |
||
142 |
offset += length |
|
143 |
} |
|
144 |
handler.handleToken(line, JEditToken.END, line.count, 0, context1) |
|
145 |
context1 |
|
146 |
} |
|
147 |
val context2 = context1.intern |
|
148 |
handler.setLineContext(context2) |
|
149 |
context2 |
|
150 |
} |
|
151 |
} |
|
58545
30b75b7958d6
citation tooltip/hyperlink based on open buffers with .bib files;
wenzelm
parents:
diff
changeset
|
152 |
} |