# HG changeset patch # User wenzelm # Date 1605474045 -3600 # Node ID 217e6cf61453a1aaa71ad051fbfbaad82c8e7853 # Parent f827c3bb6b7f70ad6c438bc1131bc4929d595694 refer to session structure from resources; diff -r f827c3bb6b7f -r 217e6cf61453 src/Pure/ML/ml_process.scala --- a/src/Pure/ML/ml_process.scala Sun Nov 15 18:16:20 2020 +0100 +++ b/src/Pure/ML/ml_process.scala Sun Nov 15 22:00:45 2020 +0100 @@ -102,6 +102,7 @@ "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) + diff -r f827c3bb6b7f -r 217e6cf61453 src/Pure/PIDE/protocol.ML --- a/src/Pure/PIDE/protocol.ML Sun Nov 15 18:16:20 2020 +0100 +++ b/src/Pure/PIDE/protocol.ML Sun Nov 15 22:00:45 2020 +0100 @@ -25,8 +25,8 @@ val _ = Isabelle_Process.protocol_command "Prover.init_session" - (fn [session_positions_yxml, session_directories_yxml, bibtex_entries_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; @@ -38,6 +38,7 @@ 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, diff -r f827c3bb6b7f -r 217e6cf61453 src/Pure/PIDE/protocol.scala --- a/src/Pure/PIDE/protocol.scala Sun Nov 15 18:16:20 2020 +0100 +++ b/src/Pure/PIDE/protocol.scala Sun Nov 15 22:00:45 2020 +0100 @@ -301,6 +301,7 @@ 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), diff -r f827c3bb6b7f -r 217e6cf61453 src/Pure/PIDE/resources.ML --- a/src/Pure/PIDE/resources.ML Sun Nov 15 18:16:20 2020 +0100 +++ b/src/Pure/PIDE/resources.ML Sun Nov 15 22:00:45 2020 +0100 @@ -10,6 +10,7 @@ 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, @@ -18,6 +19,7 @@ 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 @@ -56,6 +58,7 @@ 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, @@ -65,14 +68,15 @@ Synchronized.var "Sessions.base" empty_session_base; fun init_session - {session_positions, session_directories, bibtex_entries, 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, @@ -83,6 +87,7 @@ (fn {global_theories, loaded_theories, ...} => {session_positions = [], session_directories = Symtab.empty, + session_chapters = Symtab.empty, bibtex_entries = Symtab.empty, docs = [], global_theories = global_theories, @@ -103,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); diff -r f827c3bb6b7f -r 217e6cf61453 src/Pure/Thy/present.ML --- a/src/Pure/Thy/present.ML Sun Nov 15 18:16:20 2020 +0100 +++ b/src/Pure/Thy/present.ML Sun Nov 15 22:00:45 2020 +0100 @@ -6,7 +6,6 @@ signature PRESENT = sig - 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: int -> (unit -> HTML.text) -> theory -> theory @@ -29,30 +28,6 @@ -(** theory data **) - -type browser_info = {chapter: string, name: string}; -val empty_browser_info: browser_info = {chapter = "Unsorted", name = "Unknown"}; - -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}); - - - (** global browser info state **) (* type browser_info *) @@ -162,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 @@ -188,6 +164,6 @@ if is_session_theory thy then add_html_index (update_time, HTML.theory_entry symbols (Url.File (html_path name), name)) else (); - in thy |> Browser_Info.put {chapter = chapter, name = session_name} end); + in thy end); end; diff -r f827c3bb6b7f -r 217e6cf61453 src/Pure/Thy/sessions.scala --- a/src/Pure/Thy/sessions.scala Sun Nov 15 18:16:20 2020 +0100 +++ b/src/Pure/Thy/sessions.scala Sun Nov 15 22:00:45 2020 +0100 @@ -811,6 +811,9 @@ 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 f827c3bb6b7f -r 217e6cf61453 src/Pure/Tools/build.ML --- a/src/Pure/Tools/build.ML Sun Nov 15 18:16:20 2020 +0100 +++ b/src/Pure/Tools/build.ML Sun Nov 15 22:00:45 2020 +0100 @@ -89,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; @@ -102,9 +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 (pair string string)) (pair (list string) - (list (pair string (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,7 @@ 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, diff -r f827c3bb6b7f -r 217e6cf61453 src/Pure/Tools/build.scala --- a/src/Pure/Tools/build.scala Sun Nov 15 18:16:20 2020 +0100 +++ b/src/Pure/Tools/build.scala Sun Nov 15 22:00:45 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(pair(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, sessions_structure.bibtex_entries)))))))))))))))) + (base.loaded_theories.keys, sessions_structure.bibtex_entries))))))))))))))))) }) val env =