# HG changeset patch # User wenzelm # Date 1412417966 -7200 # Node ID cd4439d8799c04227b5842fab9ffd2550e47f313 # Parent 7d6b8f8893e865b6217c116661a0a4fd837955bf support for bibtex token markup; more robust ML token marker: no_context; tuned signature; diff -r 7d6b8f8893e8 -r cd4439d8799c src/Pure/Tools/bibtex.scala --- a/src/Pure/Tools/bibtex.scala Fri Oct 03 23:33:47 2014 +0200 +++ b/src/Pure/Tools/bibtex.scala Sat Oct 04 12:19:26 2014 +0200 @@ -16,7 +16,7 @@ { /** content **/ - val months = List( + private val months = List( "jan", "feb", "mar", @@ -29,16 +29,22 @@ "oct", "nov", "dec") + def is_month(s: String): Boolean = months.contains(s.toLowerCase) - val commands = List("preamble", "string") + 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: List[String]) + optional_other: List[String]) { - def fields: List[String] = required ::: optional_crossref ::: optional + def is_required(s: String): Boolean = required.contains(s) + def is_optional(s: String): Boolean = + optional_crossref.contains(s) || optional_other.contains(s) + + def fields: List[String] = required ::: optional_crossref ::: optional_other def template: String = "@" + kind + "{,\n" + fields.map(x => " " + x + " = {},\n").mkString + "}\n" } @@ -101,6 +107,9 @@ List(), List("author", "title", "howpublished", "month", "year", "note"))) + def get_entry(kind: String): Option[Entry] = + entries.find(entry => entry.kind.toLowerCase == kind.toLowerCase) + /** tokens and chunks **/ @@ -109,42 +118,45 @@ { 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 IDENT = Value("identifier") - val STRING = Value("string") - val SPACE = Value("white space") + val IGNORED = Value("ignored") val ERROR = Value("bad input") } } sealed case class Token(kind: Token.Kind.Value, val source: String) { - def is_space: Boolean = kind == Token.Kind.SPACE + def is_ignored: Boolean = kind == Token.Kind.IGNORED def is_error: Boolean = kind == Token.Kind.ERROR } abstract class Chunk { - def size: Int def kind: String + def tokens: List[Token] + def source: String } case class Ignored(source: String) extends Chunk { - def size: Int = source.size def kind: String = "" + val tokens = List(Token(Token.Kind.IGNORED, source)) } case class Item(kind: String, tokens: List[Token]) extends Chunk { - def size: Int = (0 /: tokens)({ case (n, token) => n + token.source.size }) + val source = tokens.map(_.source).mkString private val wellformed_content: Option[List[Token]] = tokens match { case Token(Token.Kind.KEYWORD, "@") :: body if !body.isEmpty && !body.exists(_.is_error) => - (body.init.filterNot(_.is_space), body.last) match { + (body.init.filterNot(_.is_ignored), body.last) match { case (Token(Token.Kind.IDENT, _) :: Token(Token.Kind.KEYWORD, "{") :: toks, Token(Token.Kind.KEYWORD, "}")) => Some(toks) case (Token(Token.Kind.IDENT, _) :: Token(Token.Kind.KEYWORD, "(") :: toks, @@ -187,8 +199,8 @@ 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) + private val space = """[ \t\n\r]+""".r ^^ token(Token.Kind.IGNORED) + private val strict_space = """[ \t]+""".r ^^ token(Token.Kind.IGNORED) /* ignored material outside items */ @@ -264,16 +276,27 @@ private val nat = "[0-9]+".r ^^ token(Token.Kind.NAT) - private val ident = - """[\x21-\x7f&&[^"#%'(),={}0-9]][\x21-\x7f&&[^"#%'(),={}]]*""".r ^^ token(Token.Kind.IDENT) + 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 */ + private val special_ident = + identifier ^^ { case a => + val kind = + if (is_command(a)) Token.Kind.COMMAND + else if (get_entry(a).isDefined) Token.Kind.ENTRY + else Token.Kind.IDENT + Token(kind, a) + } + private val item_start: Parser[(String, List[Token])] = - at ~ rep(strict_space) ~ ident ~ rep(strict_space) ^^ + at ~ rep(strict_space) ~ special_ident ~ rep(strict_space) ^^ { case a ~ b ~ c ~ d => (c.source, List(a) ::: b ::: List(c) ::: d) } private val item_body = @@ -285,7 +308,7 @@ { case (kind, a) ~ b ~ c ~ d => Item(kind, a ::: List(b) ::: c ::: d.toList) } private val recover_item: Parser[Item] = - at ~ "(?m)[^@]+".r ^^ { case a ~ b => Item("", List(a, Token(Token.Kind.ERROR, b))) } + at ~ "(?m)[^@]*".r ^^ { case a ~ b => Item("", List(a, Token(Token.Kind.ERROR, b))) } def item_line(ctxt: Line_Context): Parser[(Item, Line_Context)] = { @@ -294,7 +317,8 @@ item_start ~ (left_brace | left_paren) ^^ { case (kind, a) ~ b => val right = if (b.source == "{") "}" else ")" - (Item(kind, a ::: List(b)), Item_Context(kind, Closed, right)) } + (Item(kind, a ::: List(b)), Item_Context(kind, Closed, right)) } | + recover_item ^^ { case a => (a, Ignored_Context) } case Item_Context(kind, delim, right) => if (delim.depth > 0) delimited_line(ctxt) diff -r 7d6b8f8893e8 -r cd4439d8799c src/Tools/jEdit/lib/Tools/jedit --- a/src/Tools/jEdit/lib/Tools/jedit Fri Oct 03 23:33:47 2014 +0200 +++ b/src/Tools/jEdit/lib/Tools/jedit Sat Oct 04 12:19:26 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 7d6b8f8893e8 -r cd4439d8799c 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 12:19:26 2014 +0200 @@ -0,0 +1,94 @@ +/* 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(item_kind: 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.IDENT => + if (Bibtex.is_month(token.source)) JEditToken.LITERAL3 + else + Bibtex.get_entry(item_kind) 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.IGNORED => JEditToken.NULL + 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 + 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 7d6b8f8893e8 -r cd4439d8799c src/Tools/jEdit/src/isabelle.scala --- a/src/Tools/jEdit/src/isabelle.scala Fri Oct 03 23:33:47 2014 +0200 +++ b/src/Tools/jEdit/src/isabelle.scala Sat Oct 04 12:19:26 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 7d6b8f8893e8 -r cd4439d8799c src/Tools/jEdit/src/isabelle_sidekick.scala --- a/src/Tools/jEdit/src/isabelle_sidekick.scala Fri Oct 03 23:33:47 2014 +0200 +++ b/src/Tools/jEdit/src/isabelle_sidekick.scala Sat Oct 04 12:19:26 2014 +0200 @@ -231,7 +231,7 @@ try { var offset = 0 for (chunk <- Bibtex.parse(JEdit_Lib.buffer_text(buffer))) { - val n = chunk.size + val n = chunk.source.size chunk match { case item: Bibtex.Item if item.is_wellformed => val label = if (item.name == "") item.kind else item.kind + " " + item.name diff -r 7d6b8f8893e8 -r cd4439d8799c src/Tools/jEdit/src/token_markup.scala --- a/src/Tools/jEdit/src/token_markup.scala Fri Oct 03 23:33:47 2014 +0200 +++ b/src/Tools/jEdit/src/token_markup.scala Sat Oct 04 12:19:26 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 } }