--- a/NEWS Fri Oct 03 11:16:28 2014 +0200
+++ b/NEWS Fri Oct 03 14:46:26 2014 +0200
@@ -17,7 +17,7 @@
*** Prover IDE -- Isabelle/Scala/jEdit ***
-* Support for BibTeX files: context menu.
+* Support for BibTeX files: SideKick parser, context menu.
*** Pure ***
--- a/src/Pure/Tools/bibtex.scala Fri Oct 03 11:16:28 2014 +0200
+++ b/src/Pure/Tools/bibtex.scala Fri Oct 03 14:46:26 2014 +0200
@@ -32,14 +32,14 @@
val commands = List("preamble", "string")
sealed case class Entry(
- name: String,
+ kind: String,
required: List[String],
optional_crossref: List[String],
optional: List[String])
{
def fields: List[String] = required ::: optional_crossref ::: optional
def template: String =
- "@" + name + "{,\n" + fields.map(x => " " + x + " = {},\n").mkString + "}\n"
+ "@" + kind + "{,\n" + fields.map(x => " " + x + " = {},\n").mkString + "}\n"
}
val entries: List[Entry] =
@@ -123,26 +123,36 @@
def is_error: Boolean = kind == Token.Kind.ERROR
}
- abstract class Chunk
- case class Ignored(source: String) extends Chunk
- case class Malformed(source: String) extends Chunk
+ abstract class Chunk { def size: Int; def kind: String = "" }
+ case class Ignored(source: String) extends Chunk { def size: Int = source.size }
+ case class Malformed(source: String) extends Chunk { def size: Int = source.size }
case class Item(tokens: List[Token]) extends Chunk
{
- val name: String =
+ def size: Int = (0 /: tokens)({ case (n, token) => n + token.source.size })
+
+ private val content: (String, List[Token]) =
tokens match {
case Token(Token.Kind.KEYWORD, "@") :: body
if !body.isEmpty && !body.exists(_.is_error) =>
- (body.filterNot(_.is_space), body.last) match {
- case (Token(Token.Kind.IDENT, id) :: Token(Token.Kind.KEYWORD, "{") :: _,
- Token(Token.Kind.KEYWORD, "}")) => id
- case (Token(Token.Kind.IDENT, id) :: Token(Token.Kind.KEYWORD, "(") :: _,
- Token(Token.Kind.KEYWORD, ")")) => id
- case _ => ""
+ (body.init.filterNot(_.is_space), body.last) match {
+ case (Token(Token.Kind.IDENT, id) :: Token(Token.Kind.KEYWORD, "{") :: toks,
+ Token(Token.Kind.KEYWORD, "}")) => (id, toks)
+ case (Token(Token.Kind.IDENT, id) :: Token(Token.Kind.KEYWORD, "(") :: toks,
+ Token(Token.Kind.KEYWORD, ")")) => (id, toks)
+ case _ => ("", Nil)
}
+ case _ => ("", Nil)
+ }
+ override def kind: String = content._1
+ def content_tokens: List[Token] = content._2
+
+ def is_wellformed: Boolean = kind != ""
+
+ def name: String =
+ content_tokens match {
+ case Token(Token.Kind.IDENT, name) :: _ if is_wellformed => name
case _ => ""
}
- val entry_name: String = if (commands.contains(name.toLowerCase)) "" else name
- def is_wellformed: Boolean = name != ""
}
@@ -262,7 +272,7 @@
val in: Reader[Char] = new CharSequenceReader(input)
Parsers.parseAll(Parsers.chunks, in) match {
case Parsers.Success(result, _) => result
- case _ => error("Unexpected failure of tokenizing input:\n" + input.toString)
+ case _ => error("Unexpected failure to parse input:\n" + input.toString)
}
}
}
--- a/src/Tools/jEdit/src/Isabelle.props Fri Oct 03 11:16:28 2014 +0200
+++ b/src/Tools/jEdit/src/Isabelle.props Fri Oct 03 14:46:26 2014 +0200
@@ -84,4 +84,6 @@
mode.isabelle.sidekick.showStatusWindow.label=true
mode.ml.sidekick.parser=isabelle
sidekick.parser.isabelle.label=Isabelle
+mode.bibtex.sidekick.parser=bibtex
+mode.bibtex.folding=sidekick
--- a/src/Tools/jEdit/src/context_menu.scala Fri Oct 03 11:16:28 2014 +0200
+++ b/src/Tools/jEdit/src/context_menu.scala Fri Oct 03 14:46:26 2014 +0200
@@ -78,7 +78,7 @@
if (JEdit_Lib.buffer_name(buffer).endsWith(".bib") && buffer.isEditable) =>
val menu = new JMenu("BibTeX entries")
for (entry <- Bibtex.entries) {
- val item = new JMenuItem(entry.name)
+ val item = new JMenuItem(entry.kind)
item.addActionListener(new ActionListener {
def actionPerformed(evt: ActionEvent): Unit =
Isabelle.insert_line_padding(text_area, entry.template)
--- a/src/Tools/jEdit/src/isabelle_sidekick.scala Fri Oct 03 11:16:28 2014 +0200
+++ b/src/Tools/jEdit/src/isabelle_sidekick.scala Fri Oct 03 14:46:26 2014 +0200
@@ -23,6 +23,13 @@
def int_to_pos(offset: Text.Offset): Position =
new Position { def getOffset = offset; override def toString: String = offset.toString }
+ def root_data(buffer: Buffer): SideKickParsedData =
+ {
+ val data = new SideKickParsedData(buffer.getName)
+ data.getAsset(data.root).setEnd(int_to_pos(buffer.getLength))
+ data
+ }
+
class Asset(name: String, start: Text.Offset, end: Text.Offset) extends IAsset
{
protected var _name = name
@@ -71,19 +78,16 @@
stopped = false
// FIXME lock buffer (!??)
- val data = new SideKickParsedData(buffer.getName)
- val root = data.root
- data.getAsset(root).setEnd(Isabelle_Sidekick.int_to_pos(buffer.getLength))
-
+ val data = Isabelle_Sidekick.root_data(buffer)
val syntax = Isabelle.mode_syntax(name)
val ok =
if (syntax.isDefined) {
val ok = parser(buffer, syntax.get, data)
- if (stopped) { root.add(new DefaultMutableTreeNode("<stopped>")); true }
+ if (stopped) { data.root.add(new DefaultMutableTreeNode("<stopped>")); true }
else ok
}
else false
- if (!ok) root.add(new DefaultMutableTreeNode("<ignored>"))
+ if (!ok) data.root.add(new DefaultMutableTreeNode("<ignored>"))
data
}
@@ -155,13 +159,13 @@
}
opt_snapshot match {
case Some(snapshot) =>
- val root = data.root
for ((command, command_start) <- snapshot.node.command_iterator() if !stopped) {
val markup =
snapshot.state.command_markup(
snapshot.version, command, Command.Markup_Index.markup,
command.range, Markup.Elements.full)
- Isabelle_Sidekick.swing_markup_tree(markup, root, (info: Text.Info[List[XML.Elem]]) =>
+ Isabelle_Sidekick.swing_markup_tree(markup, data.root,
+ (info: Text.Info[List[XML.Elem]]) =>
{
val range = info.range + command_start
val content = command.source(info.range).replace('\n', ' ')
@@ -212,3 +216,34 @@
}
}
+
+class Isabelle_Sidekick_Bibtex extends SideKickParser("bibtex")
+{
+ override def supportsCompletion = false
+
+ private class Asset(label: String, start: Text.Offset, stop: Text.Offset) extends
+ Isabelle_Sidekick.Asset(label, start, stop) { override def getShortString: String = _name }
+
+ 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 n = chunk.size
+ chunk match {
+ case item: Bibtex.Item if item.is_wellformed =>
+ val label = if (item.name == "") item.kind else item.kind + " " + item.name
+ val asset = new Isabelle_Sidekick.Asset(label, offset, offset + n)
+ data.root.add(new DefaultMutableTreeNode(asset))
+ case _ =>
+ }
+ offset += n
+ }
+ data
+ }
+ catch { case ERROR(_) => null }
+ }
+}
+
--- a/src/Tools/jEdit/src/services.xml Fri Oct 03 11:16:28 2014 +0200
+++ b/src/Tools/jEdit/src/services.xml Fri Oct 03 14:46:26 2014 +0200
@@ -26,6 +26,9 @@
<SERVICE NAME="isabelle-root" CLASS="sidekick.SideKickParser">
new isabelle.jedit.Isabelle_Sidekick_Root();
</SERVICE>
+ <SERVICE NAME="bibtex" CLASS="sidekick.SideKickParser">
+ new isabelle.jedit.Isabelle_Sidekick_Bibtex();
+ </SERVICE>
<SERVICE CLASS="console.Shell" NAME="Scala">
new isabelle.jedit.Scala_Console();
</SERVICE>