# HG changeset patch # User wenzelm # Date 1412453731 -7200 # Node ID 48e23e34241517106c05736794ec6dbad12391c9 # Parent 872f330a0f8a0b8bcf5e867ceac68c066a2556f3# Parent ad010811f45053ea333b33fe58e9992058e3df16 merged; diff -r ad010811f450 -r 48e23e342415 NEWS --- a/NEWS Fri Oct 03 11:55:07 2014 +0200 +++ b/NEWS Sat Oct 04 22:15:31 2014 +0200 @@ -15,6 +15,12 @@ semantics due to external visual order vs. internal reverse order. +*** Prover IDE -- Isabelle/Scala/jEdit *** + +* Support for BibTeX files: context menu, context-sensitive token +marker, SideKick parser. + + *** Pure *** * Command "class_deps" takes optional sort arguments constraining diff -r ad010811f450 -r 48e23e342415 src/Pure/Tools/bibtex.scala --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Pure/Tools/bibtex.scala Sat Oct 04 22:15:31 2014 +0200 @@ -0,0 +1,385 @@ +/* Title: Pure/Tools/bibtex.scala + Author: Makarius + +Some support for bibtex files. +*/ + +package isabelle + + +import scala.collection.mutable +import scala.util.parsing.input.{Reader, CharSequenceReader} +import scala.util.parsing.combinator.RegexParsers + + +object Bibtex +{ + /** content **/ + + private val months = List( + "jan", + "feb", + "mar", + "apr", + "may", + "jun", + "jul", + "aug", + "sep", + "oct", + "nov", + "dec") + def is_month(s: String): Boolean = months.contains(s.toLowerCase) + + private val commands = List("preamble", "string") + def is_command(s: String): Boolean = commands.contains(s.toLowerCase) + + sealed case class Entry( + kind: String, + required: List[String], + optional_crossref: List[String], + optional_other: List[String]) + { + def is_required(s: String): Boolean = required.contains(s.toLowerCase) + def is_optional(s: String): Boolean = + optional_crossref.contains(s.toLowerCase) || optional_other.contains(s.toLowerCase) + + def fields: List[String] = required ::: optional_crossref ::: optional_other + def template: String = + "@" + kind + "{,\n" + fields.map(x => " " + x + " = {},\n").mkString + "}\n" + } + + val entries: List[Entry] = + List( + Entry("Article", + List("author", "title"), + List("journal", "year"), + List("volume", "number", "pages", "month", "note")), + Entry("InProceedings", + List("author", "title"), + List("booktitle", "year"), + List("editor", "volume", "number", "series", "pages", "month", "address", + "organization", "publisher", "note")), + Entry("InCollection", + List("author", "title", "booktitle"), + List("publisher", "year"), + List("editor", "volume", "number", "series", "type", "chapter", "pages", + "edition", "month", "address", "note")), + Entry("InBook", + List("author", "editor", "title", "chapter"), + List("publisher", "year"), + List("volume", "number", "series", "type", "address", "edition", "month", "pages", "note")), + Entry("Proceedings", + List("title", "year"), + List(), + List("booktitle", "editor", "volume", "number", "series", "address", "month", + "organization", "publisher", "note")), + Entry("Book", + List("author", "editor", "title"), + List("publisher", "year"), + List("volume", "number", "series", "address", "edition", "month", "note")), + Entry("Booklet", + List("title"), + List(), + List("author", "howpublished", "address", "month", "year", "note")), + Entry("PhdThesis", + List("author", "title", "school", "year"), + List(), + List("type", "address", "month", "note")), + Entry("MastersThesis", + List("author", "title", "school", "year"), + List(), + List("type", "address", "month", "note")), + Entry("TechReport", + List("author", "title", "institution", "year"), + List(), + List("type", "number", "address", "month", "note")), + Entry("Manual", + List("title"), + List(), + List("author", "organization", "address", "edition", "month", "year", "note")), + Entry("Unpublished", + List("author", "title", "note"), + List(), + List("month", "year")), + Entry("Misc", + List(), + List(), + List("author", "title", "howpublished", "month", "year", "note"))) + + def get_entry(kind: String): Option[Entry] = + entries.find(entry => entry.kind.toLowerCase == kind.toLowerCase) + + def is_entry(kind: String): Boolean = get_entry(kind).isDefined + + + + /** tokens and chunks **/ + + object Token + { + object Kind extends Enumeration + { + val COMMAND = Value("command") + val ENTRY = Value("entry") + val KEYWORD = Value("keyword") + val NAT = Value("natural number") + val STRING = Value("string") + val NAME = Value("name") + val IDENT = Value("identifier") + val SPACE = Value("white space") + val COMMENT = Value("ignored text") + val ERROR = Value("bad input") + } + } + + sealed case class Token(kind: Token.Kind.Value, val source: String) + { + def is_kind: Boolean = + kind == Token.Kind.COMMAND || + kind == Token.Kind.ENTRY || + kind == Token.Kind.IDENT + def is_name: Boolean = + kind == Token.Kind.NAME || + kind == Token.Kind.IDENT + def is_ignored: Boolean = + kind == Token.Kind.SPACE || + kind == Token.Kind.COMMENT + def is_malformed: Boolean = kind == + Token.Kind.ERROR + } + + case class Chunk(kind: String, tokens: List[Token]) + { + val source = tokens.map(_.source).mkString + + private val content: Option[List[Token]] = + tokens match { + case Token(Token.Kind.KEYWORD, "@") :: body if !body.isEmpty => + (body.init.filterNot(_.is_ignored), body.last) match { + case (tok :: Token(Token.Kind.KEYWORD, "{") :: toks, Token(Token.Kind.KEYWORD, "}")) + if tok.is_kind => Some(toks) + + case (tok :: Token(Token.Kind.KEYWORD, "(") :: toks, Token(Token.Kind.KEYWORD, ")")) + if tok.is_kind => Some(toks) + + case _ => None + } + case _ => None + } + + def name: String = + content match { + case Some(tok :: _) if tok.is_name => tok.source + case _ => "" + } + + def is_ignored: Boolean = kind == "" && tokens.forall(_.is_ignored) + def is_malformed: Boolean = kind == "" || tokens.exists(_.is_malformed) + def is_command: Boolean = + Bibtex.is_command(kind) && name != "" && content.isDefined && !is_malformed + def is_entry: Boolean = + Bibtex.is_entry(kind) && name != "" && content.isDefined && !is_malformed + } + + + + /** parsing **/ + + // context of partial line-oriented scans + abstract class Line_Context + case object Ignored_Context extends Line_Context + case class Item_Context(kind: String, delim: Delimited, right: String) extends Line_Context + case class Delimited(quoted: Boolean, depth: Int) + val Closed = Delimited(false, 0) + + private def token(kind: Token.Kind.Value)(source: String): Token = Token(kind, source) + private def keyword(source: String): Token = Token(Token.Kind.KEYWORD, source) + + + // See also http://ctan.org/tex-archive/biblio/bibtex/base/bibtex.web + // module @. + + object Parsers extends RegexParsers + { + /* white space and comments */ + + override val whiteSpace = "".r + + private val space = """[ \t\n\r]+""".r ^^ token(Token.Kind.SPACE) + private val strict_space = """[ \t]+""".r ^^ token(Token.Kind.SPACE) + + + /* ignored text */ + + private val ignored: Parser[Chunk] = + rep1("""(?mi)([^@]+|@[ \t]*comment)""".r) ^^ { + case ss => Chunk("", List(Token(Token.Kind.COMMENT, ss.mkString))) } + + private def ignored_line: Parser[(Chunk, Line_Context)] = + ignored ^^ { case a => (a, Ignored_Context) } + + + /* delimited string: outermost "..." or {...} and body with balanced {...} */ + + // see also bibtex.web: scan_a_field_token_and_eat_white, scan_balanced_braces + private def delimited_depth(delim: Delimited): Parser[(String, Delimited)] = + new Parser[(String, Delimited)] + { + require(if (delim.quoted) delim.depth > 0 else delim.depth >= 0) + + def apply(in: Input) = + { + val start = in.offset + val end = in.source.length + + var i = start + var q = delim.quoted + var d = delim.depth + var finished = false + while (!finished && i < end) { + val c = in.source.charAt(i) + + if (c == '"' && d == 0) { i += 1; d = 1; q = true } + else if (c == '"' && d == 1 && q) { + i += 1; d = 0; q = false; finished = true + } + else if (c == '{') { i += 1; d += 1 } + else if (c == '}') { + if (d == 1 && !q || d > 1) { i += 1; d -= 1; if (d == 0) finished = true } + else {i = start; finished = true } + } + else if (d > 0) i += 1 + else finished = true + } + if (i == start) Failure("bad input", in) + else { + val s = in.source.subSequence(start, i).toString + Success((s, Delimited(q, d)), in.drop(i - start)) + } + } + }.named("delimited_depth") + + private def delimited: Parser[Token] = + delimited_depth(Closed) ^? + { case (s, delim) if delim == Closed => Token(Token.Kind.STRING, s) } + + private def recover_delimited: Parser[Token] = + """(?m)["{][^@]*""".r ^^ token(Token.Kind.ERROR) + + def delimited_line(item_ctxt: Item_Context): Parser[(Chunk, Line_Context)] = + item_ctxt match { + case Item_Context(kind, delim, _) => + delimited_depth(delim) ^^ { case (s, delim1) => + (Chunk(kind, List(Token(Token.Kind.STRING, s))), item_ctxt.copy(delim = delim1)) } | + recover_delimited ^^ { case a => (Chunk(kind, List(a)), Ignored_Context) } + } + + + /* other tokens */ + + private val at = "@" ^^ keyword + private val left_brace = "{" ^^ keyword + private val right_brace = "}" ^^ keyword + private val left_paren = "(" ^^ keyword + private val right_paren = ")" ^^ keyword + + private val nat = "[0-9]+".r ^^ token(Token.Kind.NAT) + + private val identifier = + """[\x21-\x7f&&[^"#%'(),={}0-9]][\x21-\x7f&&[^"#%'(),={}]]*""".r + + private val ident = identifier ^^ token(Token.Kind.IDENT) + + val other_token = "[=#,]".r ^^ keyword | (nat | (ident | space)) + + + /* items: command or entry */ + + private val item_kind = + identifier ^^ { case a => + val kind = + if (is_command(a)) Token.Kind.COMMAND + else if (is_entry(a)) Token.Kind.ENTRY + else Token.Kind.IDENT + Token(kind, a) + } + + private val item_start = + at ~ rep(strict_space) ~ item_kind ~ rep(strict_space) ^^ + { case a ~ b ~ c ~ d => (c.source, List(a) ::: b ::: List(c) ::: d) } + + private val item_name = + rep(strict_space) ~ identifier ^^ + { case a ~ b => a ::: List(Token(Token.Kind.NAME, b)) } + + private val item_body = + delimited | (recover_delimited | other_token) + + private val item: Parser[Chunk] = + (item_start ~ left_brace ~ item_name ~ rep(item_body) ~ opt(right_brace) | + item_start ~ left_paren ~ item_name ~ rep(item_body) ~ opt(right_paren)) ^^ + { case (kind, a) ~ b ~ c ~ d ~ e => Chunk(kind, a ::: List(b) ::: c ::: d ::: e.toList) } + + private val recover_item: Parser[Chunk] = + at ~ "(?m)[^@]*".r ^^ { case a ~ b => Chunk("", List(a, Token(Token.Kind.ERROR, b))) } + + + /* chunks */ + + val chunk: Parser[Chunk] = ignored | (item | recover_item) + + def chunk_line(ctxt: Line_Context): Parser[(Chunk, Line_Context)] = + { + ctxt match { + case Ignored_Context => + ignored_line | + item_start ~ (left_brace | left_paren) ~ opt(item_name) ^^ + { case (kind, a) ~ b ~ c => + val right = if (b.source == "{") "}" else ")" + val chunk = Chunk(kind, a ::: List(b) ::: (c getOrElse Nil)) + (chunk, Item_Context(kind, Closed, right)) } | + recover_item ^^ { case a => (a, Ignored_Context) } + case item_ctxt @ Item_Context(kind, delim, right) => + if (delim.depth > 0) + delimited_line(item_ctxt) | + ignored_line + else { + delimited_line(item_ctxt) | + other_token ^^ { case a => (Chunk(kind, List(a)), ctxt) } | + right ^^ { case a => (Chunk(kind, List(keyword(a))), Ignored_Context) } | + ignored_line + } + case _ => failure("") + } + } + } + + + /* parse */ + + def parse(input: CharSequence): List[Chunk] = + { + val in: Reader[Char] = new CharSequenceReader(input) + Parsers.parseAll(Parsers.rep(Parsers.chunk), in) match { + case Parsers.Success(result, _) => result + case _ => error("Unexpected failure to parse input:\n" + input.toString) + } + } + + def parse_line(input: CharSequence, context: Line_Context): (List[Chunk], Line_Context) = + { + var in: Reader[Char] = new CharSequenceReader(input) + val chunks = new mutable.ListBuffer[Chunk] + var ctxt = context + while (!in.atEnd) { + Parsers.parse(Parsers.chunk_line(ctxt), in) match { + case Parsers.Success((x, c), rest) => { chunks += x; ctxt = c; in = rest } + case Parsers.NoSuccess(_, rest) => + error("Unepected failure to parse input:\n" + rest.source.toString) + } + } + (chunks.toList, ctxt) + } +} + diff -r ad010811f450 -r 48e23e342415 src/Pure/build-jars --- a/src/Pure/build-jars Fri Oct 03 11:55:07 2014 +0200 +++ b/src/Pure/build-jars Sat Oct 04 22:15:31 2014 +0200 @@ -85,6 +85,7 @@ Thy/thy_info.scala Thy/thy_structure.scala Thy/thy_syntax.scala + Tools/bibtex.scala Tools/build.scala Tools/build_console.scala Tools/build_doc.scala diff -r ad010811f450 -r 48e23e342415 src/Tools/jEdit/lib/Tools/jedit --- a/src/Tools/jEdit/lib/Tools/jedit Fri Oct 03 11:55:07 2014 +0200 +++ b/src/Tools/jEdit/lib/Tools/jedit Sat Oct 04 22:15:31 2014 +0200 @@ -9,6 +9,7 @@ declare -a SOURCES=( "src/active.scala" + "src/bibtex_token_markup.scala" "src/completion_popup.scala" "src/context_menu.scala" "src/dockable.scala" @@ -41,9 +42,9 @@ "src/rendering.scala" "src/rich_text_area.scala" "src/scala_console.scala" - "src/sledgehammer_dockable.scala" "src/simplifier_trace_dockable.scala" "src/simplifier_trace_window.scala" + "src/sledgehammer_dockable.scala" "src/spell_checker.scala" "src/symbols_dockable.scala" "src/syslog_dockable.scala" diff -r ad010811f450 -r 48e23e342415 src/Tools/jEdit/src/Isabelle.props --- a/src/Tools/jEdit/src/Isabelle.props Fri Oct 03 11:55:07 2014 +0200 +++ b/src/Tools/jEdit/src/Isabelle.props Sat Oct 04 22:15:31 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 ad010811f450 -r 48e23e342415 src/Tools/jEdit/src/active.scala --- a/src/Tools/jEdit/src/active.scala Fri Oct 03 11:55:07 2014 +0200 +++ b/src/Tools/jEdit/src/active.scala Sat Oct 04 22:15:31 2014 +0200 @@ -60,16 +60,18 @@ } case XML.Elem(Markup(Markup.SENDBACK, props), _) => - props match { - case Position.Id(id) => - Isabelle.edit_command(snapshot, buffer, - props.exists(_ == Markup.PADDING_COMMAND), id, text) - case _ => - if (props.exists(_ == Markup.PADDING_LINE)) - Isabelle.insert_line_padding(text_area, text) - else text_area.setSelectedText(text) + if (buffer.isEditable) { + props match { + case Position.Id(id) => + Isabelle.edit_command(snapshot, buffer, + props.exists(_ == Markup.PADDING_COMMAND), id, text) + case _ => + if (props.exists(_ == Markup.PADDING_LINE)) + Isabelle.insert_line_padding(text_area, text) + else text_area.setSelectedText(text) + } + text_area.requestFocus } - text_area.requestFocus case Protocol.Dialog(id, serial, result) => model.session.dialog_result(id, serial, result) diff -r ad010811f450 -r 48e23e342415 src/Tools/jEdit/src/bibtex_token_markup.scala --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Tools/jEdit/src/bibtex_token_markup.scala Sat Oct 04 22:15:31 2014 +0200 @@ -0,0 +1,102 @@ +/* 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 ad010811f450 -r 48e23e342415 src/Tools/jEdit/src/context_menu.scala --- a/src/Tools/jEdit/src/context_menu.scala Fri Oct 03 11:55:07 2014 +0200 +++ b/src/Tools/jEdit/src/context_menu.scala Sat Oct 04 22:15:31 2014 +0200 @@ -10,13 +10,13 @@ import isabelle._ -import java.awt.event.MouseEvent -import javax.swing.JMenuItem +import java.awt.event.{ActionListener, ActionEvent, MouseEvent} +import javax.swing.{JMenu, JMenuItem} import org.gjt.sp.jedit.menu.EnhancedMenuItem import org.gjt.sp.jedit.gui.DynamicContextMenuService -import org.gjt.sp.jedit.jEdit -import org.gjt.sp.jedit.textarea.JEditTextArea +import org.gjt.sp.jedit.{jEdit, Buffer} +import org.gjt.sp.jedit.textarea.{JEditTextArea, TextArea} class Context_Menu extends DynamicContextMenuService @@ -67,20 +67,50 @@ } + /* bibtex menu */ + + def bibtex_menu(text_area0: JEditTextArea): List[JMenuItem] = + { + text_area0 match { + case text_area: TextArea => + text_area.getBuffer match { + case buffer: Buffer + 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.kind) + item.addActionListener(new ActionListener { + def actionPerformed(evt: ActionEvent): Unit = + Isabelle.insert_line_padding(text_area, entry.template) + }) + menu.add(item) + } + List(menu) + case _ => Nil + } + case _ => Nil + } + } + + /* menu service */ def createMenu(text_area: JEditTextArea, evt: MouseEvent): Array[JMenuItem] = { PIDE.dismissed_popups(text_area.getView) - if (evt != null && evt.getSource == text_area.getPainter) { - val offset = text_area.xyToOffset(evt.getX, evt.getY) - if (offset >= 0) { - val items = spell_checker_menu(text_area, offset) - if (items.isEmpty) null else items.toArray + + val items1 = + if (evt != null && evt.getSource == text_area.getPainter) { + val offset = text_area.xyToOffset(evt.getX, evt.getY) + if (offset >= 0) spell_checker_menu(text_area, offset) + else Nil } - else null - } - else null + else Nil + + val items2 = bibtex_menu(text_area) + + val items = items1 ::: items2 + if (items.isEmpty) null else items.toArray } } diff -r ad010811f450 -r 48e23e342415 src/Tools/jEdit/src/isabelle.scala --- a/src/Tools/jEdit/src/isabelle.scala Fri Oct 03 11:55:07 2014 +0200 +++ b/src/Tools/jEdit/src/isabelle.scala Sat Oct 04 22:15:31 2014 +0200 @@ -16,6 +16,7 @@ import org.gjt.sp.jedit.{jEdit, View, Buffer} import org.gjt.sp.jedit.textarea.JEditTextArea +import org.gjt.sp.jedit.syntax.TokenMarker import org.gjt.sp.jedit.gui.{DockableWindowManager, CompleteWord} import org.gjt.sp.jedit.options.PluginOptions @@ -65,10 +66,11 @@ /* token markers */ - private val markers = - Map(modes.map(name => (name, new Token_Markup.Marker(name))): _*) + private val markers: Map[String, TokenMarker] = + Map(modes.map(name => (name, new Token_Markup.Marker(name))): _*) + + ("bibtex" -> new Bibtex_Token_Markup.Marker) - def token_marker(name: String): Option[Token_Markup.Marker] = markers.get(name) + def token_marker(name: String): Option[TokenMarker] = markers.get(name) /* dockable windows */ diff -r ad010811f450 -r 48e23e342415 src/Tools/jEdit/src/isabelle_sidekick.scala --- a/src/Tools/jEdit/src/isabelle_sidekick.scala Fri Oct 03 11:55:07 2014 +0200 +++ b/src/Tools/jEdit/src/isabelle_sidekick.scala Sat Oct 04 22:15:31 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,40 @@ } } + +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 ad010811f450 -r 48e23e342415 src/Tools/jEdit/src/services.xml --- a/src/Tools/jEdit/src/services.xml Fri Oct 03 11:55:07 2014 +0200 +++ b/src/Tools/jEdit/src/services.xml Sat Oct 04 22:15:31 2014 +0200 @@ -26,6 +26,9 @@ new isabelle.jedit.Isabelle_Sidekick_Root(); + + new isabelle.jedit.Isabelle_Sidekick_Bibtex(); + new isabelle.jedit.Scala_Console(); diff -r ad010811f450 -r 48e23e342415 src/Tools/jEdit/src/token_markup.scala --- a/src/Tools/jEdit/src/token_markup.scala Fri Oct 03 11:55:07 2014 +0200 +++ b/src/Tools/jEdit/src/token_markup.scala Sat Oct 04 22:15:31 2014 +0200 @@ -15,8 +15,8 @@ import org.gjt.sp.util.SyntaxUtilities import org.gjt.sp.jedit.{jEdit, Mode} -import org.gjt.sp.jedit.syntax.{Token => JEditToken, TokenMarker, TokenHandler, - ParserRuleSet, ModeProvider, XModeHandler, SyntaxStyle} +import org.gjt.sp.jedit.syntax.{Token => JEditToken, TokenMarker, TokenHandler, ParserRuleSet, + ModeProvider, XModeHandler, SyntaxStyle} import org.gjt.sp.jedit.textarea.{TextArea, Selection} import org.gjt.sp.jedit.buffer.JEditBuffer @@ -173,12 +173,10 @@ } - /* token marker */ + /* line context */ - private val isabelle_rules = new ParserRuleSet("isabelle", "MAIN") - - private class Line_Context(val context: Option[Scan.Line_Context]) - extends TokenMarker.LineContext(isabelle_rules, null) + class Generic_Line_Context[C](rules: ParserRuleSet, val context: Option[C]) + extends TokenMarker.LineContext(rules, null) { override def hashCode: Int = context.hashCode override def equals(that: Any): Boolean = @@ -188,6 +186,14 @@ } } + private val context_rules = new ParserRuleSet("isabelle", "MAIN") + + private class Line_Context(context: Option[Scan.Line_Context]) + extends Generic_Line_Context[Scan.Line_Context](context_rules, context) + + + /* token marker */ + class Marker(mode: String) extends TokenMarker { override def markTokens(context: TokenMarker.LineContext, @@ -202,11 +208,19 @@ val context1 = { + def no_context = + { + val styled_token = (JEditToken.NULL, line.subSequence(0, line.count).toString) + (List(styled_token), new Line_Context(None)) + } val (styled_tokens, context1) = if (mode == "isabelle-ml" || mode == "sml") { - val (tokens, ctxt1) = ML_Lex.tokenize_line(mode == "sml", line, line_ctxt.get) - val styled_tokens = tokens.map(tok => (Rendering.ml_token_markup(tok), tok.source)) - (styled_tokens, new Line_Context(Some(ctxt1))) + if (line_ctxt.isDefined) { + val (tokens, ctxt1) = ML_Lex.tokenize_line(mode == "sml", line, line_ctxt.get) + val styled_tokens = tokens.map(tok => (Rendering.ml_token_markup(tok), tok.source)) + (styled_tokens, new Line_Context(Some(ctxt1))) + } + else no_context } else { Isabelle.mode_syntax(mode) match { @@ -215,9 +229,7 @@ val styled_tokens = tokens.map(tok => (Rendering.token_markup(syntax, tok), tok.source)) (styled_tokens, new Line_Context(Some(ctxt1))) - case _ => - val styled_token = (JEditToken.NULL, line.subSequence(0, line.count).toString) - (List(styled_token), new Line_Context(None)) + case _ => no_context } }