1/* Title: Tools/jEdit/src/jedit_bibtex.scala 2 Author: Makarius 3 4BibTeX support in Isabelle/jEdit. 5*/ 6 7package isabelle.jedit 8 9 10import isabelle._ 11 12 13import scala.collection.mutable 14 15import java.awt.event.{ActionListener, ActionEvent} 16 17import javax.swing.text.Segment 18import javax.swing.tree.DefaultMutableTreeNode 19import javax.swing.{JMenu, JMenuItem} 20 21import org.gjt.sp.jedit.Buffer 22import org.gjt.sp.jedit.textarea.{JEditTextArea, TextArea} 23import org.gjt.sp.jedit.syntax.{Token => JEditToken, TokenMarker, TokenHandler, ParserRuleSet} 24 25import sidekick.{SideKickParser, SideKickParsedData} 26 27 28object JEdit_Bibtex 29{ 30 /** context menu **/ 31 32 def context_menu(text_area0: JEditTextArea): List[JMenuItem] = 33 { 34 text_area0 match { 35 case text_area: TextArea => 36 text_area.getBuffer match { 37 case buffer: Buffer 38 if (Bibtex.is_bibtex(JEdit_Lib.buffer_name(buffer)) && buffer.isEditable) => 39 val menu = new JMenu("BibTeX entries") 40 for (entry <- Bibtex.known_entries) { 41 val item = new JMenuItem(entry.kind) 42 item.addActionListener(new ActionListener { 43 def actionPerformed(evt: ActionEvent): Unit = 44 Isabelle.insert_line_padding(text_area, entry.template) 45 }) 46 menu.add(item) 47 } 48 List(menu) 49 case _ => Nil 50 } 51 case _ => Nil 52 } 53 } 54 55 56 57 /** token markup **/ 58 59 /* token style */ 60 61 private def token_style(context: String, token: Bibtex.Token): Byte = 62 token.kind match { 63 case Bibtex.Token.Kind.COMMAND => JEditToken.KEYWORD2 64 case Bibtex.Token.Kind.ENTRY => JEditToken.KEYWORD1 65 case Bibtex.Token.Kind.KEYWORD => JEditToken.OPERATOR 66 case Bibtex.Token.Kind.NAT => JEditToken.LITERAL2 67 case Bibtex.Token.Kind.STRING => JEditToken.LITERAL1 68 case Bibtex.Token.Kind.NAME => JEditToken.LABEL 69 case Bibtex.Token.Kind.IDENT => 70 if (Bibtex.is_month(token.source)) JEditToken.LITERAL3 71 else 72 Bibtex.get_entry(context) match { 73 case Some(entry) if entry.is_required(token.source) => JEditToken.KEYWORD3 74 case Some(entry) if entry.is_optional(token.source) => JEditToken.KEYWORD4 75 case _ => JEditToken.DIGIT 76 } 77 case Bibtex.Token.Kind.SPACE => JEditToken.NULL 78 case Bibtex.Token.Kind.COMMENT => JEditToken.COMMENT1 79 case Bibtex.Token.Kind.ERROR => JEditToken.INVALID 80 } 81 82 83 /* line context */ 84 85 private val context_rules = new ParserRuleSet("bibtex", "MAIN") 86 87 private class Line_Context(val context: Option[Bibtex.Line_Context]) 88 extends TokenMarker.LineContext(context_rules, null) 89 { 90 override def hashCode: Int = context.hashCode 91 override def equals(that: Any): Boolean = 92 that match { 93 case other: Line_Context => context == other.context 94 case _ => false 95 } 96 } 97 98 99 /* token marker */ 100 101 class Token_Marker extends TokenMarker 102 { 103 override def markTokens(context: TokenMarker.LineContext, 104 handler: TokenHandler, raw_line: Segment): TokenMarker.LineContext = 105 { 106 val line_ctxt = 107 context match { 108 case c: Line_Context => c.context 109 case _ => Some(Bibtex.Ignored) 110 } 111 val line = if (raw_line == null) new Segment else raw_line 112 113 def no_markup = 114 { 115 val styled_token = (JEditToken.NULL, line.subSequence(0, line.count).toString) 116 (List(styled_token), new Line_Context(None)) 117 } 118 119 val context1 = 120 { 121 val (styled_tokens, context1) = 122 line_ctxt match { 123 case Some(ctxt) => 124 try { 125 val (chunks, ctxt1) = Bibtex.parse_line(line, ctxt) 126 val styled_tokens = 127 for { chunk <- chunks; tok <- chunk.tokens } 128 yield (token_style(chunk.kind, tok), tok.source) 129 (styled_tokens, new Line_Context(Some(ctxt1))) 130 } 131 catch { case ERROR(msg) => Output.warning(msg); no_markup } 132 case None => no_markup 133 } 134 135 var offset = 0 136 for ((style, token) <- styled_tokens) { 137 val length = token.length 138 val end_offset = offset + length 139 140 if ((offset until end_offset).exists(i => line.charAt(i) == '\t')) { 141 for (i <- offset until end_offset) 142 handler.handleToken(line, style, i, 1, context1) 143 } 144 else handler.handleToken(line, style, offset, length, context1) 145 146 offset += length 147 } 148 handler.handleToken(line, JEditToken.END, line.count, 0, context1) 149 context1 150 } 151 val context2 = context1.intern 152 handler.setLineContext(context2) 153 context2 154 } 155 } 156 157 158 159 /** Sidekick parser **/ 160 161 class Sidekick_Parser extends SideKickParser("bibtex") 162 { 163 override def supportsCompletion = false 164 165 private class Asset(label: String, label_html: String, range: Text.Range, source: String) 166 extends Isabelle_Sidekick.Asset(label, range) { 167 override def getShortString: String = label_html 168 override def getLongString: String = source 169 } 170 171 def parse(buffer: Buffer, error_source: errorlist.DefaultErrorSource): SideKickParsedData = 172 { 173 val data = Isabelle_Sidekick.root_data(buffer) 174 175 try { 176 var offset = 0 177 for (chunk <- Bibtex.parse(JEdit_Lib.buffer_text(buffer))) { 178 val kind = chunk.kind 179 val name = chunk.name 180 val source = chunk.source 181 if (kind != "") { 182 val label = kind + (if (name == "") "" else " " + name) 183 val label_html = 184 "<html><b>" + HTML.output(kind) + "</b>" + 185 (if (name == "") "" else " " + HTML.output(name)) + "</html>" 186 val range = Text.Range(offset, offset + source.length) 187 val asset = new Asset(label, label_html, range, source) 188 data.root.add(new DefaultMutableTreeNode(asset)) 189 } 190 offset += source.length 191 } 192 data 193 } 194 catch { case ERROR(msg) => Output.warning(msg); null } 195 } 196 } 197} 198