--- 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);