# HG changeset patch # User wenzelm # Date 1412609247 -7200 # Node ID 72e2f0e7e3449c04f4ccc140790708fb5629c0ea # Parent 93d87fd1583db58e0ecc73654a3d6367499fb51e# Parent 51adee3ace7b35165677914d44ff818ae72a941d merged diff -r 93d87fd1583d -r 72e2f0e7e344 NEWS --- a/NEWS Mon Oct 06 16:27:31 2014 +0200 +++ b/NEWS Mon Oct 06 17:27:27 2014 +0200 @@ -22,7 +22,7 @@ * Document antiquotation @{cite} provides formal markup, which is interpreted semi-formally based on .bib files that happen to be opened -in the editor (hyperlinks etc.). +in the editor (hyperlinks, completion etc.). *** Pure *** diff -r 93d87fd1583d -r 72e2f0e7e344 src/Doc/Isar_Ref/Document_Preparation.thy --- a/src/Doc/Isar_Ref/Document_Preparation.thy Mon Oct 06 16:27:31 2014 +0200 +++ b/src/Doc/Isar_Ref/Document_Preparation.thy Mon Oct 06 17:27:27 2014 +0200 @@ -127,6 +127,7 @@ @{antiquotation_def ML_functor} & : & @{text antiquotation} \\ @{antiquotation_def "file"} & : & @{text antiquotation} \\ @{antiquotation_def "url"} & : & @{text antiquotation} \\ + @{antiquotation_def "cite"} & : & @{text antiquotation} \\ \end{matharray} The overall content of an Isabelle/Isar theory may alternate between @@ -180,7 +181,8 @@ @@{antiquotation ML_functor} options @{syntax text} | @@{antiquotation "file"} options @{syntax name} | @@{antiquotation file_unchecked} options @{syntax name} | - @@{antiquotation url} options @{syntax name} + @@{antiquotation url} options @{syntax name} | + @@{antiquotation cite} options @{syntax cartouche}? (@{syntax name} + @'and') ; options: '[' (option * ',') ']' ; @@ -279,6 +281,20 @@ \item @{text "@{url name}"} produces markup for the given URL, which results in an active hyperlink within the text. + \item @{text "@{cite name}"} produces a citation @{verbatim + "\\cite{name}"} in {\LaTeX}, where the name refers to some Bib{\TeX} + database entry. + + The variant @{text "@{cite \opt\ name}"} produces @{verbatim + "\\cite[opt]{name}"} with some free-form optional argument. Multiple names + are output with commas, e.g. @{text "@{cite foo \ bar}"} becomes + @{verbatim "\\cite{foo,bar}"}. + + The {\LaTeX} macro name is determined by the antiquotation option + @{antiquotation_option_def cite_macro}, or the configuration option + @{attribute cite_macro} in the context. For example, @{text "@{cite + [cite_macro = nocite] foobar}"} produces @{verbatim "\\nocite{foobar}"}. + \end{description} *} diff -r 93d87fd1583d -r 72e2f0e7e344 src/Pure/Tools/bibtex.scala --- a/src/Pure/Tools/bibtex.scala Mon Oct 06 16:27:31 2014 +0200 +++ b/src/Pure/Tools/bibtex.scala Mon Oct 06 17:27:27 2014 +0200 @@ -186,8 +186,12 @@ // 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 object Ignored extends Line_Context + case object At extends Line_Context + case class Item_Start(kind: String) extends Line_Context + case class Item_Open(kind: String, end: String) extends Line_Context + case class Item(kind: String, end: String, delim: Delimited) extends Line_Context + case class Delimited(quoted: Boolean, depth: Int) val Closed = Delimited(false, 0) @@ -205,7 +209,7 @@ 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 spaces = rep(space) /* ignored text */ @@ -215,7 +219,7 @@ case ss => Chunk("", List(Token(Token.Kind.COMMENT, ss.mkString))) } private def ignored_line: Parser[(Chunk, Line_Context)] = - ignored ^^ { case a => (a, Ignored_Context) } + ignored ^^ { case a => (a, Ignored) } /* delimited string: outermost "..." or {...} and body with balanced {...} */ @@ -265,25 +269,20 @@ 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) } - } + def delimited_line(ctxt: Item): Parser[(Chunk, Line_Context)] = + delimited_depth(ctxt.delim) ^^ { case (s, delim1) => + (Chunk(ctxt.kind, List(Token(Token.Kind.STRING, s))), ctxt.copy(delim = delim1)) } | + recover_delimited ^^ { case a => (Chunk(ctxt.kind, List(a)), Ignored) } /* 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 name = """[\x21-\x7f&&[^"#%'(),={}]]+""".r ^^ token(Token.Kind.NAME) + private val identifier = """[\x21-\x7f&&[^"#%'(),={}0-9]][\x21-\x7f&&[^"#%'(),={}]]*""".r @@ -292,6 +291,20 @@ val other_token = "[=#,]".r ^^ keyword | (nat | (ident | space)) + /* body */ + + private val body = + delimited | (recover_delimited | other_token) + + private def body_line(ctxt: Item) = + if (ctxt.delim.depth > 0) + delimited_line(ctxt) + else + delimited_line(ctxt) | + other_token ^^ { case a => (Chunk(ctxt.kind, List(a)), ctxt) } | + ctxt.end ^^ { case a => (Chunk(ctxt.kind, List(keyword(a))), Ignored) } + + /* items: command or entry */ private val item_kind = @@ -303,21 +316,26 @@ Token(kind, a) } + private val item_begin = + "{" ^^ { case a => ("}", keyword(a)) } | + "(" ^^ { case a => (")", keyword(a)) } + + private def item_name(kind: String) = + kind.toLowerCase match { + case "preamble" => failure("") + case "string" => identifier ^^ token(Token.Kind.NAME) + case _ => name + } + private val item_start = - at ~ rep(strict_space) ~ item_kind ~ rep(strict_space) ^^ + at ~ spaces ~ item_kind ~ spaces ^^ { 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) } + (item_start ~ item_begin ~ spaces) into + { case (kind, a) ~ ((end, b)) ~ c => + opt(item_name(kind)) ~ rep(body) ~ opt(end ^^ keyword) ^^ { + case d ~ e ~ f => Chunk(kind, a ::: List(b) ::: c ::: d.toList ::: e ::: f.toList) } } private val recover_item: Parser[Chunk] = at ~ "(?m)[^@]*".r ^^ { case a ~ b => Chunk("", List(a, Token(Token.Kind.ERROR, b))) } @@ -330,24 +348,31 @@ def chunk_line(ctxt: Line_Context): Parser[(Chunk, Line_Context)] = { ctxt match { - case Ignored_Context => + case Ignored => 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 - } + at ^^ { case a => (Chunk("", List(a)), At) } + + case At => + space ^^ { case a => (Chunk("", List(a)), ctxt) } | + item_kind ^^ { case a => (Chunk(a.source, List(a)), Item_Start(a.source)) } | + recover_item ^^ { case a => (a, Ignored) } | + ignored_line + + case Item_Start(kind) => + space ^^ { case a => (Chunk(kind, List(a)), ctxt) } | + item_begin ^^ { case (end, a) => (Chunk(kind, List(a)), Item_Open(kind, end)) } | + ignored_line + + case Item_Open(kind, end) => + space ^^ { case a => (Chunk(kind, List(a)), ctxt) } | + item_name(kind) ^^ { case a => (Chunk(kind, List(a)), Item(kind, end, Closed)) } | + body_line(Item(kind, end, Closed)) | + ignored_line + + case item_ctxt: Item => + body_line(item_ctxt) | + ignored_line + case _ => failure("") } } diff -r 93d87fd1583d -r 72e2f0e7e344 src/Pure/library.scala --- a/src/Pure/library.scala Mon Oct 06 16:27:31 2014 +0200 +++ b/src/Pure/library.scala Mon Oct 06 17:27:27 2014 +0200 @@ -145,6 +145,8 @@ if (s.startsWith("\"") && s.endsWith("\"")) Some(s.substring(1, s.length - 1)) else None + def perhaps_unquote(s: String): String = try_unquote(s) getOrElse s + def commas(ss: Iterable[String]): String = ss.iterator.mkString(", ") def commas_quote(ss: Iterable[String]): String = ss.iterator.map(quote).mkString(", ") diff -r 93d87fd1583d -r 72e2f0e7e344 src/Tools/jEdit/src/bibtex_jedit.scala --- a/src/Tools/jEdit/src/bibtex_jedit.scala Mon Oct 06 16:27:31 2014 +0200 +++ b/src/Tools/jEdit/src/bibtex_jedit.scala Mon Oct 06 17:27:27 2014 +0200 @@ -29,9 +29,14 @@ { /** buffer model **/ + /* file type */ + def check(buffer: Buffer): Boolean = JEdit_Lib.buffer_name(buffer).endsWith(".bib") + + /* parse entries */ + def parse_buffer_entries(buffer: Buffer): List[(String, Text.Offset)] = { val chunks = @@ -47,6 +52,9 @@ result.toList } + + /* retrieve entries */ + def entries_iterator(): Iterator[(String, Buffer, Text.Offset)] = for { buffer <- JEdit_Lib.jedit_buffers() @@ -55,6 +63,38 @@ } yield (name, buffer, offset) + /* completion */ + + def complete(name: String): List[String] = + { + val name1 = name.toLowerCase + (for ((entry, _, _) <- entries_iterator() if entry.toLowerCase.containsSlice(name1)) + yield entry).toList + } + + def completion( + history: Completion.History, + text_area: JEditTextArea, + rendering: Rendering): Option[Completion.Result] = + { + for { + Text.Info(r, name) <- rendering.citation(JEdit_Lib.before_caret_range(text_area, rendering)) + original <- JEdit_Lib.try_get_text(text_area.getBuffer, r) + orig = Library.perhaps_unquote(original) + entries = complete(name).filter(_ != orig) + if !entries.isEmpty + items = + entries.map({ + case entry => + val full_name = Long_Name.qualify(Markup.CITATION, entry) + val description = List(entry, "(BibTeX entry)") + val replacement = quote(entry) + Completion.Item(r, original, full_name, description, replacement, 0, false) + }).sorted(history.ordering).take(PIDE.options.int("completion_limit")) + } yield Completion.Result(r, original, false, items) + } + + /** context menu **/ @@ -127,7 +167,7 @@ val line_ctxt = context match { case c: Line_Context => c.context - case _ => Some(Bibtex.Ignored_Context) + case _ => Some(Bibtex.Ignored) } val line = if (raw_line == null) new Segment else raw_line diff -r 93d87fd1583d -r 72e2f0e7e344 src/Tools/jEdit/src/completion_popup.scala --- a/src/Tools/jEdit/src/completion_popup.scala Mon Oct 06 16:27:31 2014 +0200 +++ b/src/Tools/jEdit/src/completion_popup.scala Mon Oct 06 17:27:27 2014 +0200 @@ -134,7 +134,10 @@ case None => Completion.Result.merge(Completion.History.empty, syntax_completion(Completion.History.empty, false, Some(rendering)), - path_completion(rendering)).map(_.range) + Completion.Result.merge(Completion.History.empty, + path_completion(rendering), + Bibtex_JEdit.completion(Completion.History.empty, text_area, rendering))) + .map(_.range) } case _ => None } @@ -380,7 +383,9 @@ Completion.Result.merge(history, result0, Completion.Result.merge(history, Spell_Checker.completion(text_area, explicit, rendering), - path_completion(rendering))) + Completion.Result.merge(history, + path_completion(rendering), + Bibtex_JEdit.completion(history, text_area, rendering)))) } } result match { diff -r 93d87fd1583d -r 72e2f0e7e344 src/Tools/jEdit/src/rendering.scala --- a/src/Tools/jEdit/src/rendering.scala Mon Oct 06 16:27:31 2014 +0200 +++ b/src/Tools/jEdit/src/rendering.scala Mon Oct 06 17:27:27 2014 +0200 @@ -138,6 +138,8 @@ private val language_elements = Markup.Elements(Markup.LANGUAGE) + private val citation_elements = Markup.Elements(Markup.CITATION) + private val highlight_elements = Markup.Elements(Markup.EXPRESSION, Markup.CITATION, Markup.LANGUAGE, Markup.ML_TYPING, Markup.TOKEN_RANGE, Markup.ENTITY, Markup.PATH, Markup.URL, Markup.SORTING, @@ -296,6 +298,14 @@ case _ => None }).headOption.map(_.info) + def citation(range: Text.Range): Option[Text.Info[String]] = + snapshot.select(range, Rendering.citation_elements, _ => + { + case Text.Info(info_range, XML.Elem(Markup.Citation(name), _)) => + Some(Text.Info(snapshot.convert(info_range), name)) + case _ => None + }).headOption.map(_.info) + /* spell checker */