bibtex support in ML: document antiquotation @{cite} with markup;
authorwenzelm
Sun Oct 05 16:05:17 2014 +0200 (2014-10-05 ago)
changeset 58544340f130b3d38
parent 58543 9c1389befa56
child 58545 30b75b7958d6
bibtex support in ML: document antiquotation @{cite} with markup;
src/Pure/PIDE/markup.ML
src/Pure/PIDE/markup.scala
src/Pure/Pure.thy
src/Pure/Tools/bibtex.ML
src/Pure/Tools/bibtex.scala
     1.1 --- a/src/Pure/PIDE/markup.ML	Sun Oct 05 15:05:26 2014 +0200
     1.2 +++ b/src/Pure/PIDE/markup.ML	Sun Oct 05 16:05:17 2014 +0200
     1.3 @@ -55,6 +55,7 @@
     1.4    val position_properties: string list
     1.5    val positionN: string val position: T
     1.6    val expressionN: string val expression: T
     1.7 +  val citationN: string val citation: T
     1.8    val pathN: string val path: string -> T
     1.9    val urlN: string val url: string -> T
    1.10    val indentN: string
    1.11 @@ -346,6 +347,11 @@
    1.12  val (expressionN, expression) = markup_elem "expression";
    1.13  
    1.14  
    1.15 +(* citation *)
    1.16 +
    1.17 +val (citationN, citation) = markup_elem "citation";
    1.18 +
    1.19 +
    1.20  (* external resources *)
    1.21  
    1.22  val (pathN, path) = markup_string "path" nameN;
     2.1 --- a/src/Pure/PIDE/markup.scala	Sun Oct 05 15:05:26 2014 +0200
     2.2 +++ b/src/Pure/PIDE/markup.scala	Sun Oct 05 16:05:17 2014 +0200
     2.3 @@ -120,6 +120,11 @@
     2.4    val EXPRESSION = "expression"
     2.5  
     2.6  
     2.7 +  /* citation */
     2.8 +
     2.9 +  val CITATION = "citation"
    2.10 +
    2.11 +
    2.12    /* embedded languages */
    2.13  
    2.14    val Symbols = new Properties.Boolean("symbols")
     3.1 --- a/src/Pure/Pure.thy	Sun Oct 05 15:05:26 2014 +0200
     3.2 +++ b/src/Pure/Pure.thy	Sun Oct 05 16:05:17 2014 +0200
     3.3 @@ -110,6 +110,7 @@
     3.4  ML_file "Tools/print_operation.ML"
     3.5  ML_file "Isar/isar_syn.ML"
     3.6  ML_file "Isar/calculation.ML"
     3.7 +ML_file "Tools/bibtex.ML"
     3.8  ML_file "Tools/rail.ML"
     3.9  ML_file "Tools/rule_insts.ML";
    3.10  ML_file "Tools/thm_deps.ML";
     4.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     4.2 +++ b/src/Pure/Tools/bibtex.ML	Sun Oct 05 16:05:17 2014 +0200
     4.3 @@ -0,0 +1,32 @@
     4.4 +(*  Title:      Pure/Tools/bibtex.ML
     4.5 +    Author:     Makarius
     4.6 +
     4.7 +BibTeX support.
     4.8 +*)
     4.9 +
    4.10 +signature BIBTEX =
    4.11 +sig
    4.12 +  val cite_macro: string Config.T
    4.13 +end;
    4.14 +
    4.15 +structure Bibtex: BIBTEX =
    4.16 +struct
    4.17 +
    4.18 +val cite_macro = Attrib.setup_config_string @{binding cite_macro} (K "cite");
    4.19 +
    4.20 +val _ =
    4.21 +  Theory.setup
    4.22 +   (Thy_Output.add_option @{binding cite_macro} (Config.put cite_macro) #>
    4.23 +    Thy_Output.antiquotation @{binding cite}
    4.24 +      (Scan.lift
    4.25 +        (Scan.option (Parse.verbatim || Parse.cartouche) --
    4.26 +         Scan.repeat1 (Parse.position Args.name)))
    4.27 +      (fn {context = ctxt, ...} => fn (opt, cites) =>
    4.28 +        let
    4.29 +          val _ = Context_Position.reports ctxt (map (fn (_, p) => (p, Markup.citation)) cites);
    4.30 +          val opt_arg = (case opt of NONE => "" | SOME s => "[" ^ s ^ "]");
    4.31 +          val arg = "{" ^ space_implode "," (map #1 cites) ^ "}";
    4.32 +        in "\\" ^ Config.get ctxt cite_macro ^ opt_arg ^ arg end));
    4.33 +
    4.34 +end;
    4.35 +
     5.1 --- a/src/Pure/Tools/bibtex.scala	Sun Oct 05 15:05:26 2014 +0200
     5.2 +++ b/src/Pure/Tools/bibtex.scala	Sun Oct 05 16:05:17 2014 +0200
     5.3 @@ -1,7 +1,7 @@
     5.4  /*  Title:      Pure/Tools/bibtex.scala
     5.5      Author:     Makarius
     5.6  
     5.7 -Some support for bibtex files.
     5.8 +BibTeX support.
     5.9  */
    5.10  
    5.11  package isabelle