--- a/NEWS Thu Dec 28 23:39:02 2017 +0100
+++ b/NEWS Fri Dec 29 17:40:57 2017 +0100
@@ -103,6 +103,9 @@
antiquotations in control symbol notation, e.g. \<^const_name> becomes
\isactrlconstUNDERSCOREname.
+* Document antiquotation @{cite} now checks the given Bibtex entries
+against the Bibtex database files -- only in batch-mode session builds.
+
* Document antiquotation @{session name} checks and prints the given
session name verbatim.
--- a/src/Doc/Isar_Ref/Document_Preparation.thy Thu Dec 28 23:39:02 2017 +0100
+++ b/src/Doc/Isar_Ref/Document_Preparation.thy Fri Dec 29 17:40:57 2017 +0100
@@ -301,7 +301,8 @@
active hyperlink within the text.
\<^descr> \<open>@{cite name}\<close> produces a citation \<^verbatim>\<open>\cite{name}\<close> in {\LaTeX}, where the
- name refers to some Bib{\TeX} database entry.
+ name refers to some Bib{\TeX} database entry. This is only checked in
+ batch-mode session builds.
The variant \<open>@{cite \<open>opt\<close> name}\<close> produces \<^verbatim>\<open>\cite[opt]{name}\<close> with some
free-form optional argument. Multiple names are output with commas, e.g.
--- a/src/Pure/Thy/bibtex.ML Thu Dec 28 23:39:02 2017 +0100
+++ b/src/Pure/Thy/bibtex.ML Fri Dec 29 17:40:57 2017 +0100
@@ -51,6 +51,14 @@
Parse.and_list1 (Parse.position Args.name)))
(fn {context = ctxt, ...} => fn (opt, citations) =>
let
+ val thy = Proof_Context.theory_of ctxt;
+ val bibtex_entries = Present.get_bibtex_entries thy;
+ val _ =
+ if null bibtex_entries andalso Context.theory_name thy <> Context.PureN then ()
+ else
+ citations |> List.app (fn (name, pos) =>
+ if member (op =) bibtex_entries name then ()
+ else error ("Unknown Bibtex entry " ^ quote name ^ Position.here pos));
val _ =
Context_Position.reports ctxt
(map (fn (name, pos) => (pos, Markup.citation name)) citations);
--- a/src/Pure/Thy/present.ML Thu Dec 28 23:39:02 2017 +0100
+++ b/src/Pure/Thy/present.ML Fri Dec 29 17:40:57 2017 +0100
@@ -6,6 +6,7 @@
signature PRESENT =
sig
+ val get_bibtex_entries: theory -> string list
val theory_qualifier: theory -> string
val document_enabled: string -> bool
val document_variants: string -> (string * string) list
@@ -13,7 +14,7 @@
(Path.T * Path.T) list -> Path.T -> string * string -> bool -> unit
val finish: unit -> unit
val theory_output: Position.T -> theory -> Latex.text list -> unit
- val begin_theory: int -> (unit -> HTML.text) -> theory -> theory
+ val begin_theory: string list -> int -> (unit -> HTML.text) -> theory -> theory
end;
structure Present: PRESENT =
@@ -39,15 +40,16 @@
structure Browser_Info = Theory_Data
(
- type T = {chapter: string, name: string};
- val empty = {chapter = "Unsorted", name = "Unknown"}: T;
+ type T = {chapter: string, name: string, bibtex_entries: string list};
+ val empty = {chapter = "Unsorted", name = "Unknown", bibtex_entries = []}: T;
fun extend _ = empty;
fun merge _ = empty;
);
val _ = Theory.setup
- (Browser_Info.put {chapter = Context.PureN, name = Context.PureN});
+ (Browser_Info.put {chapter = Context.PureN, name = Context.PureN, bibtex_entries = []});
+val get_bibtex_entries = #bibtex_entries o Browser_Info.get;
(** global browser info state **)
@@ -288,7 +290,7 @@
fun theory_link (curr_chapter, curr_session) thy =
let
- val {chapter, name = session} = Browser_Info.get thy;
+ val {chapter, name = session, ...} = Browser_Info.get thy;
val link = html_path (Context.theory_name thy);
in
if curr_session = session then SOME link
@@ -298,7 +300,7 @@
else SOME (Path.appends [Path.parent, Path.parent, Path.basic chapter, Path.basic session, link])
end;
-fun begin_theory update_time mk_text thy =
+fun begin_theory bibtex_entries update_time mk_text thy =
with_session_info thy (fn {symbols, name = session_name, chapter, ...} =>
let
val name = Context.theory_name thy;
@@ -315,6 +317,8 @@
(add_html_index (update_time, HTML.theory_entry symbols (Url.File (html_path name), name));
add_tex_index (update_time, Latex.theory_entry name))
else ();
- in Browser_Info.put {chapter = chapter, name = session_name} thy end);
+ in
+ Browser_Info.put {chapter = chapter, name = session_name, bibtex_entries = bibtex_entries} thy
+ end);
end;
--- a/src/Pure/Thy/sessions.scala Thu Dec 28 23:39:02 2017 +0100
+++ b/src/Pure/Thy/sessions.scala Fri Dec 29 17:40:57 2017 +0100
@@ -321,6 +321,10 @@
val sources_errors =
for (p <- session_files if !p.is_file) yield "No such file: " + p
+ val bibtex_errors =
+ try { info.bibtex_entries; Nil }
+ catch { case ERROR(msg) => List(msg) }
+
val base =
Base(
pos = info.pos,
@@ -331,7 +335,7 @@
imported_sources = check_sources(imported_files),
sources = check_sources(session_files),
session_graph_display = session_graph_display,
- errors = dependencies.errors ::: sources_errors,
+ errors = dependencies.errors ::: sources_errors ::: bibtex_errors,
imports = Some(imports_base))
session_bases + (info.name -> base)
@@ -458,6 +462,13 @@
def deps: List[String] = parent.toList ::: imports
def timeout: Time = Time.seconds(options.real("timeout") * options.real("timeout_scale"))
+
+ def bibtex_entries: List[Text.Info[String]] =
+ (for {
+ (document_dir, file) <- document_files.iterator
+ if Bibtex.is_bibtex(file.base_name)
+ info <- Bibtex.entries(File.read(dir + document_dir + file)).iterator
+ } yield info).toList
}
def make_info(options: Options, dir_selected: Boolean, dir: Path, chapter: String,
--- a/src/Pure/Thy/thy_info.ML Thu Dec 28 23:39:02 2017 +0100
+++ b/src/Pure/Thy/thy_info.ML Fri Dec 29 17:40:57 2017 +0100
@@ -16,6 +16,7 @@
val use_theories:
{document: bool,
symbols: HTML.symbols,
+ bibtex_entries: string list,
last_timing: Toplevel.transition -> Time.time,
qualifier: string,
master_dir: Path.T} -> (string * Position.T) list -> unit
@@ -242,7 +243,8 @@
val thy = Toplevel.end_theory end_pos end_state;
in (results, thy) end;
-fun eval_thy document symbols last_timing update_time master_dir header text_pos text parents =
+fun eval_thy {document, symbols, bibtex_entries, last_timing} update_time master_dir header
+ text_pos text parents =
let
val (name, _) = #name header;
val keywords =
@@ -255,7 +257,7 @@
fun init () =
Resources.begin_theory master_dir header parents
- |> Present.begin_theory update_time
+ |> Present.begin_theory bibtex_entries update_time
(fn () => implode (map (HTML.present_span symbols keywords) spans));
val (results, thy) =
@@ -282,8 +284,7 @@
fun required_by _ [] = ""
| required_by s initiators = s ^ "(required by " ^ show_path (rev initiators) ^ ")";
-fun load_thy document symbols last_timing
- initiators update_time deps text (name, pos) keywords parents =
+fun load_thy context initiators update_time deps text (name, pos) keywords parents =
let
val _ = remove_thy name;
val _ = writeln ("Loading theory " ^ quote name ^ required_by " " initiators);
@@ -304,7 +305,7 @@
val text_pos = Position.put_id (Document_ID.print exec_id) (Path.position thy_path);
val (theory, present, weight) =
- eval_thy document symbols last_timing update_time dir header text_pos text
+ eval_thy context update_time dir header text_pos text
(if name = Context.PureN then [Context.the_global_context ()] else parents);
val timing_result = Timing.result timing_start;
@@ -336,10 +337,9 @@
in
-fun require_thys document symbols last_timing initiators qualifier dir strs tasks =
- fold_map (require_thy document symbols last_timing initiators qualifier dir) strs tasks
- |>> forall I
-and require_thy document symbols last_timing initiators qualifier dir (s, require_pos) tasks =
+fun require_thys context initiators qualifier dir strs tasks =
+ fold_map (require_thy context initiators qualifier dir) strs tasks |>> forall I
+and require_thy context initiators qualifier dir (s, require_pos) tasks =
let
val {master_dir, theory_name, ...} = Resources.import_name qualifier dir s;
in
@@ -360,8 +360,7 @@
val parents = map (#theory_name o Resources.import_name qualifier' dir' o #1) imports;
val (parents_current, tasks') =
- require_thys document symbols last_timing (theory_name :: initiators)
- qualifier' dir' imports tasks;
+ require_thys context (theory_name :: initiators) qualifier' dir' imports tasks;
val all_current = current andalso parents_current;
val task =
@@ -373,8 +372,8 @@
let
val update_time = serial ();
val load =
- load_thy document symbols last_timing initiators update_time dep
- text (theory_name, theory_pos) keywords;
+ load_thy context initiators update_time
+ dep text (theory_name, theory_pos) keywords;
in Task (parents, load) end);
val tasks'' = new_entry theory_name parents task tasks';
@@ -386,16 +385,19 @@
(* use theories *)
-fun use_theories {document, symbols, last_timing, qualifier, master_dir} imports =
+fun use_theories {document, symbols, bibtex_entries, last_timing, qualifier, master_dir} imports =
let
- val (_, tasks) =
- require_thys document symbols last_timing [] qualifier master_dir imports String_Graph.empty;
+ val context =
+ {document = document, symbols = symbols, bibtex_entries = bibtex_entries,
+ last_timing = last_timing};
+ val (_, tasks) = require_thys context [] qualifier master_dir imports String_Graph.empty;
in if Multithreading.enabled () then schedule_futures tasks else schedule_seq tasks end;
fun use_thy name =
use_theories
- {document = false, symbols = HTML.no_symbols, last_timing = K Time.zeroTime,
- qualifier = Resources.default_qualifier, master_dir = Path.current}
+ {document = false, symbols = HTML.no_symbols, bibtex_entries = [],
+ last_timing = K Time.zeroTime, qualifier = Resources.default_qualifier,
+ master_dir = Path.current}
[(name, Position.none)];
--- a/src/Pure/Tools/build.ML Thu Dec 28 23:39:02 2017 +0100
+++ b/src/Pure/Tools/build.ML Fri Dec 29 17:40:57 2017 +0100
@@ -103,7 +103,7 @@
(* build theories *)
-fun build_theories symbols last_timing qualifier master_dir (options, thys) =
+fun build_theories symbols bibtex_entries last_timing qualifier master_dir (options, thys) =
let
val condition = space_explode "," (Options.string options "condition");
val conds = filter_out (can getenv_strict) condition;
@@ -116,6 +116,7 @@
(Thy_Info.use_theories {
document = Present.document_enabled (Options.string options "document"),
symbols = symbols,
+ bibtex_entries = bibtex_entries,
last_timing = last_timing,
qualifier = qualifier,
master_dir = master_dir}
@@ -151,7 +152,8 @@
sessions: string list,
global_theories: (string * string) list,
loaded_theories: string list,
- known_theories: (string * string) list};
+ known_theories: (string * string) list,
+ bibtex_entries: string list};
fun decode_args yxml =
let
@@ -159,13 +161,14 @@
val position = Position.of_properties o properties;
val (symbol_codes, (command_timings, (do_output, (verbose, (browser_info,
(document_files, (graph_file, (parent_name, (chapter, (name, (master_dir,
- (theories, (sessions, (global_theories, (loaded_theories, known_theories))))))))))))))) =
+ (theories, (sessions, (global_theories, (loaded_theories,
+ (known_theories, bibtex_entries)))))))))))))))) =
pair (list (pair string int)) (pair (list properties) (pair bool (pair bool (pair string
(pair (list (pair string string)) (pair string (pair string (pair string (pair string
(pair string
(pair (((list (pair Options.decode (list (pair string position))))))
- (pair (list string) (pair (list (pair string string))
- (pair (list string) (list (pair string string))))))))))))))))
+ (pair (list string) (pair (list (pair string string)) (pair (list string)
+ (pair (list (pair string string)) (list string))))))))))))))))
(YXML.parse_body yxml);
in
Args {symbol_codes = symbol_codes, command_timings = command_timings, do_output = do_output,
@@ -174,12 +177,12 @@
graph_file = Path.explode graph_file, parent_name = parent_name, chapter = chapter,
name = name, master_dir = Path.explode master_dir, theories = theories, sessions = sessions,
global_theories = global_theories, loaded_theories = loaded_theories,
- known_theories = known_theories}
+ known_theories = known_theories, bibtex_entries = bibtex_entries}
end;
fun build_session (Args {symbol_codes, command_timings, do_output, verbose, browser_info,
document_files, graph_file, parent_name, chapter, name, master_dir, theories, sessions,
- global_theories, loaded_theories, known_theories}) =
+ global_theories, loaded_theories, known_theories, bibtex_entries}) =
let
val symbols = HTML.make_symbols symbol_codes;
@@ -209,7 +212,7 @@
val res1 =
theories |>
- (List.app (build_theories symbols last_timing name master_dir)
+ (List.app (build_theories symbols bibtex_entries last_timing name master_dir)
|> session_timing name verbose
|> Exn.capture);
val res2 = Exn.capture Session.finish ();
--- a/src/Pure/Tools/build.scala Thu Dec 28 23:39:02 2017 +0100
+++ b/src/Pure/Tools/build.scala Fri Dec 29 17:40:57 2017 +0100
@@ -213,13 +213,15 @@
pair(string, pair(string, pair(string, pair(Path.encode,
pair(list(pair(Options.encode, list(pair(string, properties)))),
pair(list(string), pair(list(pair(string, string)), pair(list(string),
- list(pair(string, string)))))))))))))))))(
+ pair(list(pair(string, string)), list(string)))))))))))))))))(
(Symbol.codes, (command_timings, (do_output, (verbose,
(store.browser_info, (info.document_files, (File.standard_path(graph_file),
(parent, (info.chapter, (name, (Path.current,
(info.theories, (base.known.sessions.toList,
- (base.global_theories.toList, (base.loaded_theories.keys,
- base.dest_known_theories))))))))))))))))
+ (base.global_theories.toList,
+ (base.loaded_theories.keys,
+ (base.dest_known_theories,
+ info.bibtex_entries.map(_.info))))))))))))))))))
})
val env =