# HG changeset patch
# User wenzelm
# Date 1412517917 -7200
# Node ID 340f130b3d383083747aeb23052e2a16431ec048
# Parent  9c1389befa56ffdb72fe1be80c6e0cb1c80ce380
bibtex support in ML: document antiquotation @{cite} with markup;

diff -r 9c1389befa56 -r 340f130b3d38 src/Pure/PIDE/markup.ML
--- a/src/Pure/PIDE/markup.ML	Sun Oct 05 15:05:26 2014 +0200
+++ b/src/Pure/PIDE/markup.ML	Sun Oct 05 16:05:17 2014 +0200
@@ -55,6 +55,7 @@
   val position_properties: string list
   val positionN: string val position: T
   val expressionN: string val expression: T
+  val citationN: string val citation: T
   val pathN: string val path: string -> T
   val urlN: string val url: string -> T
   val indentN: string
@@ -346,6 +347,11 @@
 val (expressionN, expression) = markup_elem "expression";
 
 
+(* citation *)
+
+val (citationN, citation) = markup_elem "citation";
+
+
 (* external resources *)
 
 val (pathN, path) = markup_string "path" nameN;
diff -r 9c1389befa56 -r 340f130b3d38 src/Pure/PIDE/markup.scala
--- a/src/Pure/PIDE/markup.scala	Sun Oct 05 15:05:26 2014 +0200
+++ b/src/Pure/PIDE/markup.scala	Sun Oct 05 16:05:17 2014 +0200
@@ -120,6 +120,11 @@
   val EXPRESSION = "expression"
 
 
+  /* citation */
+
+  val CITATION = "citation"
+
+
   /* embedded languages */
 
   val Symbols = new Properties.Boolean("symbols")
diff -r 9c1389befa56 -r 340f130b3d38 src/Pure/Pure.thy
--- a/src/Pure/Pure.thy	Sun Oct 05 15:05:26 2014 +0200
+++ b/src/Pure/Pure.thy	Sun Oct 05 16:05:17 2014 +0200
@@ -110,6 +110,7 @@
 ML_file "Tools/print_operation.ML"
 ML_file "Isar/isar_syn.ML"
 ML_file "Isar/calculation.ML"
+ML_file "Tools/bibtex.ML"
 ML_file "Tools/rail.ML"
 ML_file "Tools/rule_insts.ML";
 ML_file "Tools/thm_deps.ML";
diff -r 9c1389befa56 -r 340f130b3d38 src/Pure/Tools/bibtex.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/Tools/bibtex.ML	Sun Oct 05 16:05:17 2014 +0200
@@ -0,0 +1,32 @@
+(*  Title:      Pure/Tools/bibtex.ML
+    Author:     Makarius
+
+BibTeX support.
+*)
+
+signature BIBTEX =
+sig
+  val cite_macro: string Config.T
+end;
+
+structure Bibtex: BIBTEX =
+struct
+
+val cite_macro = Attrib.setup_config_string @{binding cite_macro} (K "cite");
+
+val _ =
+  Theory.setup
+   (Thy_Output.add_option @{binding cite_macro} (Config.put cite_macro) #>
+    Thy_Output.antiquotation @{binding cite}
+      (Scan.lift
+        (Scan.option (Parse.verbatim || Parse.cartouche) --
+         Scan.repeat1 (Parse.position Args.name)))
+      (fn {context = ctxt, ...} => fn (opt, cites) =>
+        let
+          val _ = Context_Position.reports ctxt (map (fn (_, p) => (p, Markup.citation)) cites);
+          val opt_arg = (case opt of NONE => "" | SOME s => "[" ^ s ^ "]");
+          val arg = "{" ^ space_implode "," (map #1 cites) ^ "}";
+        in "\\" ^ Config.get ctxt cite_macro ^ opt_arg ^ arg end));
+
+end;
+
diff -r 9c1389befa56 -r 340f130b3d38 src/Pure/Tools/bibtex.scala
--- a/src/Pure/Tools/bibtex.scala	Sun Oct 05 15:05:26 2014 +0200
+++ b/src/Pure/Tools/bibtex.scala	Sun Oct 05 16:05:17 2014 +0200
@@ -1,7 +1,7 @@
 /*  Title:      Pure/Tools/bibtex.scala
     Author:     Makarius
 
-Some support for bibtex files.
+BibTeX support.
 */
 
 package isabelle