# HG changeset patch # User wenzelm # Date 1674240772 -3600 # Node ID f5896dea6fceff30c05a65db63e12c084eb1d5cb # Parent ac7af931189f43af2ef177a5900f85b290b06ad2 more direct check of bibtex entries via Isabelle/Scala; diff -r ac7af931189f -r f5896dea6fce src/Pure/PIDE/markup.ML --- a/src/Pure/PIDE/markup.ML Fri Jan 20 16:30:09 2023 +0100 +++ b/src/Pure/PIDE/markup.ML Fri Jan 20 19:52:52 2023 +0100 @@ -86,6 +86,7 @@ val deleteN: string val delete: T val load_commandN: string val bash_functionN: string + val bibtex_entryN: string val scala_functionN: string val system_optionN: string val sessionN: string @@ -489,6 +490,7 @@ val load_commandN = "load_command"; val bash_functionN = "bash_function"; +val bibtex_entryN = "bibtex_entry"; val scala_functionN = "scala_function"; val system_optionN = "system_option"; diff -r ac7af931189f -r f5896dea6fce src/Pure/PIDE/resources.ML --- a/src/Pure/PIDE/resources.ML Fri Jan 20 16:30:09 2023 +0100 +++ b/src/Pure/PIDE/resources.ML Fri Jan 20 19:52:52 2023 +0100 @@ -10,7 +10,6 @@ val init_session: {session_positions: (string * Properties.T) list, session_directories: (string * string) list, - bibtex_entries: (string * string list) list, command_timings: Properties.T list, load_commands: (string * Position.T) list, scala_functions: (string * ((bool * bool) * Position.T)) list, @@ -30,7 +29,6 @@ val begin_theory: Path.T -> Thy_Header.header -> theory list -> theory val thy_path: Path.T -> Path.T val theory_qualifier: string -> string - val theory_bibtex_entries: string -> string list val find_theory_file: string -> Path.T option val import_name: string -> Path.T -> string -> {node_name: Path.T, master_dir: Path.T, theory_name: string} @@ -105,7 +103,6 @@ val empty_session_base = ({session_positions = []: (string * entry) list, session_directories = Symtab.empty: Path.T list Symtab.table, - bibtex_entries = Symtab.empty: string list Symtab.table, timings = empty_timings, load_commands = []: (string * Position.T) list, scala_functions = Symtab.empty: ((bool * bool) * Position.T) Symtab.table}, @@ -116,7 +113,7 @@ Synchronized.var "Sessions.base" empty_session_base; fun init_session - {session_positions, session_directories, bibtex_entries, command_timings, load_commands, + {session_positions, session_directories, command_timings, load_commands, scala_functions, global_theories, loaded_theories} = Synchronized.change global_session_base (fn _ => @@ -124,7 +121,6 @@ session_directories = Symtab.build (session_directories |> fold_rev (fn (dir, name) => Symtab.cons_list (name, Path.explode dir))), - bibtex_entries = Symtab.make bibtex_entries, timings = make_timings command_timings, load_commands = load_commands, scala_functions = Symtab.make scala_functions}, @@ -133,22 +129,21 @@ fun init_session_yxml yxml = let - val (session_positions, (session_directories, (bibtex_entries, (command_timings, - (load_commands, (scala_functions, (global_theories, loaded_theories))))))) = + val (session_positions, (session_directories, (command_timings, + (load_commands, (scala_functions, (global_theories, loaded_theories)))))) = YXML.parse_body_bytes yxml |> let open XML.Decode in (pair (list (pair string properties)) (pair (list (pair string string)) - (pair (list (pair string (list string))) (pair (list properties) + (pair (list properties) (pair (list (pair string properties)) (pair (list (pair string (pair (pair bool bool) properties))) - (pair (list (pair string string)) (list string)))))))) + (pair (list (pair string string)) (list string))))))) end; in init_session {session_positions = session_positions, session_directories = session_directories, - bibtex_entries = bibtex_entries, command_timings = command_timings, load_commands = (map o apsnd) Position.of_properties load_commands, scala_functions = (map o apsnd o apsnd) Position.of_properties scala_functions, @@ -268,9 +263,6 @@ if literal_theory theory then theory else Long_Name.qualify qualifier theory; -fun theory_bibtex_entries theory = - Symtab.lookup_list (get_session_base1 #bibtex_entries) (theory_qualifier theory); - fun find_theory_file thy_name = let val thy_file = thy_path (Path.basic (Long_Name.base_name thy_name)); diff -r ac7af931189f -r f5896dea6fce src/Pure/PIDE/resources.scala --- a/src/Pure/PIDE/resources.scala Fri Jan 20 16:30:09 2023 +0100 +++ b/src/Pure/PIDE/resources.scala Fri Jan 20 19:52:52 2023 +0100 @@ -43,19 +43,17 @@ YXML.string_of_body( pair(list(pair(string, properties)), pair(list(pair(string, string)), - pair(list(pair(string, list(string))), pair(list(properties), pair(list(pair(string, properties)), pair(list(Scala.encode_fun), - pair(list(pair(string, string)), list(string))))))))( + pair(list(pair(string, string)), list(string)))))))( (sessions_structure.session_positions, (sessions_structure.dest_session_directories, - (sessions_structure.bibtex_entries, (command_timings, (Command_Span.load_commands.map(cmd => (cmd.name, cmd.position)), (Scala.functions, (sessions_structure.global_theories.toList, - session_base.loaded_theories.keys))))))))) + session_base.loaded_theories.keys)))))))) } diff -r ac7af931189f -r f5896dea6fce src/Pure/System/scala.scala --- a/src/Pure/System/scala.scala Fri Jan 20 16:30:09 2023 +0100 +++ b/src/Pure/System/scala.scala Fri Jan 20 19:52:52 2023 +0100 @@ -96,19 +96,6 @@ } } - object Theory_Name extends Fun("command_theory_name") with Single_Fun { - val here = Scala_Project.here - override def invoke(session: Session, args: List[Bytes]): List[Bytes] = { - val id = Value.Long.parse(Library.the_single(args).text) - val name = - session.get_state().lookup_id(id) match { - case None => "" - case Some(st) => st.command.node_name.theory - } - List(Bytes(name)) - } - } - /** compiler **/ @@ -378,7 +365,6 @@ class Scala_Functions extends Scala.Functions( Scala.Echo, Scala.Sleep, - Scala.Theory_Name, Scala.Toplevel, Scala_Build.Scala_Fun, Base64.Decode, @@ -389,6 +375,7 @@ Compress.Zstd_Uncompress, Doc.Doc_Names, Bibtex.Check_Database, + Bibtex.Session_Entries, Isabelle_System.Make_Directory, Isabelle_System.Copy_Dir, Isabelle_System.Copy_File, diff -r ac7af931189f -r f5896dea6fce src/Pure/Thy/bibtex.ML --- a/src/Pure/Thy/bibtex.ML Fri Jan 20 16:30:09 2023 +0100 +++ b/src/Pure/Thy/bibtex.ML Fri Jan 20 19:52:52 2023 +0100 @@ -9,6 +9,7 @@ val check_database: Position.T -> string -> (string * Position.T) list * (string * Position.T) list val check_database_output: Position.T -> string -> unit + val check_bibtex_entry: Proof.context -> string * Position.T -> unit val cite_macro: string Config.T val cite_antiquotation: binding -> (Proof.context -> string) -> theory -> theory end; @@ -35,6 +36,29 @@ end; +(* check bibtex entry *) + +fun check_bibtex_entry ctxt (name, pos) = + let + fun warn () = + if Context_Position.is_visible ctxt then + warning ("Unknown session context: cannot check Bibtex entry " ^ + quote name ^ Position.here pos) + else (); + in + if name = "*" then () + else + (case Position.id_of pos of + NONE => warn () + | SOME id => + (case \<^scala>\bibtex_session_entries\ [id] of + [] => warn () + | _ :: entries => + Completion.check_entity Markup.bibtex_entryN (map (rpair Position.none) entries) + ctxt (name, pos) |> ignore)) + end; + + (* document antiquotations *) val cite_macro = Attrib.setup_config_string \<^binding>\cite_macro\ (K ""); @@ -48,19 +72,6 @@ val parse_citations = Parse.and_list1 Args.name_position; -fun command_theory_name () = - let - fun err () = error ("Cannot determine command theory name: bad PIDE id"); - val res = - (case Position.id_of (Position.thread_data ()) of - SOME id => \<^scala>\command_theory_name\ id - | NONE => err ()); - in if res = "" then err () else res end; - -fun theory_name thy = - let val name0 = Context.theory_long_name thy; - in if name0 = Context.PureN then command_theory_name () else name0 end; - fun cite_command ctxt get_kind ((opt_loc, citations), macro_name) = let val loc = the_default Input.empty opt_loc; @@ -68,15 +79,7 @@ Context_Position.reports ctxt (Document_Output.document_reports loc @ map (fn (name, pos) => (pos, Markup.citation name)) citations); - - val thy_name = theory_name (Proof_Context.theory_of ctxt); - val bibtex_entries = Resources.theory_bibtex_entries thy_name; - val _ = - if null bibtex_entries andalso thy_name <> Context.PureN then () - else - citations |> List.app (fn (name, pos) => - if member (op =) bibtex_entries name orelse name = "*" then () - else error ("Unknown Bibtex entry " ^ quote name ^ Position.here pos)); + val _ = List.app (check_bibtex_entry ctxt) citations; val kind = if macro_name = "" then get_kind ctxt else macro_name; val location = Document_Output.output_document ctxt {markdown = false} loc; diff -r ac7af931189f -r f5896dea6fce src/Pure/Thy/bibtex.scala --- a/src/Pure/Thy/bibtex.scala Fri Jan 20 16:30:09 2023 +0100 +++ b/src/Pure/Thy/bibtex.scala Fri Jan 20 19:52:52 2023 +0100 @@ -210,6 +210,24 @@ new Entries(entries ::: other.entries, errors ::: other.errors) } + object Session_Entries extends Scala.Fun("bibtex_session_entries") { + val here = Scala_Project.here + + override def invoke(session: Session, args: List[Bytes]): List[Bytes] = { + val sessions = session.resources.sessions_structure + val id = Value.Long.parse(Library.the_single(args).text) + val qualifier = + session.get_state().lookup_id(id) match { + case None => Sessions.DRAFT + case Some(st) => sessions.theory_qualifier(st.command.node_name.theory) + } + val res = + if (qualifier == Sessions.DRAFT || !sessions.defined(qualifier)) Nil + else qualifier :: sessions(qualifier).bibtex_entries.entries.map(_.info) + res.map(Bytes.apply) + } + } + /* completion */