--- 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) +
--- 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,
--- 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),
--- 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);
--- 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;
--- 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(", ", ", ")")
}
--- 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,
--- 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 =