# HG changeset patch # User wenzelm # Date 1568642410 -7200 # Node ID a3cfe859d9158bb18f54aa6e9d76d3666db13225 # Parent 91319c3d28415691d6e10628de60ef740604a9a5 find theories via session directories only -- ignore known_theories; diff -r 91319c3d2841 -r a3cfe859d915 src/Pure/ML/ml_process.scala --- 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 diff -r 91319c3d2841 -r a3cfe859d915 src/Pure/PIDE/protocol.ML --- 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 _ = diff -r 91319c3d2841 -r a3cfe859d915 src/Pure/PIDE/protocol.scala --- 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)) } diff -r 91319c3d2841 -r a3cfe859d915 src/Pure/PIDE/resources.ML --- 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; diff -r 91319c3d2841 -r a3cfe859d915 src/Pure/PIDE/resources.scala --- 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 = { diff -r 91319c3d2841 -r a3cfe859d915 src/Pure/Thy/sessions.scala --- 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) } diff -r 91319c3d2841 -r a3cfe859d915 src/Pure/Tools/build.ML --- 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 diff -r 91319c3d2841 -r a3cfe859d915 src/Pure/Tools/build.scala --- 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 =