formal check of @{cite} bibtex entries -- only in batch-mode session builds;
authorwenzelm
Fri Dec 29 17:40:57 2017 +0100 (17 months ago)
changeset 6729786a099f896fc
parent 67296 888aa91f0556
child 67298 fee3ed06a281
formal check of @{cite} bibtex entries -- only in batch-mode session builds;
NEWS
src/Doc/Isar_Ref/Document_Preparation.thy
src/Pure/Thy/bibtex.ML
src/Pure/Thy/present.ML
src/Pure/Thy/sessions.scala
src/Pure/Thy/thy_info.ML
src/Pure/Tools/build.ML
src/Pure/Tools/build.scala
     1.1 --- a/NEWS	Thu Dec 28 23:39:02 2017 +0100
     1.2 +++ b/NEWS	Fri Dec 29 17:40:57 2017 +0100
     1.3 @@ -103,6 +103,9 @@
     1.4  antiquotations in control symbol notation, e.g. \<^const_name> becomes
     1.5  \isactrlconstUNDERSCOREname.
     1.6  
     1.7 +* Document antiquotation @{cite} now checks the given Bibtex entries
     1.8 +against the Bibtex database files -- only in batch-mode session builds.
     1.9 +
    1.10  * Document antiquotation @{session name} checks and prints the given
    1.11  session name verbatim.
    1.12  
     2.1 --- a/src/Doc/Isar_Ref/Document_Preparation.thy	Thu Dec 28 23:39:02 2017 +0100
     2.2 +++ b/src/Doc/Isar_Ref/Document_Preparation.thy	Fri Dec 29 17:40:57 2017 +0100
     2.3 @@ -301,7 +301,8 @@
     2.4    active hyperlink within the text.
     2.5  
     2.6    \<^descr> \<open>@{cite name}\<close> produces a citation \<^verbatim>\<open>\cite{name}\<close> in {\LaTeX}, where the
     2.7 -  name refers to some Bib{\TeX} database entry.
     2.8 +  name refers to some Bib{\TeX} database entry. This is only checked in
     2.9 +  batch-mode session builds.
    2.10  
    2.11    The variant \<open>@{cite \<open>opt\<close> name}\<close> produces \<^verbatim>\<open>\cite[opt]{name}\<close> with some
    2.12    free-form optional argument. Multiple names are output with commas, e.g.
     3.1 --- a/src/Pure/Thy/bibtex.ML	Thu Dec 28 23:39:02 2017 +0100
     3.2 +++ b/src/Pure/Thy/bibtex.ML	Fri Dec 29 17:40:57 2017 +0100
     3.3 @@ -51,6 +51,14 @@
     3.4           Parse.and_list1 (Parse.position Args.name)))
     3.5        (fn {context = ctxt, ...} => fn (opt, citations) =>
     3.6          let
     3.7 +          val thy = Proof_Context.theory_of ctxt;
     3.8 +          val bibtex_entries = Present.get_bibtex_entries thy;
     3.9 +          val _ =
    3.10 +            if null bibtex_entries andalso Context.theory_name thy <> Context.PureN then ()
    3.11 +            else
    3.12 +              citations |> List.app (fn (name, pos) =>
    3.13 +                if member (op =) bibtex_entries name then ()
    3.14 +                else error ("Unknown Bibtex entry " ^ quote name ^ Position.here pos));
    3.15            val _ =
    3.16              Context_Position.reports ctxt
    3.17                (map (fn (name, pos) => (pos, Markup.citation name)) citations);
     4.1 --- a/src/Pure/Thy/present.ML	Thu Dec 28 23:39:02 2017 +0100
     4.2 +++ b/src/Pure/Thy/present.ML	Fri Dec 29 17:40:57 2017 +0100
     4.3 @@ -6,6 +6,7 @@
     4.4  
     4.5  signature PRESENT =
     4.6  sig
     4.7 +  val get_bibtex_entries: theory -> string list
     4.8    val theory_qualifier: theory -> string
     4.9    val document_enabled: string -> bool
    4.10    val document_variants: string -> (string * string) list
    4.11 @@ -13,7 +14,7 @@
    4.12      (Path.T * Path.T) list -> Path.T -> string * string -> bool -> unit
    4.13    val finish: unit -> unit
    4.14    val theory_output: Position.T -> theory -> Latex.text list -> unit
    4.15 -  val begin_theory: int -> (unit -> HTML.text) -> theory -> theory
    4.16 +  val begin_theory: string list -> int -> (unit -> HTML.text) -> theory -> theory
    4.17  end;
    4.18  
    4.19  structure Present: PRESENT =
    4.20 @@ -39,15 +40,16 @@
    4.21  
    4.22  structure Browser_Info = Theory_Data
    4.23  (
    4.24 -  type T = {chapter: string, name: string};
    4.25 -  val empty = {chapter = "Unsorted", name = "Unknown"}: T;
    4.26 +  type T = {chapter: string, name: string, bibtex_entries: string list};
    4.27 +  val empty = {chapter = "Unsorted", name = "Unknown", bibtex_entries = []}: T;
    4.28    fun extend _ = empty;
    4.29    fun merge _ = empty;
    4.30  );
    4.31  
    4.32  val _ = Theory.setup
    4.33 -  (Browser_Info.put {chapter = Context.PureN, name = Context.PureN});
    4.34 +  (Browser_Info.put {chapter = Context.PureN, name = Context.PureN, bibtex_entries = []});
    4.35  
    4.36 +val get_bibtex_entries = #bibtex_entries o Browser_Info.get;
    4.37  
    4.38  
    4.39  (** global browser info state **)
    4.40 @@ -288,7 +290,7 @@
    4.41  
    4.42  fun theory_link (curr_chapter, curr_session) thy =
    4.43    let
    4.44 -    val {chapter, name = session} = Browser_Info.get thy;
    4.45 +    val {chapter, name = session, ...} = Browser_Info.get thy;
    4.46      val link = html_path (Context.theory_name thy);
    4.47    in
    4.48      if curr_session = session then SOME link
    4.49 @@ -298,7 +300,7 @@
    4.50      else SOME (Path.appends [Path.parent, Path.parent, Path.basic chapter, Path.basic session, link])
    4.51    end;
    4.52  
    4.53 -fun begin_theory update_time mk_text thy =
    4.54 +fun begin_theory bibtex_entries update_time mk_text thy =
    4.55    with_session_info thy (fn {symbols, name = session_name, chapter, ...} =>
    4.56      let
    4.57        val name = Context.theory_name thy;
    4.58 @@ -315,6 +317,8 @@
    4.59            (add_html_index (update_time, HTML.theory_entry symbols (Url.File (html_path name), name));
    4.60             add_tex_index (update_time, Latex.theory_entry name))
    4.61          else ();
    4.62 -    in Browser_Info.put {chapter = chapter, name = session_name} thy end);
    4.63 +    in
    4.64 +      Browser_Info.put {chapter = chapter, name = session_name, bibtex_entries = bibtex_entries} thy
    4.65 +    end);
    4.66  
    4.67  end;
     5.1 --- a/src/Pure/Thy/sessions.scala	Thu Dec 28 23:39:02 2017 +0100
     5.2 +++ b/src/Pure/Thy/sessions.scala	Fri Dec 29 17:40:57 2017 +0100
     5.3 @@ -321,6 +321,10 @@
     5.4              val sources_errors =
     5.5                for (p <- session_files if !p.is_file) yield "No such file: " + p
     5.6  
     5.7 +            val bibtex_errors =
     5.8 +              try { info.bibtex_entries; Nil }
     5.9 +              catch { case ERROR(msg) => List(msg) }
    5.10 +
    5.11              val base =
    5.12                Base(
    5.13                  pos = info.pos,
    5.14 @@ -331,7 +335,7 @@
    5.15                  imported_sources = check_sources(imported_files),
    5.16                  sources = check_sources(session_files),
    5.17                  session_graph_display = session_graph_display,
    5.18 -                errors = dependencies.errors ::: sources_errors,
    5.19 +                errors = dependencies.errors ::: sources_errors ::: bibtex_errors,
    5.20                  imports = Some(imports_base))
    5.21  
    5.22              session_bases + (info.name -> base)
    5.23 @@ -458,6 +462,13 @@
    5.24      def deps: List[String] = parent.toList ::: imports
    5.25  
    5.26      def timeout: Time = Time.seconds(options.real("timeout") * options.real("timeout_scale"))
    5.27 +
    5.28 +    def bibtex_entries: List[Text.Info[String]] =
    5.29 +      (for {
    5.30 +        (document_dir, file) <- document_files.iterator
    5.31 +        if Bibtex.is_bibtex(file.base_name)
    5.32 +        info <- Bibtex.entries(File.read(dir + document_dir + file)).iterator
    5.33 +      } yield info).toList
    5.34    }
    5.35  
    5.36    def make_info(options: Options, dir_selected: Boolean, dir: Path, chapter: String,
     6.1 --- a/src/Pure/Thy/thy_info.ML	Thu Dec 28 23:39:02 2017 +0100
     6.2 +++ b/src/Pure/Thy/thy_info.ML	Fri Dec 29 17:40:57 2017 +0100
     6.3 @@ -16,6 +16,7 @@
     6.4    val use_theories:
     6.5      {document: bool,
     6.6       symbols: HTML.symbols,
     6.7 +     bibtex_entries: string list,
     6.8       last_timing: Toplevel.transition -> Time.time,
     6.9       qualifier: string,
    6.10       master_dir: Path.T} -> (string * Position.T) list -> unit
    6.11 @@ -242,7 +243,8 @@
    6.12      val thy = Toplevel.end_theory end_pos end_state;
    6.13    in (results, thy) end;
    6.14  
    6.15 -fun eval_thy document symbols last_timing update_time master_dir header text_pos text parents =
    6.16 +fun eval_thy {document, symbols, bibtex_entries, last_timing} update_time master_dir header
    6.17 +    text_pos text parents =
    6.18    let
    6.19      val (name, _) = #name header;
    6.20      val keywords =
    6.21 @@ -255,7 +257,7 @@
    6.22  
    6.23      fun init () =
    6.24        Resources.begin_theory master_dir header parents
    6.25 -      |> Present.begin_theory update_time
    6.26 +      |> Present.begin_theory bibtex_entries update_time
    6.27          (fn () => implode (map (HTML.present_span symbols keywords) spans));
    6.28  
    6.29      val (results, thy) =
    6.30 @@ -282,8 +284,7 @@
    6.31  fun required_by _ [] = ""
    6.32    | required_by s initiators = s ^ "(required by " ^ show_path (rev initiators) ^ ")";
    6.33  
    6.34 -fun load_thy document symbols last_timing
    6.35 -    initiators update_time deps text (name, pos) keywords parents =
    6.36 +fun load_thy context initiators update_time deps text (name, pos) keywords parents =
    6.37    let
    6.38      val _ = remove_thy name;
    6.39      val _ = writeln ("Loading theory " ^ quote name ^ required_by " " initiators);
    6.40 @@ -304,7 +305,7 @@
    6.41  
    6.42      val text_pos = Position.put_id (Document_ID.print exec_id) (Path.position thy_path);
    6.43      val (theory, present, weight) =
    6.44 -      eval_thy document symbols last_timing update_time dir header text_pos text
    6.45 +      eval_thy context update_time dir header text_pos text
    6.46          (if name = Context.PureN then [Context.the_global_context ()] else parents);
    6.47  
    6.48      val timing_result = Timing.result timing_start;
    6.49 @@ -336,10 +337,9 @@
    6.50  
    6.51  in
    6.52  
    6.53 -fun require_thys document symbols last_timing initiators qualifier dir strs tasks =
    6.54 -      fold_map (require_thy document symbols last_timing initiators qualifier dir) strs tasks
    6.55 -      |>> forall I
    6.56 -and require_thy document symbols last_timing initiators qualifier dir (s, require_pos) tasks =
    6.57 +fun require_thys context initiators qualifier dir strs tasks =
    6.58 +      fold_map (require_thy context initiators qualifier dir) strs tasks |>> forall I
    6.59 +and require_thy context initiators qualifier dir (s, require_pos) tasks =
    6.60    let
    6.61      val {master_dir, theory_name, ...} = Resources.import_name qualifier dir s;
    6.62    in
    6.63 @@ -360,8 +360,7 @@
    6.64  
    6.65            val parents = map (#theory_name o Resources.import_name qualifier' dir' o #1) imports;
    6.66            val (parents_current, tasks') =
    6.67 -            require_thys document symbols last_timing (theory_name :: initiators)
    6.68 -              qualifier' dir' imports tasks;
    6.69 +            require_thys context (theory_name :: initiators) qualifier' dir' imports tasks;
    6.70  
    6.71            val all_current = current andalso parents_current;
    6.72            val task =
    6.73 @@ -373,8 +372,8 @@
    6.74                    let
    6.75                      val update_time = serial ();
    6.76                      val load =
    6.77 -                      load_thy document symbols last_timing initiators update_time dep
    6.78 -                        text (theory_name, theory_pos) keywords;
    6.79 +                      load_thy context initiators update_time
    6.80 +                        dep text (theory_name, theory_pos) keywords;
    6.81                    in Task (parents, load) end);
    6.82  
    6.83            val tasks'' = new_entry theory_name parents task tasks';
    6.84 @@ -386,16 +385,19 @@
    6.85  
    6.86  (* use theories *)
    6.87  
    6.88 -fun use_theories {document, symbols, last_timing, qualifier, master_dir} imports =
    6.89 +fun use_theories {document, symbols, bibtex_entries, last_timing, qualifier, master_dir} imports =
    6.90    let
    6.91 -    val (_, tasks) =
    6.92 -      require_thys document symbols last_timing [] qualifier master_dir imports String_Graph.empty;
    6.93 +    val context =
    6.94 +      {document = document, symbols = symbols, bibtex_entries = bibtex_entries,
    6.95 +        last_timing = last_timing};
    6.96 +    val (_, tasks) = require_thys context [] qualifier master_dir imports String_Graph.empty;
    6.97    in if Multithreading.enabled () then schedule_futures tasks else schedule_seq tasks end;
    6.98  
    6.99  fun use_thy name =
   6.100    use_theories
   6.101 -    {document = false, symbols = HTML.no_symbols, last_timing = K Time.zeroTime,
   6.102 -     qualifier = Resources.default_qualifier, master_dir = Path.current}
   6.103 +    {document = false, symbols = HTML.no_symbols, bibtex_entries = [],
   6.104 +      last_timing = K Time.zeroTime, qualifier = Resources.default_qualifier,
   6.105 +      master_dir = Path.current}
   6.106      [(name, Position.none)];
   6.107  
   6.108  
     7.1 --- a/src/Pure/Tools/build.ML	Thu Dec 28 23:39:02 2017 +0100
     7.2 +++ b/src/Pure/Tools/build.ML	Fri Dec 29 17:40:57 2017 +0100
     7.3 @@ -103,7 +103,7 @@
     7.4  
     7.5  (* build theories *)
     7.6  
     7.7 -fun build_theories symbols last_timing qualifier master_dir (options, thys) =
     7.8 +fun build_theories symbols bibtex_entries last_timing qualifier master_dir (options, thys) =
     7.9    let
    7.10      val condition = space_explode "," (Options.string options "condition");
    7.11      val conds = filter_out (can getenv_strict) condition;
    7.12 @@ -116,6 +116,7 @@
    7.13          (Thy_Info.use_theories {
    7.14            document = Present.document_enabled (Options.string options "document"),
    7.15            symbols = symbols,
    7.16 +          bibtex_entries = bibtex_entries,
    7.17            last_timing = last_timing,
    7.18            qualifier = qualifier,
    7.19            master_dir = master_dir}
    7.20 @@ -151,7 +152,8 @@
    7.21    sessions: string list,
    7.22    global_theories: (string * string) list,
    7.23    loaded_theories: string list,
    7.24 -  known_theories: (string * string) list};
    7.25 +  known_theories: (string * string) list,
    7.26 +  bibtex_entries: string list};
    7.27  
    7.28  fun decode_args yxml =
    7.29    let
    7.30 @@ -159,13 +161,14 @@
    7.31      val position = Position.of_properties o properties;
    7.32      val (symbol_codes, (command_timings, (do_output, (verbose, (browser_info,
    7.33        (document_files, (graph_file, (parent_name, (chapter, (name, (master_dir,
    7.34 -      (theories, (sessions, (global_theories, (loaded_theories, known_theories))))))))))))))) =
    7.35 +      (theories, (sessions, (global_theories, (loaded_theories,
    7.36 +      (known_theories, bibtex_entries)))))))))))))))) =
    7.37        pair (list (pair string int)) (pair (list properties) (pair bool (pair bool (pair string
    7.38          (pair (list (pair string string)) (pair string (pair string (pair string (pair string
    7.39            (pair string
    7.40              (pair (((list (pair Options.decode (list (pair string position))))))
    7.41 -              (pair (list string) (pair (list (pair string string))
    7.42 -                (pair (list string) (list (pair string string))))))))))))))))
    7.43 +              (pair (list string) (pair (list (pair string string)) (pair (list string)
    7.44 +                (pair (list (pair string string)) (list string))))))))))))))))
    7.45        (YXML.parse_body yxml);
    7.46    in
    7.47      Args {symbol_codes = symbol_codes, command_timings = command_timings, do_output = do_output,
    7.48 @@ -174,12 +177,12 @@
    7.49        graph_file = Path.explode graph_file, parent_name = parent_name, chapter = chapter,
    7.50        name = name, master_dir = Path.explode master_dir, theories = theories, sessions = sessions,
    7.51        global_theories = global_theories, loaded_theories = loaded_theories,
    7.52 -      known_theories = known_theories}
    7.53 +      known_theories = known_theories, bibtex_entries = bibtex_entries}
    7.54    end;
    7.55  
    7.56  fun build_session (Args {symbol_codes, command_timings, do_output, verbose, browser_info,
    7.57      document_files, graph_file, parent_name, chapter, name, master_dir, theories, sessions,
    7.58 -    global_theories, loaded_theories, known_theories}) =
    7.59 +    global_theories, loaded_theories, known_theories, bibtex_entries}) =
    7.60    let
    7.61      val symbols = HTML.make_symbols symbol_codes;
    7.62  
    7.63 @@ -209,7 +212,7 @@
    7.64  
    7.65      val res1 =
    7.66        theories |>
    7.67 -        (List.app (build_theories symbols last_timing name master_dir)
    7.68 +        (List.app (build_theories symbols bibtex_entries last_timing name master_dir)
    7.69            |> session_timing name verbose
    7.70            |> Exn.capture);
    7.71      val res2 = Exn.capture Session.finish ();
     8.1 --- a/src/Pure/Tools/build.scala	Thu Dec 28 23:39:02 2017 +0100
     8.2 +++ b/src/Pure/Tools/build.scala	Fri Dec 29 17:40:57 2017 +0100
     8.3 @@ -213,13 +213,15 @@
     8.4                  pair(string, pair(string, pair(string, pair(Path.encode,
     8.5                  pair(list(pair(Options.encode, list(pair(string, properties)))),
     8.6                  pair(list(string), pair(list(pair(string, string)), pair(list(string),
     8.7 -                list(pair(string, string)))))))))))))))))(
     8.8 +                pair(list(pair(string, string)), list(string)))))))))))))))))(
     8.9                (Symbol.codes, (command_timings, (do_output, (verbose,
    8.10                  (store.browser_info, (info.document_files, (File.standard_path(graph_file),
    8.11                  (parent, (info.chapter, (name, (Path.current,
    8.12                  (info.theories, (base.known.sessions.toList,
    8.13 -                (base.global_theories.toList, (base.loaded_theories.keys,
    8.14 -                base.dest_known_theories))))))))))))))))
    8.15 +                (base.global_theories.toList,
    8.16 +                (base.loaded_theories.keys,
    8.17 +                (base.dest_known_theories,
    8.18 +                info.bibtex_entries.map(_.info))))))))))))))))))
    8.19              })
    8.20  
    8.21          val env =