--- a/src/Pure/ML/ml_process.scala Mon Sep 16 19:31:38 2019 +0200
+++ b/src/Pure/ML/ml_process.scala Mon Sep 16 23:51:24 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/command.scala Mon Sep 16 19:31:38 2019 +0200
+++ b/src/Pure/PIDE/command.scala Mon Sep 16 23:51:24 2019 +0200
@@ -524,20 +524,7 @@
for { ((import_name, pos), s) <- imports_pos zip raw_imports if !can_import(import_name) }
yield {
val completion =
- if (Thy_Header.is_base_name(s)) {
- val completed = Completion.completed(import_name.theory_base_name)
- val qualifier = resources.session_base.theory_qualifier(node_name)
- val dir = node_name.master_dir
- for {
- known_name <- resources.session_base.known.theory_names
- if completed(known_name.theory_base_name)
- }
- yield {
- resources.standard_import(
- resources.session_base, qualifier, dir, known_name.theory)
- }
- }.sorted
- else Nil
+ if (Thy_Header.is_base_name(s)) resources.complete_import_name(node_name, s) else Nil
val msg =
"Bad theory import " +
Markup.Path(import_name.node).markup(quote(import_name.toString)) +
--- a/src/Pure/PIDE/document.scala Mon Sep 16 19:31:38 2019 +0200
+++ b/src/Pure/PIDE/document.scala Mon Sep 16 23:51:24 2019 +0200
@@ -102,8 +102,6 @@
{
val empty = Name("")
- def loaded_theory(theory: String): Name = Name(theory, "", theory)
-
object Ordering extends scala.math.Ordering[Name]
{
def compare(name1: Name, name2: Name): Int = name1.node compare name2.node
--- a/src/Pure/PIDE/headless.scala Mon Sep 16 19:31:38 2019 +0200
+++ b/src/Pure/PIDE/headless.scala Mon Sep 16 23:51:24 2019 +0200
@@ -161,7 +161,7 @@
def cancel_result: Use_Theories_State =
if (finished_result) this else copy(result = Some(Exn.Exn(Exn.Interrupt())))
- def clean_theories: (List[Document.Node.Name], Use_Theories_State) =
+ def clean_theories: ((List[Document.Node.Name], Int), Use_Theories_State) =
{
@tailrec def frontier(base: List[Document.Node.Name], front: Set[Document.Node.Name])
: Set[Document.Node.Name] =
@@ -175,7 +175,7 @@
}
}
- if (already_committed.isEmpty) (Nil, this)
+ if (already_committed.isEmpty) ((Nil, 0), this)
else {
val base =
(for {
@@ -183,9 +183,9 @@
if succs.isEmpty && already_committed.isDefinedAt(name)
} yield name).toList
val clean = frontier(base, Set.empty)
- if (clean.isEmpty) (Nil, this)
+ if (clean.isEmpty) ((Nil, 0), this)
else {
- (dep_graph.topological_order.filter(clean),
+ ((dep_graph.topological_order.filter(clean), dep_graph.size - clean.size),
copy(dep_graph = dep_graph.exclude(clean)))
}
}
@@ -323,9 +323,10 @@
val delay_commit_clean =
Standard_Thread.delay_first(commit_cleanup_delay max Time.zero) {
- val clean_theories = use_theories_state.change_result(_.clean_theories)
+ val (clean_theories, remaining) = use_theories_state.change_result(_.clean_theories)
if (clean_theories.nonEmpty) {
- progress.echo("Removing " + clean_theories.length + " theories ...")
+ progress.echo("Removing " + clean_theories.length +
+ " theories (" + remaining + " remaining) ...")
resources.clean_theories(session, id, clean_theories)
}
}
--- a/src/Pure/PIDE/protocol.ML Mon Sep 16 19:31:38 2019 +0200
+++ b/src/Pure/PIDE/protocol.ML Mon Sep 16 23:51:24 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 19:31:38 2019 +0200
+++ b/src/Pure/PIDE/protocol.scala Mon Sep 16 23:51:24 2019 +0200
@@ -239,14 +239,12 @@
def session_base(resources: Resources)
{
- val base = resources.session_base.standard_path
protocol_command("Prover.init_session_base",
encode_sessions(resources.sessions_structure.session_positions),
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(resources.session_base.doc_names),
+ encode_table(resources.session_base.global_theories.toList),
+ encode_list(resources.session_base.loaded_theories.keys))
}
--- a/src/Pure/PIDE/resources.ML Mon Sep 16 19:31:38 2019 +0200
+++ b/src/Pure/PIDE/resources.ML Mon Sep 16 23:51:24 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);
@@ -116,7 +112,6 @@
val check_doc = check_name #docs "documentation" (fn name => fn _ => Markup.doc name);
-
(* manage source files *)
type files =
@@ -164,33 +159,34 @@
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 make_theory_node node_name theory =
+ {node_name = node_name, master_dir = Path.dir node_name, theory_name = theory};
+
+fun loaded_theory_node theory =
+ {node_name = Path.basic theory, master_dir = Path.current, theory_name = theory};
fun import_name qualifier dir s =
- let val theory = theory_name qualifier (Thy_Header.import_name s) in
- if loaded_theory theory
- then {node_name = Path.basic theory, master_dir = Path.current, theory_name = theory}
+ let
+ val theory = theory_name qualifier (Thy_Header.import_name s);
+ fun theory_node () =
+ make_theory_node (File.full_path dir (thy_path (Path.expand (Path.explode s)))) theory;
+ in
+ if not (Thy_Header.is_base_name s) then theory_node ()
+ else if loaded_theory theory then loaded_theory_node theory
else
- let
- val node_name =
- (case find_theory_file theory of
- SOME node_name => node_name
- | NONE =>
- if Thy_Header.is_base_name s andalso Long_Name.is_qualified s
- then Path.explode s
- else File.full_path dir (thy_path (Path.expand (Path.explode s))));
- in {node_name = node_name, master_dir = Path.dir node_name, theory_name = theory} end
+ (case find_theory_file theory of
+ SOME node_name => make_theory_node node_name theory
+ | NONE => if Long_Name.is_qualified s then loaded_theory_node theory else theory_node ())
end;
fun check_file dir file = File.check_file (File.full_path dir file);
@@ -200,7 +196,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 19:31:38 2019 +0200
+++ b/src/Pure/PIDE/resources.scala Mon Sep 16 23:51:24 2019 +0200
@@ -55,6 +55,9 @@
Document.Node.Name(node, master_dir, theory)
}
+ def loaded_theory_node(theory: String): Document.Node.Name =
+ Document.Node.Name(theory, "", theory)
+
/* source files of Isabelle/ML bootstrap */
@@ -118,29 +121,29 @@
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 =
{
val theory = theory_name(qualifier, Thy_Header.import_name(s))
- if (session_base.loaded_theory(theory)) Document.Node.Name.loaded_theory(theory)
+ def theory_node = make_theory_node(dir, thy_path(Path.explode(s)), theory)
+
+ if (!Thy_Header.is_base_name(s)) theory_node
+ else if (session_base.loaded_theory(theory)) loaded_theory_node(theory)
else {
find_theory_node(theory) match {
case Some(node_name) => node_name
- case None =>
- if (Thy_Header.is_base_name(s) && Long_Name.is_qualified(s))
- Document.Node.Name.loaded_theory(theory)
- else make_theory_node(dir, thy_path(Path.explode(s)), theory)
+ case None => if (Long_Name.is_qualified(s)) loaded_theory_node(theory) else theory_node
}
}
}
@@ -151,14 +154,15 @@
def import_name(info: Sessions.Info, s: String): Document.Node.Name =
import_name(info.name, info.dir.implode, s)
- def find_theory(default_qualifier: String, file: JFile): Option[Document.Node.Name] =
+ def find_theory(file: JFile): Option[Document.Node.Name] =
{
- val dir = File.canonical(file).getParentFile
- val qualifier = session_base.session_directories.get(dir).getOrElse(default_qualifier)
- Thy_Header.theory_name(file.getName) match {
- case "" => None
- case s => Some(import_name(qualifier, File.path(file).dir.implode, s))
- }
+ for {
+ qualifier <- session_base.session_directories.get(File.canonical(file).getParentFile)
+ theory_base <- proper_string(Thy_Header.theory_name(file.getName))
+ theory = theory_name(qualifier, theory_base)
+ theory_node <- find_theory_node(theory)
+ if File.eq(theory_node.path.file, file)
+ } yield theory_node
}
def dump_checkpoints(info: Sessions.Info): Set[Document.Node.Name] =
@@ -168,26 +172,21 @@
(thy, _) <- thys.iterator
} yield import_name(info, thy)).toSet
- def standard_import(base: Sessions.Base, qualifier: String, dir: String, s: String): String =
+ def complete_import_name(context_name: Document.Node.Name, s: String): List[String] =
{
- val name = import_name(qualifier, dir, s)
- val s1 =
- if (session_base.loaded_theory(name)) name.theory
- else {
- (try { Some(name.path) } catch { case ERROR(_) => None }) match {
- case None => s
- case Some(path) =>
- session_base.known.get_file(path.file) match {
- case Some(name1) if base.theory_qualifier(name1) != qualifier =>
- name1.theory
- case Some(name1) if Thy_Header.is_base_name(s) =>
- name1.theory_base_name
- case _ => s
- }
- }
- }
- val name2 = import_name(qualifier, dir, s1)
- if (name.node == name2.node) s1 else s
+ val context_session = session_base.theory_qualifier(context_name)
+ val context_dir =
+ try { Some(context_name.master_dir_path) }
+ catch { case ERROR(_) => None }
+ (for {
+ (session, (info, _)) <- sessions_structure.imports_graph.iterator
+ dir <- (if (session == context_session) context_dir.toList else info.dirs).iterator
+ theory <- Thy_Header.try_read_dir(dir).iterator
+ if Completion.completed(s)(theory)
+ } yield {
+ if (session == context_session || session_base.global_theories.isDefinedAt(theory)) theory
+ else Long_Name.qualify(session, theory)
+ }).toList.sorted
}
def with_thy_reader[A](name: Document.Node.Name, f: Reader[Char] => A): A =
--- a/src/Pure/Thy/sessions.scala Mon Sep 16 19:31:38 2019 +0200
+++ b/src/Pure/Thy/sessions.scala Mon Sep 16 23:51:24 2019 +0200
@@ -40,25 +40,18 @@
{
val empty: Known = Known()
- def make(local_dir: Path, bases: List[Base],
+ def make(bases: List[Base],
theories: List[Document.Node.Entry] = Nil,
loaded_files: List[(String, List[Path])] = Nil): Known =
{
- def bases_iterator(local: Boolean) =
+ def bases_theories_iterator =
for {
base <- bases.iterator
- (_, entry) <- (if (local) base.known.theories_local else base.known.theories).iterator
+ (_, entry) <- base.known.theories.iterator
} yield entry
- def local_theories_iterator =
- {
- val local_path = local_dir.canonical_file.toPath
- theories.iterator.filter(entry =>
- entry.name.path.canonical_file.toPath.startsWith(local_path))
- }
-
val known_theories =
- (Map.empty[String, Document.Node.Entry] /: (bases_iterator(false) ++ theories.iterator))({
+ (Map.empty[String, Document.Node.Entry] /: (bases_theories_iterator ++ theories.iterator))({
case (known, entry) =>
known.get(entry.name.theory) match {
case Some(entry1) if entry.name != entry1.name =>
@@ -67,62 +60,23 @@
case _ => known + (entry.name.theory -> entry)
}
})
- val known_theories_local =
- (Map.empty[String, Document.Node.Entry] /:
- (bases_iterator(true) ++ local_theories_iterator))({
- case (known, entry) => known + (entry.name.theory -> entry)
- })
- val known_files =
- (Map.empty[JFile, List[Document.Node.Name]] /:
- (bases_iterator(true) ++ bases_iterator(false) ++ theories.iterator))({
- case (known, entry) =>
- val name = entry.name
- val file = name.path.canonical_file
- val theories1 = known.getOrElse(file, Nil)
- if (theories1.exists(name1 => name.node == name1.node && name.theory == name1.theory))
- known
- else known + (file -> (name :: theories1))
- })
val known_loaded_files =
(loaded_files.toMap /: bases.map(base => base.known.loaded_files))(_ ++ _)
- Known(
- known_theories,
- known_theories_local,
- known_files.iterator.map(p => (p._1, p._2.reverse)).toMap,
- known_loaded_files)
+ Known(known_theories, known_loaded_files)
}
}
sealed case class Known(
theories: Map[String, Document.Node.Entry] = Map.empty,
- theories_local: Map[String, Document.Node.Entry] = Map.empty,
- files: Map[JFile, List[Document.Node.Name]] = Map.empty,
loaded_files: Map[String, List[Path]] = Map.empty)
{
def platform_path: Known =
- copy(theories = for ((a, b) <- theories) yield (a, b.map(File.platform_path(_))),
- theories_local = for ((a, b) <- theories_local) yield (a, b.map(File.platform_path(_))),
- files = for ((a, b) <- files) yield (a, b.map(c => c.map(File.platform_path(_)))))
+ copy(theories = for ((a, b) <- theories) yield (a, b.map(File.platform_path(_))))
def standard_path: Known =
- copy(theories = for ((a, b) <- theories) yield (a, b.map(File.standard_path(_))),
- theories_local = for ((a, b) <- theories_local) yield (a, b.map(File.standard_path(_))),
- files = for ((a, b) <- files) yield (a, b.map(c => c.map(File.standard_path(_)))))
-
- def theory_names: List[Document.Node.Name] = theories.iterator.map(p => p._2.name).toList
-
- lazy val theory_graph: Document.Node.Name.Graph[Unit] =
- Document.Node.Name.make_graph(
- for ((_, entry) <- theories.toList)
- yield ((entry.name, ()), entry.header.imports.map(imp => theories(imp.theory).name)))
-
- def get_file(file: JFile, bootstrap: Boolean = false): Option[Document.Node.Name] =
- {
- val res = files.getOrElse(File.canonical(file), Nil).headOption
- if (bootstrap) res.map(_.map_theory(Thy_Header.bootstrap_name(_))) else res
- }
+ copy(theories = for ((a, b) <- theories) yield (a, b.map(File.standard_path(_))))
}
object Base
@@ -156,9 +110,6 @@
"Sessions.Base(loaded_theories = " + loaded_theories.size +
", used_theories = " + used_theories.length + ")"
- def platform_path: Base = copy(known = known.platform_path)
- def standard_path: Base = copy(known = known.standard_path)
-
def theory_qualifier(name: String): String =
global_theories.getOrElse(name, Long_Name.qualifier(name))
def theory_qualifier(name: Document.Node.Name): String = theory_qualifier(name.theory)
@@ -174,10 +125,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)
}
@@ -289,7 +236,7 @@
}
val imports_base: Sessions.Base =
parent_base.copy(known =
- Known.make(info.dir, parent_base :: info.imports.map(session_bases(_))))
+ Known.make(parent_base :: info.imports.map(session_bases(_))))
val resources = new Resources(sessions_structure, imports_base)
@@ -357,7 +304,7 @@
}
val known =
- Known.make(info.dir, List(imports_base),
+ Known.make(List(imports_base),
theories = dependencies.entries,
loaded_files = loaded_files)
@@ -365,14 +312,19 @@
for ((options, name) <- dependencies.adjunct_theories)
yield (name, options)
+ def used_theories_session_iterator: Iterator[Document.Node.Name] =
+ for {
+ (name, _) <- used_theories.iterator
+ if imports_base.theory_qualifier(name) == session_name
+ } yield name
+
val dir_errors =
{
val ok = info.dirs.map(_.canonical_file).toSet
val bad =
(for {
- (name, _) <- used_theories.iterator
- if imports_base.theory_qualifier(name) == session_name
- val path = name.master_dir_path
+ name <- used_theories_session_iterator
+ path = name.master_dir_path
if !ok(path.canonical_file)
path1 = File.relative_path(info.dir.canonical, path).getOrElse(path)
} yield (path1, name)).toList
@@ -385,8 +337,15 @@
if (bad_dirs.isEmpty) Nil
else List("Implicit use of session directories: " + commas(bad_dirs))
val errs3 = for (p <- info.dirs if !p.is_dir) yield "No such directory: " + p
+ val errs4 =
+ (for {
+ name <- used_theories_session_iterator
+ name1 <- resources.find_theory_node(name.theory)
+ if name.node != name1.node
+ } yield "Incoherent theory file import:\n " + name.path + " vs. \n " + name1.path)
+ .toList
- errs1 ::: errs2 ::: errs3
+ errs1 ::: errs2 ::: errs3 ::: errs4
}
val sources_errors =
--- a/src/Pure/Thy/thy_header.scala Mon Sep 16 19:31:38 2019 +0200
+++ b/src/Pure/Thy/thy_header.scala Mon Sep 16 23:51:24 2019 +0200
@@ -116,6 +116,14 @@
def bootstrap_name(theory: String): String =
bootstrap_thys.collectFirst({ case (a, b) if a == theory => b }).getOrElse(theory)
+ def try_read_dir(dir: Path): List[String] =
+ {
+ val files =
+ try { File.read_dir(dir) }
+ catch { case ERROR(_) => Nil }
+ for { Thy_File_Name(name) <- files } yield name
+ }
+
/* parser */
--- a/src/Pure/Thy/thy_info.ML Mon Sep 16 19:31:38 2019 +0200
+++ b/src/Pure/Thy/thy_info.ML Mon Sep 16 23:51:24 2019 +0200
@@ -370,7 +370,7 @@
Result {theory = theory, exec_id = exec_id, present = present, commit = commit, weight = weight}
end;
-fun check_deps dir name =
+fun check_thy_deps dir name =
(case lookup_deps name of
SOME NONE => (true, NONE, Position.none, get_imports name, [])
| NONE =>
@@ -402,7 +402,7 @@
let
val _ = member (op =) initiators theory_name andalso error (cycle_msg initiators);
- val (current, deps, theory_pos, imports, keywords) = check_deps master_dir theory_name
+ val (current, deps, theory_pos, imports, keywords) = check_thy_deps master_dir theory_name
handle ERROR msg =>
cat_error msg
("The error(s) above occurred for theory " ^ quote theory_name ^
--- a/src/Pure/Tools/build.ML Mon Sep 16 19:31:38 2019 +0200
+++ b/src/Pure/Tools/build.ML Mon Sep 16 23:51:24 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 19:31:38 2019 +0200
+++ b/src/Pure/Tools/build.scala Mon Sep 16 23:51:24 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 =
--- a/src/Tools/VSCode/src/vscode_resources.scala Mon Sep 16 19:31:38 2019 +0200
+++ b/src/Tools/VSCode/src/vscode_resources.scala Mon Sep 16 23:51:24 2019 +0200
@@ -94,10 +94,10 @@
def node_file(name: Document.Node.Name): JFile = new JFile(name.node)
def node_name(file: JFile): Document.Node.Name =
- find_theory(Sessions.DRAFT, file) getOrElse {
+ find_theory(file) getOrElse {
val node = file.getPath
val theory = theory_name(Sessions.DRAFT, Thy_Header.theory_name(node))
- if (session_base.loaded_theory(theory)) Document.Node.Name.loaded_theory(theory)
+ if (session_base.loaded_theory(theory)) loaded_theory_node(theory)
else {
val master_dir = file.getParent
Document.Node.Name(node, master_dir, theory)
--- a/src/Tools/jEdit/src/jedit_resources.scala Mon Sep 16 19:31:38 2019 +0200
+++ b/src/Tools/jEdit/src/jedit_resources.scala Mon Sep 16 23:51:24 2019 +0200
@@ -28,7 +28,7 @@
}
class JEdit_Resources private(val session_base_info: Sessions.Base_Info)
- extends Resources(session_base_info.sessions_structure, session_base_info.base.platform_path)
+ extends Resources(session_base_info.sessions_structure, session_base_info.base)
{
def session_name: String = session_base_info.session
def session_errors: List[String] = session_base_info.errors
@@ -37,11 +37,11 @@
/* document node name */
def node_name(path: String): Document.Node.Name =
- JEdit_Lib.check_file(path).flatMap(file => find_theory(Sessions.DRAFT, file)) getOrElse {
+ JEdit_Lib.check_file(path).flatMap(find_theory(_)) getOrElse {
val vfs = VFSManager.getVFSForPath(path)
val node = if (vfs.isInstanceOf[FileVFS]) MiscUtilities.resolveSymlinks(path) else path
val theory = theory_name(Sessions.DRAFT, Thy_Header.theory_name(node))
- if (session_base.loaded_theory(theory)) Document.Node.Name.loaded_theory(theory)
+ if (session_base.loaded_theory(theory)) loaded_theory_node(theory)
else {
val master_dir = vfs.getParentOfPath(path)
Document.Node.Name(node, master_dir, theory)