# HG changeset patch
# User wenzelm
# Date 1412525666 -7200
# Node ID 72e2b2a609c4c1c75617d1e1bc64df8a1ed140ba
# Parent 30b75b7958d62c074b9b76b0ca2473b3de9f1229
clarified modules;
diff -r 30b75b7958d6 -r 72e2b2a609c4 src/Tools/jEdit/lib/Tools/jedit
--- a/src/Tools/jEdit/lib/Tools/jedit Sun Oct 05 17:58:36 2014 +0200
+++ b/src/Tools/jEdit/lib/Tools/jedit Sun Oct 05 18:14:26 2014 +0200
@@ -10,7 +10,6 @@
declare -a SOURCES=(
"src/active.scala"
"src/bibtex_jedit.scala"
- "src/bibtex_token_markup.scala"
"src/completion_popup.scala"
"src/context_menu.scala"
"src/dockable.scala"
diff -r 30b75b7958d6 -r 72e2b2a609c4 src/Tools/jEdit/src/bibtex_jedit.scala
--- a/src/Tools/jEdit/src/bibtex_jedit.scala Sun Oct 05 17:58:36 2014 +0200
+++ b/src/Tools/jEdit/src/bibtex_jedit.scala Sun Oct 05 18:14:26 2014 +0200
@@ -10,12 +10,21 @@
import isabelle._
+import javax.swing.text.Segment
+import javax.swing.tree.DefaultMutableTreeNode
+
import org.gjt.sp.jedit.Buffer
+import org.gjt.sp.jedit.syntax.{Token => JEditToken, TokenMarker, TokenHandler, ParserRuleSet}
+
+import sidekick.{SideKickParser, SideKickParsedData}
object Bibtex_JEdit
{
- /* buffer model entries */
+ /** buffer model **/
+
+ def check(buffer: Buffer): Boolean =
+ JEdit_Lib.buffer_name(buffer).endsWith(".bib")
def entries_iterator(): Iterator[(String, Buffer, Text.Offset)] =
for {
@@ -23,5 +32,132 @@
model <- PIDE.document_model(buffer).iterator
(name, offset) <- model.bibtex_entries.iterator
} yield (name, buffer, offset)
+
+
+
+ /** token markup **/
+
+ /* token style */
+
+ private def token_style(context: String, token: Bibtex.Token): Byte =
+ token.kind match {
+ case Bibtex.Token.Kind.COMMAND => JEditToken.KEYWORD2
+ case Bibtex.Token.Kind.ENTRY => JEditToken.KEYWORD1
+ case Bibtex.Token.Kind.KEYWORD => JEditToken.OPERATOR
+ case Bibtex.Token.Kind.NAT => JEditToken.LITERAL2
+ case Bibtex.Token.Kind.STRING => JEditToken.LITERAL1
+ case Bibtex.Token.Kind.NAME => JEditToken.LABEL
+ case Bibtex.Token.Kind.IDENT =>
+ if (Bibtex.is_month(token.source)) JEditToken.LITERAL3
+ else
+ Bibtex.get_entry(context) match {
+ case Some(entry) if entry.is_required(token.source) => JEditToken.KEYWORD3
+ case Some(entry) if entry.is_optional(token.source) => JEditToken.KEYWORD4
+ case _ => JEditToken.DIGIT
+ }
+ case Bibtex.Token.Kind.SPACE => JEditToken.NULL
+ case Bibtex.Token.Kind.COMMENT => JEditToken.COMMENT1
+ case Bibtex.Token.Kind.ERROR => JEditToken.INVALID
+ }
+
+
+ /* line context */
+
+ private val context_rules = new ParserRuleSet("bibtex", "MAIN")
+
+ private class Line_Context(context: Option[Bibtex.Line_Context])
+ extends Token_Markup.Generic_Line_Context[Bibtex.Line_Context](context_rules, context)
+
+
+ /* token marker */
+
+ class Token_Marker extends TokenMarker
+ {
+ override def markTokens(context: TokenMarker.LineContext,
+ handler: TokenHandler, raw_line: Segment): TokenMarker.LineContext =
+ {
+ val line_ctxt =
+ context match {
+ case c: Line_Context => c.context
+ case _ => Some(Bibtex.Ignored_Context)
+ }
+ val line = if (raw_line == null) new Segment else raw_line
+
+ val context1 =
+ {
+ val (styled_tokens, context1) =
+ line_ctxt match {
+ case Some(ctxt) =>
+ val (chunks, ctxt1) = Bibtex.parse_line(line, ctxt)
+ val styled_tokens =
+ for { chunk <- chunks; tok <- chunk.tokens }
+ yield (token_style(chunk.kind, tok), tok.source)
+ (styled_tokens, new Line_Context(Some(ctxt1)))
+ case None =>
+ val styled_token = (JEditToken.NULL, line.subSequence(0, line.count).toString)
+ (List(styled_token), new Line_Context(None))
+ }
+
+ var offset = 0
+ for ((style, token) <- styled_tokens) {
+ val length = token.length
+ val end_offset = offset + length
+
+ if ((offset until end_offset).exists(i => line.charAt(i) == '\t')) {
+ for (i <- offset until end_offset)
+ handler.handleToken(line, style, i, 1, context1)
+ }
+ else handler.handleToken(line, style, offset, length, context1)
+
+ offset += length
+ }
+ handler.handleToken(line, JEditToken.END, line.count, 0, context1)
+ context1
+ }
+ val context2 = context1.intern
+ handler.setLineContext(context2)
+ context2
+ }
+ }
+
+
+
+ /** Sidekick parser **/
+
+ class Sidekick_Parser extends SideKickParser("bibtex")
+ {
+ override def supportsCompletion = false
+
+ private class Asset(
+ label: String, label_html: String, start: Text.Offset, stop: Text.Offset, source: String)
+ extends Isabelle_Sidekick.Asset(label, start, stop) {
+ override def getShortString: String = label_html
+ override def getLongString: String = source
+ }
+
+ def parse(buffer: Buffer, error_source: errorlist.DefaultErrorSource): SideKickParsedData =
+ {
+ val data = Isabelle_Sidekick.root_data(buffer)
+
+ try {
+ var offset = 0
+ for (chunk <- Bibtex.parse(JEdit_Lib.buffer_text(buffer))) {
+ val kind = chunk.kind
+ val name = chunk.name
+ val source = chunk.source
+ if (kind != "") {
+ val label = kind + (if (name == "") "" else " " + name)
+ val label_html =
+ "" + kind + "" + (if (name == "") "" else " " + name) + ""
+ val asset = new Asset(label, label_html, offset, offset + source.size, source)
+ data.root.add(new DefaultMutableTreeNode(asset))
+ }
+ offset += source.size
+ }
+ data
+ }
+ catch { case ERROR(_) => null }
+ }
+ }
}
diff -r 30b75b7958d6 -r 72e2b2a609c4 src/Tools/jEdit/src/bibtex_token_markup.scala
--- a/src/Tools/jEdit/src/bibtex_token_markup.scala Sun Oct 05 17:58:36 2014 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,102 +0,0 @@
-/* Title: Tools/jEdit/src/bibtex_token_markup.scala
- Author: Makarius
-
-Bibtex token markup.
-*/
-
-package isabelle.jedit
-
-
-import isabelle._
-
-import org.gjt.sp.jedit.syntax.{Token => JEditToken, TokenMarker, TokenHandler, ParserRuleSet}
-
-import javax.swing.text.Segment
-
-
-object Bibtex_Token_Markup
-{
- /* token style */
-
- private def token_style(context: String, token: Bibtex.Token): Byte =
- token.kind match {
- case Bibtex.Token.Kind.COMMAND => JEditToken.KEYWORD2
- case Bibtex.Token.Kind.ENTRY => JEditToken.KEYWORD1
- case Bibtex.Token.Kind.KEYWORD => JEditToken.OPERATOR
- case Bibtex.Token.Kind.NAT => JEditToken.LITERAL2
- case Bibtex.Token.Kind.STRING => JEditToken.LITERAL1
- case Bibtex.Token.Kind.NAME => JEditToken.LABEL
- case Bibtex.Token.Kind.IDENT =>
- if (Bibtex.is_month(token.source)) JEditToken.LITERAL3
- else
- Bibtex.get_entry(context) match {
- case Some(entry) if entry.is_required(token.source) => JEditToken.KEYWORD3
- case Some(entry) if entry.is_optional(token.source) => JEditToken.KEYWORD4
- case _ => JEditToken.DIGIT
- }
- case Bibtex.Token.Kind.SPACE => JEditToken.NULL
- case Bibtex.Token.Kind.COMMENT => JEditToken.COMMENT1
- case Bibtex.Token.Kind.ERROR => JEditToken.INVALID
- }
-
-
- /* line context */
-
- private val context_rules = new ParserRuleSet("bibtex", "MAIN")
-
- private class Line_Context(context: Option[Bibtex.Line_Context])
- extends Token_Markup.Generic_Line_Context[Bibtex.Line_Context](context_rules, context)
-
-
- /* token marker */
-
- class Marker extends TokenMarker
- {
- override def markTokens(context: TokenMarker.LineContext,
- handler: TokenHandler, raw_line: Segment): TokenMarker.LineContext =
- {
- val line_ctxt =
- context match {
- case c: Line_Context => c.context
- case _ => Some(Bibtex.Ignored_Context)
- }
- val line = if (raw_line == null) new Segment else raw_line
-
- val context1 =
- {
- val (styled_tokens, context1) =
- line_ctxt match {
- case Some(ctxt) =>
- val (chunks, ctxt1) = Bibtex.parse_line(line, ctxt)
- val styled_tokens =
- for { chunk <- chunks; tok <- chunk.tokens }
- yield (token_style(chunk.kind, tok), tok.source)
- (styled_tokens, new Line_Context(Some(ctxt1)))
- case None =>
- val styled_token = (JEditToken.NULL, line.subSequence(0, line.count).toString)
- (List(styled_token), new Line_Context(None))
- }
-
- var offset = 0
- for ((style, token) <- styled_tokens) {
- val length = token.length
- val end_offset = offset + length
-
- if ((offset until end_offset).exists(i => line.charAt(i) == '\t')) {
- for (i <- offset until end_offset)
- handler.handleToken(line, style, i, 1, context1)
- }
- else handler.handleToken(line, style, offset, length, context1)
-
- offset += length
- }
- handler.handleToken(line, JEditToken.END, line.count, 0, context1)
- context1
- }
- val context2 = context1.intern
- handler.setLineContext(context2)
- context2
- }
- }
-}
-
diff -r 30b75b7958d6 -r 72e2b2a609c4 src/Tools/jEdit/src/context_menu.scala
--- a/src/Tools/jEdit/src/context_menu.scala Sun Oct 05 17:58:36 2014 +0200
+++ b/src/Tools/jEdit/src/context_menu.scala Sun Oct 05 18:14:26 2014 +0200
@@ -75,7 +75,7 @@
case text_area: TextArea =>
text_area.getBuffer match {
case buffer: Buffer
- if (Isabelle.is_bibtex(buffer) && buffer.isEditable) =>
+ if (Bibtex_JEdit.check(buffer) && buffer.isEditable) =>
val menu = new JMenu("BibTeX entries")
for (entry <- Bibtex.entries) {
val item = new JMenuItem(entry.kind)
diff -r 30b75b7958d6 -r 72e2b2a609c4 src/Tools/jEdit/src/document_model.scala
--- a/src/Tools/jEdit/src/document_model.scala Sun Oct 05 17:58:36 2014 +0200
+++ b/src/Tools/jEdit/src/document_model.scala Sun Oct 05 18:14:26 2014 +0200
@@ -163,7 +163,7 @@
def bibtex_entries(): List[(String, Text.Offset)] =
GUI_Thread.require {
- if (Isabelle.is_bibtex(buffer)) {
+ if (Bibtex_JEdit.check(buffer)) {
_bibtex match {
case Some(entries) => entries
case None =>
diff -r 30b75b7958d6 -r 72e2b2a609c4 src/Tools/jEdit/src/isabelle.scala
--- a/src/Tools/jEdit/src/isabelle.scala Sun Oct 05 17:58:36 2014 +0200
+++ b/src/Tools/jEdit/src/isabelle.scala Sun Oct 05 18:14:26 2014 +0200
@@ -64,17 +64,11 @@
}
- /* buffer types */
-
- def is_bibtex(buffer: Buffer): Boolean =
- JEdit_Lib.buffer_name(buffer).endsWith(".bib")
-
-
/* token markers */
private val markers: Map[String, TokenMarker] =
Map(modes.map(name => (name, new Token_Markup.Marker(name))): _*) +
- ("bibtex" -> new Bibtex_Token_Markup.Marker)
+ ("bibtex" -> new Bibtex_JEdit.Token_Marker)
def token_marker(name: String): Option[TokenMarker] = markers.get(name)
diff -r 30b75b7958d6 -r 72e2b2a609c4 src/Tools/jEdit/src/isabelle_sidekick.scala
--- a/src/Tools/jEdit/src/isabelle_sidekick.scala Sun Oct 05 17:58:36 2014 +0200
+++ b/src/Tools/jEdit/src/isabelle_sidekick.scala Sun Oct 05 18:14:26 2014 +0200
@@ -242,40 +242,3 @@
}
}
-
-class Isabelle_Sidekick_Bibtex extends SideKickParser("bibtex")
-{
- override def supportsCompletion = false
-
- private class Asset(
- label: String, label_html: String, start: Text.Offset, stop: Text.Offset, source: String)
- extends Isabelle_Sidekick.Asset(label, start, stop) {
- override def getShortString: String = label_html
- override def getLongString: String = source
- }
-
- def parse(buffer: Buffer, error_source: errorlist.DefaultErrorSource): SideKickParsedData =
- {
- val data = Isabelle_Sidekick.root_data(buffer)
-
- try {
- var offset = 0
- for (chunk <- Bibtex.parse(JEdit_Lib.buffer_text(buffer))) {
- val kind = chunk.kind
- val name = chunk.name
- val source = chunk.source
- if (kind != "") {
- val label = kind + (if (name == "") "" else " " + name)
- val label_html =
- "" + kind + "" + (if (name == "") "" else " " + name) + ""
- val asset = new Asset(label, label_html, offset, offset + source.size, source)
- data.root.add(new DefaultMutableTreeNode(asset))
- }
- offset += source.size
- }
- data
- }
- catch { case ERROR(_) => null }
- }
-}
-
diff -r 30b75b7958d6 -r 72e2b2a609c4 src/Tools/jEdit/src/services.xml
--- a/src/Tools/jEdit/src/services.xml Sun Oct 05 17:58:36 2014 +0200
+++ b/src/Tools/jEdit/src/services.xml Sun Oct 05 18:14:26 2014 +0200
@@ -27,7 +27,7 @@
new isabelle.jedit.Isabelle_Sidekick_Root();
- new isabelle.jedit.Isabelle_Sidekick_Bibtex();
+ new isabelle.jedit.Bibtex_JEdit.Sidekick_Parser();
new isabelle.jedit.Scala_Console();