# HG changeset patch # User wenzelm # Date 1605475573 -3600 # Node ID b519d819d376e7011caa9c9efd1edc354984379a # Parent c7bc3e70a8c77dc7773140b2161b8a0bb2582898# Parent 5fc193537b7c6d78e531e909951e2eb625471946 merged diff -r c7bc3e70a8c7 -r b519d819d376 src/Pure/ML/ml_process.scala --- a/src/Pure/ML/ml_process.scala Sun Nov 15 10:13:03 2020 +0000 +++ b/src/Pure/ML/ml_process.scala Sun Nov 15 22:26:13 2020 +0100 @@ -78,27 +78,36 @@ val eval_options = if (heaps.isEmpty) Nil else List("Options.load_default ()") // session base - val eval_session_base = + val init_session = Isabelle_System.tmp_file("init_session", ext = "ML") + val init_session_name = init_session.getAbsolutePath + Isabelle_System.chmod("600", File.path(init_session)) + File.write(init_session, session_base match { - case None => Nil + case None => "" case Some(base) => - def print_table(table: List[(String, String)]): String = + def print_table: List[(String, String)] => String = ML_Syntax.print_list( ML_Syntax.print_pair( - ML_Syntax.print_string_bytes, ML_Syntax.print_string_bytes))(table) - def print_list(list: List[String]): String = - ML_Syntax.print_list(ML_Syntax.print_string_bytes)(list) - def print_sessions(list: List[(String, Position.T)]): String = + ML_Syntax.print_string_bytes, ML_Syntax.print_string_bytes)) + def print_list: List[String] => String = + ML_Syntax.print_list(ML_Syntax.print_string_bytes) + def print_sessions: List[(String, Position.T)] => String = ML_Syntax.print_list( - ML_Syntax.print_pair(ML_Syntax.print_string_bytes, ML_Syntax.print_properties))(list) + ML_Syntax.print_pair(ML_Syntax.print_string_bytes, ML_Syntax.print_properties)) + def print_bibtex_entries: List[(String, List[String])] => String = + ML_Syntax.print_list( + ML_Syntax.print_pair(ML_Syntax.print_string_bytes, + ML_Syntax.print_list(ML_Syntax.print_string_bytes))) - List("Resources.init_session" + + "Resources.init_session" + "{session_positions = " + print_sessions(sessions_structure.session_positions) + ", session_directories = " + print_table(sessions_structure.dest_session_directories) + + ", session_chapters = " + print_table(sessions_structure.session_chapters) + + ", bibtex_entries = " + print_bibtex_entries(sessions_structure.bibtex_entries) + ", docs = " + print_list(base.doc_names) + ", global_theories = " + print_table(base.global_theories.toList) + - ", loaded_theories = " + print_list(base.loaded_theories.keys) + "}") - } + ", loaded_theories = " + print_list(base.loaded_theories.keys) + "}" + }) // process val eval_process = @@ -131,7 +140,9 @@ // bash val bash_args = ml_runtime_options ::: - (eval_init ::: eval_modes ::: eval_options ::: eval_session_base).flatMap(List("--eval", _)) ::: + (eval_init ::: eval_modes ::: eval_options).flatMap(List("--eval", _)) ::: + List("--use", init_session_name, + "--eval", "OS.FileSys.remove " + ML_Syntax.print_string_bytes(init_session_name)) ::: use_prelude.flatMap(List("--use", _)) ::: List("--eval", eval_process) ::: args Bash.process( @@ -143,6 +154,7 @@ cleanup = () => { isabelle_process_options.delete + init_session.delete Isabelle_System.rm_tree(isabelle_tmp) cleanup() }) diff -r c7bc3e70a8c7 -r b519d819d376 src/Pure/PIDE/protocol.ML --- a/src/Pure/PIDE/protocol.ML Sun Nov 15 10:13:03 2020 +0000 +++ b/src/Pure/PIDE/protocol.ML Sun Nov 15 22:26:13 2020 +0100 @@ -25,17 +25,21 @@ val _ = Isabelle_Process.protocol_command "Prover.init_session" - (fn [session_positions_yxml, session_directories_yxml, doc_names_yxml, global_theories_yxml, - loaded_theories_yxml] => + (fn [session_positions_yxml, session_directories_yxml, session_chapters_yxml, + bibtex_entries_yxml, doc_names_yxml, global_theories_yxml, loaded_theories_yxml] => let val decode_table = YXML.parse_body #> let open XML.Decode in list (pair string string) end; val decode_list = YXML.parse_body #> let open XML.Decode in list string end; val decode_sessions = YXML.parse_body #> let open XML.Decode in list (pair string properties) end; + val decode_bibtex_entries = + YXML.parse_body #> let open XML.Decode in list (pair string (list string)) end; in Resources.init_session {session_positions = decode_sessions session_positions_yxml, session_directories = decode_table session_directories_yxml, + session_chapters = decode_table session_chapters_yxml, + bibtex_entries = decode_bibtex_entries bibtex_entries_yxml, docs = decode_list doc_names_yxml, global_theories = decode_table global_theories_yxml, loaded_theories = decode_list loaded_theories_yxml} diff -r c7bc3e70a8c7 -r b519d819d376 src/Pure/PIDE/protocol.scala --- a/src/Pure/PIDE/protocol.scala Sun Nov 15 10:13:03 2020 +0000 +++ b/src/Pure/PIDE/protocol.scala Sun Nov 15 22:26:13 2020 +0100 @@ -285,29 +285,24 @@ /* session base */ - private def encode_table(table: List[(String, String)]): String = - { - import XML.Encode._ - Symbol.encode_yxml(list(pair(string, string))(table)) - } - - private def encode_list(lst: List[String]): String = + def init_session(resources: Resources) { import XML.Encode._ - Symbol.encode_yxml(list(string)(lst)) - } - private def encode_sessions(lst: List[(String, Position.T)]): String = - { - import XML.Encode._ - Symbol.encode_yxml(list(pair(string, properties))(lst)) - } + def encode_table(arg: List[(String, String)]): String = + Symbol.encode_yxml(list(pair(string, string))(arg)) + def encode_list(arg: List[String]): String = + Symbol.encode_yxml(list(string)(arg)) + def encode_sessions(arg: List[(String, Position.T)]): String = + Symbol.encode_yxml(list(pair(string, properties))(arg)) + def encode_bibtex_entries(arg: List[(String, List[String])]): String = + Symbol.encode_yxml(list(pair(string, list(string)))(arg)) - def init_session(resources: Resources) - { protocol_command("Prover.init_session", encode_sessions(resources.sessions_structure.session_positions), encode_table(resources.sessions_structure.dest_session_directories), + encode_table(resources.sessions_structure.session_chapters), + encode_bibtex_entries(resources.sessions_structure.bibtex_entries), encode_list(resources.session_base.doc_names), encode_table(resources.session_base.global_theories.toList), encode_list(resources.session_base.loaded_theories.keys)) diff -r c7bc3e70a8c7 -r b519d819d376 src/Pure/PIDE/resources.ML --- a/src/Pure/PIDE/resources.ML Sun Nov 15 10:13:03 2020 +0000 +++ b/src/Pure/PIDE/resources.ML Sun Nov 15 22:26:13 2020 +0100 @@ -10,6 +10,8 @@ val init_session: {session_positions: (string * Properties.T) list, session_directories: (string * string) list, + session_chapters: (string * string) list, + bibtex_entries: (string * string list) list, docs: string list, global_theories: (string * string) list, loaded_theories: string list} -> unit @@ -17,12 +19,14 @@ val global_theory: string -> string option val loaded_theory: string -> bool val check_session: Proof.context -> string * Position.T -> string + val session_chapter: string -> string val check_doc: Proof.context -> string * Position.T -> string val master_directory: theory -> Path.T val imports_of: theory -> (string * Position.T) list 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} @@ -54,6 +58,8 @@ val empty_session_base = {session_positions = []: (string * entry) list, session_directories = Symtab.empty: Path.T list Symtab.table, + session_chapters = Symtab.empty: string Symtab.table, + bibtex_entries = Symtab.empty: string list Symtab.table, docs = []: (string * entry) list, global_theories = Symtab.empty: string Symtab.table, loaded_theories = Symtab.empty: unit Symtab.table}; @@ -62,13 +68,16 @@ Synchronized.var "Sessions.base" empty_session_base; fun init_session - {session_positions, session_directories, docs, global_theories, loaded_theories} = + {session_positions, session_directories, session_chapters, + bibtex_entries, docs, global_theories, loaded_theories} = Synchronized.change global_session_base (fn _ => {session_positions = sort_by #1 (map (apsnd make_entry) session_positions), session_directories = fold_rev (fn (dir, name) => Symtab.cons_list (name, Path.explode dir)) session_directories Symtab.empty, + session_chapters = Symtab.make session_chapters, + bibtex_entries = Symtab.make bibtex_entries, docs = sort_by #1 (map (apsnd make_entry o rpair []) docs), global_theories = Symtab.make global_theories, loaded_theories = Symtab.make_set loaded_theories}); @@ -78,6 +87,8 @@ (fn {global_theories, loaded_theories, ...} => {session_positions = [], session_directories = Symtab.empty, + session_chapters = Symtab.empty, + bibtex_entries = Symtab.empty, docs = [], global_theories = global_theories, loaded_theories = loaded_theories}); @@ -97,6 +108,9 @@ Markup.entity Markup.sessionN name |> Markup.properties (Position.entity_properties_of false serial pos)); +fun session_chapter name = + the_default "Unsorted" (Symtab.lookup (get_session_base #session_chapters) name); + val check_doc = check_name #docs "documentation" (Markup.doc o #1); @@ -148,6 +162,9 @@ then theory else Long_Name.qualify qualifier theory; +fun theory_bibtex_entries theory = + Symtab.lookup_list (get_session_base #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 c7bc3e70a8c7 -r b519d819d376 src/Pure/Thy/bibtex.ML --- a/src/Pure/Thy/bibtex.ML Sun Nov 15 10:13:03 2020 +0000 +++ b/src/Pure/Thy/bibtex.ML Sun Nov 15 22:26:13 2020 +0100 @@ -47,7 +47,7 @@ (fn ctxt => fn (opt, citations) => let val thy = Proof_Context.theory_of ctxt; - val bibtex_entries = Present.get_bibtex_entries thy; + val bibtex_entries = Resources.theory_bibtex_entries (Context.theory_long_name thy); val _ = if null bibtex_entries andalso Context.theory_name thy <> Context.PureN then () else diff -r c7bc3e70a8c7 -r b519d819d376 src/Pure/Thy/present.ML --- a/src/Pure/Thy/present.ML Sun Nov 15 10:13:03 2020 +0000 +++ b/src/Pure/Thy/present.ML Sun Nov 15 22:26:13 2020 +0100 @@ -6,12 +6,9 @@ signature PRESENT = sig - val tex_path: string -> Path.T - val get_bibtex_entries: theory -> string list - val theory_qualifier: theory -> string val init: HTML.symbols -> bool -> Path.T -> string list -> string * string -> bool -> unit val finish: unit -> unit - val begin_theory: string list -> int -> (unit -> HTML.text) -> theory -> theory + val begin_theory: int -> (unit -> HTML.text) -> theory -> theory end; structure Present: PRESENT = @@ -20,8 +17,6 @@ (** paths **) -val tex_ext = Path.ext "tex"; -val tex_path = tex_ext o Path.basic; val html_ext = Path.ext "html"; val html_path = html_ext o Path.basic; val index_path = Path.basic "index.html"; @@ -33,32 +28,6 @@ -(** theory data **) - -type browser_info = {chapter: string, name: string, bibtex_entries: string list}; -val empty_browser_info: browser_info = {chapter = "Unsorted", name = "Unknown", bibtex_entries = []}; - -structure Browser_Info = Theory_Data -( - type T = browser_info - val empty = empty_browser_info; - val extend = I; - val merge = #1; -); - -fun reset_browser_info thy = - if Browser_Info.get thy = empty_browser_info then NONE - else SOME (Browser_Info.put empty_browser_info thy); - -val _ = - Theory.setup - (Theory.at_begin reset_browser_info #> - 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 **) (* type browser_info *) @@ -168,7 +137,8 @@ fun theory_link (curr_chapter, curr_session) thy = let - val {chapter, name = session, ...} = Browser_Info.get thy; + val session = Resources.theory_qualifier (Context.theory_long_name thy); + val chapter = Resources.session_chapter session; val link = html_path (Context.theory_name thy); in if curr_session = session then SOME link @@ -178,7 +148,7 @@ else SOME (Path.parent + Path.parent + Path.basic chapter + Path.basic session + link) end; -fun begin_theory bibtex_entries update_time mk_text thy = +fun begin_theory update_time mk_text thy = with_session_info thy (fn {symbols, name = session_name, chapter, ...} => let val name = Context.theory_name thy; @@ -190,14 +160,10 @@ val _ = update_html name (HTML.theory symbols name parent_specs (mk_text ())); - val bibtex_entries' = + val _ = if is_session_theory thy then - (add_html_index (update_time, HTML.theory_entry symbols (Url.File (html_path name), name)); - bibtex_entries) - else []; - in - thy - |> Browser_Info.put {chapter = chapter, name = session_name, bibtex_entries = bibtex_entries'} - end); + add_html_index (update_time, HTML.theory_entry symbols (Url.File (html_path name), name)) + else (); + in thy end); end; diff -r c7bc3e70a8c7 -r b519d819d376 src/Pure/Thy/sessions.scala --- a/src/Pure/Thy/sessions.scala Sun Nov 15 10:13:03 2020 +0000 +++ b/src/Pure/Thy/sessions.scala Sun Nov 15 22:26:13 2020 +0100 @@ -511,7 +511,7 @@ case s => Some(dir + Path.explode(s)) } - def bibtex_entries: List[Text.Info[String]] = + lazy val bibtex_entries: List[Text.Info[String]] = (for { (document_dir, file) <- document_files.iterator if Bibtex.is_bibtex(file.file_name) @@ -804,6 +804,16 @@ def imports_requirements(ss: List[String]): List[String] = imports_graph.all_preds_rev(ss) def imports_topological_order: List[String] = imports_graph.topological_order + def bibtex_entries: List[(String, List[String])] = + build_topological_order.flatMap(name => + apply(name).bibtex_entries match { + case Nil => None + case entries => Some(name -> entries.map(_.info)) + }) + + def session_chapters: List[(String, String)] = + build_topological_order.map(name => name -> apply(name).chapter) + override def toString: String = imports_graph.keys_iterator.mkString("Sessions.Structure(", ", ", ")") } diff -r c7bc3e70a8c7 -r b519d819d376 src/Pure/Thy/thy_info.ML --- a/src/Pure/Thy/thy_info.ML Sun Nov 15 10:13:03 2020 +0000 +++ b/src/Pure/Thy/thy_info.ML Sun Nov 15 22:26:13 2020 +0100 @@ -21,7 +21,6 @@ type context = {options: Options.T, symbols: HTML.symbols, - bibtex_entries: string list, last_timing: Toplevel.transition -> Time.time} val use_theories: context -> string -> Path.T -> (string * Position.T) list -> unit val use_thy: string -> unit @@ -66,11 +65,10 @@ else let val thy_name = Context.theory_name thy; - val document_path = Path.basic "document" + Present.tex_path thy_name; - + val document_tex_name = Path.explode_binding0 ("document/" ^ thy_name ^ ".tex"); val latex = Latex.isabelle_body thy_name body; val output = [Latex.output_text latex, Latex.output_positions file_pos latex]; - in Export.export thy (Path.binding0 document_path) (XML.blob output) end + in Export.export thy document_tex_name (XML.blob output) end end)); @@ -188,13 +186,11 @@ type context = {options: Options.T, symbols: HTML.symbols, - bibtex_entries: string list, last_timing: Toplevel.transition -> Time.time}; fun default_context (): context = {options = Options.default (), symbols = HTML.no_symbols, - bibtex_entries = [], last_timing = K Time.zeroTime}; @@ -304,7 +300,7 @@ fun eval_thy (context: context) update_time master_dir header text_pos text parents = let - val {options, symbols, bibtex_entries, last_timing} = context; + val {options, symbols, last_timing} = context; val (name, _) = #name header; val keywords = fold (curry Keyword.merge_keywords o Thy_Header.get_keywords) parents @@ -315,7 +311,7 @@ fun init () = Resources.begin_theory master_dir header parents - |> Present.begin_theory bibtex_entries update_time + |> Present.begin_theory update_time (fn () => implode (map (HTML.present_span symbols keywords) spans)); val (results, thy) = diff -r c7bc3e70a8c7 -r b519d819d376 src/Pure/Tools/build.ML --- a/src/Pure/Tools/build.ML Sun Nov 15 10:13:03 2020 +0000 +++ b/src/Pure/Tools/build.ML Sun Nov 15 22:26:13 2020 +0100 @@ -55,11 +55,10 @@ (* build theories *) -fun build_theories symbols bibtex_entries last_timing qualifier master_dir (options, thys) = +fun build_theories symbols last_timing qualifier master_dir (options, thys) = let val context = - {options = options, symbols = symbols, bibtex_entries = bibtex_entries, - last_timing = last_timing}; + {options = options, symbols = symbols, last_timing = last_timing}; val condition = space_explode "," (Options.string options "condition"); val conds = filter_out (can getenv_strict) condition; in @@ -90,8 +89,8 @@ let val (symbol_codes, (command_timings, (verbose, (browser_info, (documents, (parent_name, (chapter, (session_name, (master_dir, - (theories, (session_positions, (session_directories, (doc_names, (global_theories, - (loaded_theories, bibtex_entries))))))))))))))) = + (theories, (session_positions, (session_directories, (session_chapters, + (doc_names, (global_theories, (loaded_theories, bibtex_entries)))))))))))))))) = YXML.parse_body args_yxml |> let open XML.Decode; @@ -103,8 +102,10 @@ (pair path (pair (((list (pair Options.decode (list (pair string position)))))) (pair (list (pair string properties)) - (pair (list (pair string string)) (pair (list string) - (pair (list (pair string string)) (pair (list string) (list string))))))))))))))) + (pair (list (pair string string)) + (pair (list (pair string string)) (pair (list string) + (pair (list (pair string string)) (pair (list string) + (list (pair string (list string)))))))))))))))))) end; val symbols = HTML.make_symbols symbol_codes; @@ -115,6 +116,8 @@ Resources.init_session {session_positions = session_positions, session_directories = session_directories, + session_chapters = session_chapters, + bibtex_entries = bibtex_entries, docs = doc_names, global_theories = global_theories, loaded_theories = loaded_theories}; @@ -133,8 +136,7 @@ val res1 = theories |> - (List.app - (build_theories symbols bibtex_entries last_timing session_name master_dir) + (List.app (build_theories symbols last_timing session_name master_dir) |> session_timing |> Exn.capture); val res2 = Exn.capture Session.finish (); diff -r c7bc3e70a8c7 -r b519d819d376 src/Pure/Tools/build.scala --- a/src/Pure/Tools/build.scala Sun Nov 15 10:13:03 2020 +0000 +++ b/src/Pure/Tools/build.scala Sun Nov 15 22:26:13 2020 +0100 @@ -180,15 +180,18 @@ pair(list(pair(Options.encode, list(pair(string, properties)))), pair(list(pair(string, properties)), pair(list(pair(string, string)), - pair(list(string), pair(list(pair(string, string)), - pair(list(string), list(string))))))))))))))))( + pair(list(pair(string, string)), + pair(list(string), + pair(list(pair(string, string)), + pair(list(string), list(pair(string, list(string)))))))))))))))))))( (Symbol.codes, (command_timings0, (verbose, (store.browser_info, (documents, (parent, (info.chapter, (session_name, (Path.current, (info.theories, (sessions_structure.session_positions, (sessions_structure.dest_session_directories, + (sessions_structure.session_chapters, (base.doc_names, (base.global_theories.toList, - (base.loaded_theories.keys, info.bibtex_entries.map(_.info))))))))))))))))) + (base.loaded_theories.keys, sessions_structure.bibtex_entries))))))))))))))))) }) val env =