--- 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 ***
--- 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 \<open>opt\<close> name}"} produces @{verbatim
+ "\\cite[opt]{name}"} with some free-form optional argument. Multiple names
+ are output with commas, e.g. @{text "@{cite foo \<AND> 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}
*}
--- 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("")
}
}
--- 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(", ")
--- 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
--- 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 {
--- 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 */