--- a/src/Pure/PIDE/resources.ML Sat Nov 28 16:25:29 2020 +0100
+++ b/src/Pure/PIDE/resources.ML Sat Nov 28 17:38:03 2020 +0100
@@ -13,7 +13,6 @@
session_chapters: (string * string) list,
bibtex_entries: (string * string list) list,
command_timings: Properties.T list,
- docs: string list,
scala_functions: (string * Position.T) list,
global_theories: (string * string) list,
loaded_theories: string list} -> unit
@@ -25,7 +24,6 @@
val check_session: Proof.context -> string * Position.T -> string
val session_chapter: string -> string
val last_timing: Toplevel.transition -> Time.time
- val check_doc: Proof.context -> string * Position.T -> string
val scala_function_pos: string -> Position.T
val master_directory: theory -> Path.T
val imports_of: theory -> (string * Position.T) list
@@ -104,7 +102,6 @@
session_chapters = Symtab.empty: string Symtab.table,
bibtex_entries = Symtab.empty: string list Symtab.table,
timings = empty_timings,
- docs = []: (string * entry) list,
scala_functions = Symtab.empty: Position.T Symtab.table},
{global_theories = Symtab.empty: string Symtab.table,
loaded_theories = Symtab.empty: unit Symtab.table});
@@ -114,7 +111,7 @@
fun init_session
{session_positions, session_directories, session_chapters, bibtex_entries,
- command_timings, docs, scala_functions, global_theories, loaded_theories} =
+ command_timings, scala_functions, global_theories, loaded_theories} =
Synchronized.change global_session_base
(fn _ =>
({session_positions = sort_by #1 (map (apsnd make_entry) session_positions),
@@ -124,7 +121,6 @@
session_chapters = Symtab.make session_chapters,
bibtex_entries = Symtab.make bibtex_entries,
timings = make_timings command_timings,
- docs = sort_by #1 (map (apsnd make_entry o rpair []) docs),
scala_functions = Symtab.make scala_functions},
{global_theories = Symtab.make global_theories,
loaded_theories = Symtab.make_set loaded_theories}));
@@ -132,15 +128,14 @@
fun init_session_yxml yxml =
let
val (session_positions, (session_directories, (session_chapters, (bibtex_entries,
- (command_timings, (docs, (scala_functions, (global_theories, loaded_theories)))))))) =
+ (command_timings, (scala_functions, (global_theories, loaded_theories))))))) =
YXML.parse_body yxml |>
let open XML.Decode in
(pair (list (pair string properties))
(pair (list (pair string string)) (pair (list (pair string string))
(pair (list (pair string (list string))) (pair (list properties)
- (pair (list string)
- (pair (list (pair string properties))
- (pair (list (pair string string)) (list string)))))))))
+ (pair (list (pair string properties))
+ (pair (list (pair string string)) (list string))))))))
end;
in
init_session
@@ -149,7 +144,6 @@
session_chapters = session_chapters,
bibtex_entries = bibtex_entries,
command_timings = command_timings,
- docs = docs,
scala_functions = map (apsnd Position.of_properties) scala_functions,
global_theories = global_theories,
loaded_theories = loaded_theories}
@@ -169,22 +163,18 @@
fun global_theory a = Symtab.lookup (get_session_base2 #global_theories) a;
fun loaded_theory a = Symtab.defined (get_session_base2 #loaded_theories) a;
-fun check_name which kind markup ctxt arg =
- Completion.check_item kind markup (get_session_base1 which |> sort_by #1) ctxt arg;
-
-val check_session =
- check_name #session_positions "session"
+fun check_session ctxt arg =
+ Completion.check_item "session"
(fn (name, {pos, serial}) =>
Markup.entity Markup.sessionN name
- |> Markup.properties (Position.entity_properties_of false serial pos));
+ |> Markup.properties (Position.entity_properties_of false serial pos))
+ (get_session_base1 #session_positions) ctxt arg;
fun session_chapter name =
the_default "Unsorted" (Symtab.lookup (get_session_base1 #session_chapters) name);
fun last_timing tr = get_timings (get_session_base1 #timings) tr;
-val check_doc = check_name #docs "documentation" (Markup.doc o #1);
-
fun scala_function_pos name =
Symtab.lookup (get_session_base1 #scala_functions) name
|> the_default Position.none;
@@ -386,8 +376,6 @@
val _ = Theory.setup
(Thy_Output.antiquotation_verbatim_embedded \<^binding>\<open>session\<close>
(Scan.lift Parse.embedded_position) check_session #>
- Thy_Output.antiquotation_verbatim_embedded \<^binding>\<open>doc\<close>
- (Scan.lift Parse.embedded_position) check_doc #>
Thy_Output.antiquotation_raw_embedded \<^binding>\<open>path\<close> (document_antiq check_path) (K I) #>
Thy_Output.antiquotation_raw_embedded \<^binding>\<open>file\<close> (document_antiq check_file) (K I) #>
Thy_Output.antiquotation_raw_embedded \<^binding>\<open>dir\<close> (document_antiq check_dir) (K I) #>