--- a/src/Pure/ML/ml_process.scala Mon Sep 16 15:30:38 2019 +0200
+++ b/src/Pure/ML/ml_process.scala Mon Sep 16 16:00:10 2019 +0200
@@ -101,8 +101,7 @@
", session_directories = " + print_table(sessions_structure1.dest_session_directories) +
", docs = " + print_list(base.doc_names) +
", global_theories = " + print_table(base.global_theories.toList) +
- ", loaded_theories = " + print_list(base.loaded_theories.keys) +
- ", known_theories = " + print_table(base.dest_known_theories) + "}")
+ ", loaded_theories = " + print_list(base.loaded_theories.keys) + "}")
}
// process
--- a/src/Pure/PIDE/protocol.ML Mon Sep 16 15:30:38 2019 +0200
+++ b/src/Pure/PIDE/protocol.ML Mon Sep 16 16:00:10 2019 +0200
@@ -20,7 +20,7 @@
val _ =
Isabelle_Process.protocol_command "Prover.init_session_base"
(fn [session_positions_yxml, session_directories_yxml, doc_names_yxml, global_theories_yxml,
- loaded_theories_yxml, known_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;
@@ -32,8 +32,7 @@
session_directories = decode_table session_directories_yxml,
docs = decode_list doc_names_yxml,
global_theories = decode_table global_theories_yxml,
- loaded_theories = decode_list loaded_theories_yxml,
- known_theories = decode_table known_theories_yxml}
+ loaded_theories = decode_list loaded_theories_yxml}
end);
val _ =
--- a/src/Pure/PIDE/protocol.scala Mon Sep 16 15:30:38 2019 +0200
+++ b/src/Pure/PIDE/protocol.scala Mon Sep 16 16:00:10 2019 +0200
@@ -245,8 +245,7 @@
encode_table(resources.sessions_structure.dest_session_directories),
encode_list(base.doc_names),
encode_table(base.global_theories.toList),
- encode_list(base.loaded_theories.keys),
- encode_table(base.dest_known_theories))
+ encode_list(base.loaded_theories.keys))
}
--- a/src/Pure/PIDE/resources.ML Mon Sep 16 15:30:38 2019 +0200
+++ b/src/Pure/PIDE/resources.ML Mon Sep 16 16:00:10 2019 +0200
@@ -12,8 +12,7 @@
session_directories: (string * string) list,
docs: string list,
global_theories: (string * string) list,
- loaded_theories: string list,
- known_theories: (string * string) list} -> unit
+ loaded_theories: string list} -> unit
val finish_session_base: unit -> unit
val global_theory: string -> string option
val loaded_theory: string -> bool
@@ -57,14 +56,13 @@
session_directories = Symtab.empty: Path.T list Symtab.table,
docs = []: (string * entry) list,
global_theories = Symtab.empty: string Symtab.table,
- loaded_theories = Symtab.empty: unit Symtab.table,
- known_theories = Symtab.empty: Path.T Symtab.table};
+ loaded_theories = Symtab.empty: unit Symtab.table};
val global_session_base =
Synchronized.var "Sessions.base" empty_session_base;
fun init_session_base
- {session_positions, session_directories, docs, global_theories, loaded_theories, known_theories} =
+ {session_positions, session_directories, docs, global_theories, loaded_theories} =
Synchronized.change global_session_base
(fn _ =>
{session_positions = sort_by #1 (map (apsnd make_entry) session_positions),
@@ -73,8 +71,7 @@
session_directories Symtab.empty,
docs = sort_by #1 (map (apsnd make_entry o rpair []) docs),
global_theories = Symtab.make global_theories,
- loaded_theories = Symtab.make_set loaded_theories,
- known_theories = Symtab.make (map (apsnd Path.explode) known_theories)});
+ loaded_theories = Symtab.make_set loaded_theories});
fun finish_session_base () =
Synchronized.change global_session_base
@@ -83,8 +80,7 @@
session_directories = Symtab.empty,
docs = [],
global_theories = global_theories,
- loaded_theories = loaded_theories,
- known_theories = #known_theories empty_session_base});
+ loaded_theories = loaded_theories});
fun get_session_base f = f (Synchronized.value global_session_base);
@@ -164,18 +160,15 @@
else Long_Name.qualify qualifier theory;
fun find_theory_file thy_name =
- (case Symtab.lookup (get_session_base #known_theories) thy_name of
- NONE =>
- let
- val thy_file = thy_path (Path.basic (Long_Name.base_name thy_name));
- val session = theory_qualifier thy_name;
- val dirs = Symtab.lookup_list (get_session_base #session_directories) session;
- in
- dirs |> get_first (fn dir =>
- let val path = Path.append dir thy_file
- in if File.is_file path then SOME path else NONE end)
- end
- | some => some);
+ let
+ val thy_file = thy_path (Path.basic (Long_Name.base_name thy_name));
+ val session = theory_qualifier thy_name;
+ val dirs = Symtab.lookup_list (get_session_base #session_directories) session;
+ in
+ dirs |> get_first (fn dir =>
+ let val path = Path.append dir thy_file
+ in if File.is_file path then SOME path else NONE end)
+ end;
fun import_name qualifier dir s =
let val theory = theory_name qualifier (Thy_Header.import_name s) in
@@ -200,7 +193,7 @@
val thy_base_name = Long_Name.base_name thy_name;
val master_file =
(case find_theory_file thy_name of
- SOME known_path => check_file Path.current known_path
+ SOME path => check_file Path.current path
| NONE => check_file dir (thy_path (Path.basic thy_base_name)));
val text = File.read master_file;
--- a/src/Pure/PIDE/resources.scala Mon Sep 16 15:30:38 2019 +0200
+++ b/src/Pure/PIDE/resources.scala Mon Sep 16 16:00:10 2019 +0200
@@ -118,17 +118,17 @@
else Long_Name.qualify(qualifier, theory)
def find_theory_node(theory: String): Option[Document.Node.Name] =
- session_base.known.theories.get(theory).map(_.name) orElse {
- val thy_file = thy_path(Path.basic(Long_Name.base_name(theory)))
- val session = session_base.theory_qualifier(theory)
- val dirs =
- sessions_structure.get(session) match {
- case Some(info) => info.dirs
- case None => Nil
- }
- dirs.collectFirst({
- case dir if (dir + thy_file).is_file => make_theory_node("", dir + thy_file, theory) })
- }
+ {
+ val thy_file = thy_path(Path.basic(Long_Name.base_name(theory)))
+ val session = session_base.theory_qualifier(theory)
+ val dirs =
+ sessions_structure.get(session) match {
+ case Some(info) => info.dirs
+ case None => Nil
+ }
+ dirs.collectFirst({
+ case dir if (dir + thy_file).is_file => make_theory_node("", dir + thy_file, theory) })
+ }
def import_name(qualifier: String, dir: String, s: String): Document.Node.Name =
{
--- a/src/Pure/Thy/sessions.scala Mon Sep 16 15:30:38 2019 +0200
+++ b/src/Pure/Thy/sessions.scala Mon Sep 16 16:00:10 2019 +0200
@@ -174,10 +174,6 @@
def node_syntax(nodes: Document.Nodes, name: Document.Node.Name): Outer_Syntax =
nodes(name).syntax orElse loaded_theory_syntax(name) getOrElse overall_syntax
- def dest_known_theories: List[(String, String)] =
- for ((theory, entry) <- known.theories.toList)
- yield (theory, entry.name.node)
-
def get_imports: Base =
imports getOrElse Base.bootstrap(session_directories, global_theories)
}
--- a/src/Pure/Tools/build.ML Mon Sep 16 15:30:38 2019 +0200
+++ b/src/Pure/Tools/build.ML Mon Sep 16 16:00:10 2019 +0200
@@ -157,7 +157,6 @@
doc_names: string list,
global_theories: (string * string) list,
loaded_theories: string list,
- known_theories: (string * string) list,
bibtex_entries: string list};
fun decode_args yxml =
@@ -167,15 +166,14 @@
val (symbol_codes, (command_timings, (do_output, (verbose, (browser_info,
(document_files, (graph_file, (parent_name, (chapter, (name, (master_dir,
(theories, (session_positions, (session_directories, (doc_names, (global_theories,
- (loaded_theories, (known_theories, bibtex_entries)))))))))))))))))) =
+ (loaded_theories, bibtex_entries))))))))))))))))) =
pair (list (pair string int)) (pair (list properties) (pair bool (pair bool (pair string
(pair (list (pair string string)) (pair string (pair string (pair string (pair string
(pair string
(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)
- (pair (list (pair string string)) (list string))))))))))))))))))
+ (pair (list (pair string string)) (pair (list string) (list string)))))))))))))))))
(YXML.parse_body yxml);
in
Args {symbol_codes = symbol_codes, command_timings = command_timings, do_output = do_output,
@@ -185,13 +183,12 @@
name = name, master_dir = Path.explode master_dir, theories = theories,
session_positions = session_positions, session_directories = session_directories,
doc_names = doc_names, global_theories = global_theories, loaded_theories = loaded_theories,
- known_theories = known_theories, bibtex_entries = bibtex_entries}
+ bibtex_entries = bibtex_entries}
end;
fun build_session (Args {symbol_codes, command_timings, do_output, verbose, browser_info,
document_files, graph_file, parent_name, chapter, name, master_dir, theories, session_positions,
- session_directories, doc_names, global_theories, loaded_theories, known_theories,
- bibtex_entries}) =
+ session_directories, doc_names, global_theories, loaded_theories, bibtex_entries}) =
let
val symbols = HTML.make_symbols symbol_codes;
@@ -201,8 +198,7 @@
session_directories = session_directories,
docs = doc_names,
global_theories = global_theories,
- loaded_theories = loaded_theories,
- known_theories = known_theories};
+ loaded_theories = loaded_theories};
val _ =
Session.init
--- a/src/Pure/Tools/build.scala Mon Sep 16 15:30:38 2019 +0200
+++ b/src/Pure/Tools/build.scala Mon Sep 16 16:00:10 2019 +0200
@@ -221,7 +221,7 @@
pair(list(pair(string, properties)),
pair(list(pair(string, string)),
pair(list(string), pair(list(pair(string, string)),
- pair(list(string), pair(list(pair(string, string)), list(string)))))))))))))))))))(
+ pair(list(string), list(string))))))))))))))))))(
(Symbol.codes, (command_timings, (do_output, (verbose,
(store.browser_info, (info.document_files, (File.standard_path(graph_file),
(parent, (info.chapter, (name, (Path.current,
@@ -229,8 +229,7 @@
(sessions_structure.session_positions,
(sessions_structure.dest_session_directories,
(base.doc_names, (base.global_theories.toList,
- (base.loaded_theories.keys, (base.dest_known_theories,
- info.bibtex_entries.map(_.info))))))))))))))))))))
+ (base.loaded_theories.keys, info.bibtex_entries.map(_.info)))))))))))))))))))
})
val env =