# HG changeset patch # User wenzelm # Date 1412340386 -7200 # Node ID f05ccce3eca2b95b98bbb763afb5f4e365401d28 # Parent f008ceb3b0464f409b3fdd315655a8b0ba9c8468 SideKick parser for bibtex entries; tuned signature; diff -r f008ceb3b046 -r f05ccce3eca2 NEWS --- 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 *** diff -r f008ceb3b046 -r f05ccce3eca2 src/Pure/Tools/bibtex.scala --- 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) } } } diff -r f008ceb3b046 -r f05ccce3eca2 src/Tools/jEdit/src/Isabelle.props --- 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 diff -r f008ceb3b046 -r f05ccce3eca2 src/Tools/jEdit/src/context_menu.scala --- 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) diff -r f008ceb3b046 -r f05ccce3eca2 src/Tools/jEdit/src/isabelle_sidekick.scala --- 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("")); true } + if (stopped) { data.root.add(new DefaultMutableTreeNode("")); true } else ok } else false - if (!ok) root.add(new DefaultMutableTreeNode("")) + if (!ok) data.root.add(new DefaultMutableTreeNode("")) 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 } + } +} + diff -r f008ceb3b046 -r f05ccce3eca2 src/Tools/jEdit/src/services.xml --- 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 @@ new isabelle.jedit.Isabelle_Sidekick_Root(); + + new isabelle.jedit.Isabelle_Sidekick_Bibtex(); + new isabelle.jedit.Scala_Console();