# HG changeset patch
# User wenzelm
# Date 1568287989 -7200
# Node ID 8c7706b053c7a33fb42a8a45a3896d8b6d55b408
# Parent  4c53227f4b73548d84e7a76eebc8935d70df01e2
find theory files via session structure: much faster Prover IDE startup;

diff -r 4c53227f4b73 -r 8c7706b053c7 NEWS
--- a/NEWS	Wed Sep 11 20:48:10 2019 +0200
+++ b/NEWS	Thu Sep 12 13:33:09 2019 +0200
@@ -46,6 +46,16 @@
 instances during roundup.
 
 
+*** Isabelle/jEdit Prover IDE ***
+
+* Prover IDE startup is now much faster, because theory dependencies are
+no longer explored in advance. The overall session structure with its
+declarations of 'directories' is sufficient to locate theory files. Thus
+the "session focus" of option "isabelle jedit -S" has become obsolete
+(likewise for "isabelle vscode_server -S"). Existing option "-R" is both
+sufficient and more convenient to start editing a particular session.
+
+
 *** HOL ***
 
 * ASCII membership syntax concerning big operators for infimum and
diff -r 4c53227f4b73 -r 8c7706b053c7 src/Doc/JEdit/JEdit.thy
--- a/src/Doc/JEdit/JEdit.thy	Wed Sep 11 20:48:10 2019 +0200
+++ b/src/Doc/JEdit/JEdit.thy	Thu Sep 12 13:33:09 2019 +0200
@@ -228,12 +228,11 @@
 \<open>Usage: isabelle jedit [OPTIONS] [FILES ...]
 
   Options are:
-    -A NAME      ancestor session for options -R and -S (default: parent)
+    -A NAME      ancestor session for option -R (default: parent)
     -D NAME=X    set JVM system property
     -J OPTION    add JVM runtime option
                  (default $JEDIT_JAVA_SYSTEM_OPTIONS $JEDIT_JAVA_OPTIONS)
     -R NAME      build image with requirements from other sessions
-    -S NAME      like option -R, with focus on selected session
     -b           build only
     -d DIR       include session directory
     -f           fresh build
@@ -262,12 +261,9 @@
   The \<^verbatim>\<open>-R\<close> option builds an auxiliary logic image with all theories from
   other sessions that are not already present in its parent; it also opens the
   session \<^verbatim>\<open>ROOT\<close> entry in the editor to facilitate editing of the main
-  session. The \<^verbatim>\<open>-S\<close> option is like \<^verbatim>\<open>-R\<close>, with a focus on the selected
-  session and its descendants: the namespace of accessible theories is
-  restricted accordingly. This reduces startup time for big projects, notably
-  the ``Archive of Formal Proofs''. The \<^verbatim>\<open>-A\<close> option specifies and alternative
-  ancestor session for options \<^verbatim>\<open>-R\<close> and \<^verbatim>\<open>-S\<close>: this allows to restructure the
-  hierarchy of session images on the spot.
+  session. The \<^verbatim>\<open>-A\<close> option specifies and alternative ancestor session for
+  option \<^verbatim>\<open>-R\<close>: this allows to restructure the hierarchy of session images on
+  the spot.
 
   The \<^verbatim>\<open>-i\<close> option includes additional sessions into the name-space of
   theories: multiple occurrences are possible.
diff -r 4c53227f4b73 -r 8c7706b053c7 src/Pure/ML/ml_process.scala
--- a/src/Pure/ML/ml_process.scala	Wed Sep 11 20:48:10 2019 +0200
+++ b/src/Pure/ML/ml_process.scala	Thu Sep 12 13:33:09 2019 +0200
@@ -29,14 +29,15 @@
     val logic_name = Isabelle_System.default_logic(logic)
     val _store = store.getOrElse(Sessions.store(options))
 
+    val sessions_structure1 =
+      sessions_structure.getOrElse(Sessions.load_structure(options, dirs = dirs))
+
     val heaps: List[String] =
       if (raw_ml_system) Nil
       else {
         val selection = Sessions.Selection(sessions = List(logic_name))
-        val selected_sessions =
-          sessions_structure.getOrElse(Sessions.load_structure(options, dirs = dirs))
-            .selection(selection)
-        selected_sessions.build_requirements(List(logic_name)).
+        sessions_structure1.selection(selection).
+          build_requirements(List(logic_name)).
           map(a => File.platform_path(_store.the_heap(a)))
       }
 
@@ -96,7 +97,8 @@
               ML_Syntax.print_pair(ML_Syntax.print_string_bytes, ML_Syntax.print_properties))(list)
 
           List("Resources.init_session_base" +
-            " {sessions = " + print_sessions(base.known.sessions.toList) +
+            " {session_positions = " + print_sessions(sessions_structure1.session_positions) +
+            ", 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) +
diff -r 4c53227f4b73 -r 8c7706b053c7 src/Pure/PIDE/headless.scala
--- a/src/Pure/PIDE/headless.scala	Wed Sep 11 20:48:10 2019 +0200
+++ b/src/Pure/PIDE/headless.scala	Thu Sep 12 13:33:09 2019 +0200
@@ -562,7 +562,8 @@
   class Resources private[Headless](
       val session_base_info: Sessions.Base_Info,
       log: Logger = No_Logger)
-    extends isabelle.Resources(session_base_info.check_base, log = log)
+    extends isabelle.Resources(
+      session_base_info.sessions_structure, session_base_info.check_base, log = log)
   {
     resources =>
 
diff -r 4c53227f4b73 -r 8c7706b053c7 src/Pure/PIDE/protocol.ML
--- a/src/Pure/PIDE/protocol.ML	Wed Sep 11 20:48:10 2019 +0200
+++ b/src/Pure/PIDE/protocol.ML	Thu Sep 12 13:33:09 2019 +0200
@@ -19,8 +19,8 @@
 
 val _ =
   Isabelle_Process.protocol_command "Prover.init_session_base"
-    (fn [sessions_yxml, doc_names_yxml, global_theories_yxml, loaded_theories_yxml,
-          known_theories_yxml] =>
+    (fn [session_positions_yxml, session_directories_yxml, doc_names_yxml, global_theories_yxml,
+          loaded_theories_yxml, known_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;
@@ -28,7 +28,8 @@
           YXML.parse_body #> let open XML.Decode in list (pair string properties) end;
       in
         Resources.init_session_base
-          {sessions = decode_sessions sessions_yxml,
+          {session_positions = decode_sessions session_positions_yxml,
+           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,
diff -r 4c53227f4b73 -r 8c7706b053c7 src/Pure/PIDE/protocol.scala
--- a/src/Pure/PIDE/protocol.scala	Wed Sep 11 20:48:10 2019 +0200
+++ b/src/Pure/PIDE/protocol.scala	Thu Sep 12 13:33:09 2019 +0200
@@ -241,7 +241,8 @@
   {
     val base = resources.session_base.standard_path
     protocol_command("Prover.init_session_base",
-      encode_sessions(base.known.sessions.toList),
+      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),
diff -r 4c53227f4b73 -r 8c7706b053c7 src/Pure/PIDE/resources.ML
--- a/src/Pure/PIDE/resources.ML	Wed Sep 11 20:48:10 2019 +0200
+++ b/src/Pure/PIDE/resources.ML	Thu Sep 12 13:33:09 2019 +0200
@@ -8,7 +8,8 @@
 sig
   val default_qualifier: string
   val init_session_base:
-    {sessions: (string * Properties.T) list,
+    {session_positions: (string * Properties.T) list,
+     session_directories: (string * string) list,
      docs: string list,
      global_theories: (string * string) list,
      loaded_theories: string list,
@@ -16,7 +17,6 @@
   val finish_session_base: unit -> unit
   val global_theory: string -> string option
   val loaded_theory: string -> bool
-  val known_theory: string -> Path.T option
   val check_session: Proof.context -> string * Position.T -> string
   val check_doc: Proof.context -> string * Position.T -> string
   val master_directory: theory -> Path.T
@@ -24,6 +24,7 @@
   val begin_theory: Path.T -> Thy_Header.header -> theory list -> theory
   val thy_path: Path.T -> Path.T
   val theory_qualifier: string -> string
+  val find_theory_file: string -> Path.T option
   val import_name: string -> Path.T -> string ->
     {node_name: Path.T, master_dir: Path.T, theory_name: string}
   val check_thy: Path.T -> string ->
@@ -52,7 +53,8 @@
   {pos = Position.of_properties props, serial = serial ()};
 
 val empty_session_base =
-  {sessions = []: (string * entry) list,
+  {session_positions = []: (string * entry) list,
+   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,
@@ -61,10 +63,14 @@
 val global_session_base =
   Synchronized.var "Sessions.base" empty_session_base;
 
-fun init_session_base {sessions, docs, global_theories, loaded_theories, known_theories} =
+fun init_session_base
+    {session_positions, session_directories, docs, global_theories, loaded_theories, known_theories} =
   Synchronized.change global_session_base
     (fn _ =>
-      {sessions = sort_by #1 (map (apsnd make_entry) sessions),
+      {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,
        docs = sort_by #1 (map (apsnd make_entry o rpair []) docs),
        global_theories = Symtab.make global_theories,
        loaded_theories = Symtab.make_set loaded_theories,
@@ -73,7 +79,8 @@
 fun finish_session_base () =
   Synchronized.change global_session_base
     (fn {global_theories, loaded_theories, ...} =>
-      {sessions = [],
+      {session_positions = [],
+       session_directories = Symtab.empty,
        docs = [],
        global_theories = global_theories,
        loaded_theories = loaded_theories,
@@ -83,7 +90,6 @@
 
 fun global_theory a = Symtab.lookup (get_session_base #global_theories) a;
 fun loaded_theory a = Symtab.defined (get_session_base #loaded_theories) a;
-fun known_theory a = Symtab.lookup (get_session_base #known_theories) a;
 
 fun check_name which kind markup ctxt (name, pos) =
   let val entries = get_session_base which in
@@ -106,7 +112,7 @@
   Markup.properties
     (Position.entity_properties_of false serial pos) (Markup.entity Markup.sessionN name);
 
-val check_session = check_name #sessions "session" markup_session;
+val check_session = check_name #session_positions "session" markup_session;
 val check_doc = check_name #docs "documentation" (fn name => fn _ => Markup.doc name);
 
 
@@ -157,6 +163,20 @@
   then theory
   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);
+
 fun import_name qualifier dir s =
   let val theory = theory_name qualifier (Thy_Header.import_name s) in
     if loaded_theory theory
@@ -164,7 +184,7 @@
     else
       let
         val node_name =
-          (case known_theory theory of
+          (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
@@ -179,7 +199,7 @@
   let
     val thy_base_name = Long_Name.base_name thy_name;
     val master_file =
-      (case known_theory thy_name of
+      (case find_theory_file thy_name of
         SOME known_path => check_file Path.current known_path
       | NONE => check_file dir (thy_path (Path.basic thy_base_name)));
     val text = File.read master_file;
diff -r 4c53227f4b73 -r 8c7706b053c7 src/Pure/PIDE/resources.scala
--- a/src/Pure/PIDE/resources.scala	Wed Sep 11 20:48:10 2019 +0200
+++ b/src/Pure/PIDE/resources.scala	Thu Sep 12 13:33:09 2019 +0200
@@ -14,6 +14,7 @@
 
 
 class Resources(
+  val sessions_structure: Sessions.Structure,
   val session_base: Sessions.Base,
   val log: Logger = No_Logger)
 {
@@ -47,6 +48,13 @@
   def append(node_name: Document.Node.Name, source_path: Path): String =
     append(node_name.master_dir, source_path)
 
+  def make_theory_node(dir: String, file: Path, theory: String): Document.Node.Name =
+  {
+    val node = append(dir, file)
+    val master_dir = append(dir, file.dir)
+    Document.Node.Name(node, master_dir, theory)
+  }
+
 
   /* source files of Isabelle/ML bootstrap */
 
@@ -109,22 +117,30 @@
       theory
     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) })
+    }
+
   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)
     else {
-      session_base.known_theory(theory) match {
+      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 {
-            val path = Path.explode(s)
-            val node = append(dir, thy_path(path))
-            val master_dir = append(dir, path.dir)
-            Document.Node.Name(node, master_dir, theory)
-          }
+          else make_theory_node(dir, thy_path(Path.explode(s)), theory)
       }
     }
   }
diff -r 4c53227f4b73 -r 8c7706b053c7 src/Pure/Thy/sessions.ML
--- a/src/Pure/Thy/sessions.ML	Wed Sep 11 20:48:10 2019 +0200
+++ b/src/Pure/Thy/sessions.ML	Thu Sep 12 13:33:09 2019 +0200
@@ -86,7 +86,7 @@
               val {node_name, theory_name, ...} =
                 Resources.import_name session session_dir s
                   handle ERROR msg => error (msg ^ Position.here pos);
-              val theory_path = the_default node_name (Resources.known_theory theory_name);
+              val theory_path = the_default node_name (Resources.find_theory_file theory_name);
               val _ = Resources.check_file ctxt (SOME Path.current) (Path.implode theory_path, pos);
             in () end);
 
diff -r 4c53227f4b73 -r 8c7706b053c7 src/Pure/Thy/sessions.scala
--- a/src/Pure/Thy/sessions.scala	Wed Sep 11 20:48:10 2019 +0200
+++ b/src/Pure/Thy/sessions.scala	Thu Sep 12 13:33:09 2019 +0200
@@ -41,7 +41,6 @@
     val empty: Known = Known()
 
     def make(local_dir: Path, bases: List[Base],
-      sessions: List[(String, Position.T)] = Nil,
       theories: List[Document.Node.Entry] = Nil,
       loaded_files: List[(String, List[Path])] = Nil): Known =
     {
@@ -58,9 +57,6 @@
           entry.name.path.canonical_file.toPath.startsWith(local_path))
       }
 
-      val known_sessions =
-        (sessions.toMap /: bases)({ case (known, base) => known ++ base.known.sessions })
-
       val known_theories =
         (Map.empty[String, Document.Node.Entry] /: (bases_iterator(false) ++ theories.iterator))({
           case (known, entry) =>
@@ -92,7 +88,6 @@
         (loaded_files.toMap /: bases.map(base => base.known.loaded_files))(_ ++ _)
 
       Known(
-        known_sessions,
         known_theories,
         known_theories_local,
         known_files.iterator.map(p => (p._1, p._2.reverse)).toMap,
@@ -101,7 +96,6 @@
   }
 
   sealed case class Known(
-    sessions: Map[String, Position.T] = Map.empty,
     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,
@@ -180,9 +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 known_theory(name: String): Option[Document.Node.Name] =
-      known.theories.get(name).map(_.name)
-
     def dest_known_theories: List[(String, String)] =
       for ((theory, entry) <- known.theories.toList)
         yield (theory, entry.name.node)
@@ -304,7 +295,7 @@
               parent_base.copy(known =
                 Known.make(info.dir, parent_base :: info.imports.map(session_bases(_))))
 
-            val resources = new Resources(imports_base)
+            val resources = new Resources(sessions_structure, imports_base)
 
             if (verbose || list_files) {
               val groups =
@@ -371,7 +362,6 @@
 
             val known =
               Known.make(info.dir, List(imports_base),
-                sessions = List(info.name -> info.pos),
                 theories = dependencies.entries,
                 loaded_files = loaded_files)
 
@@ -466,9 +456,7 @@
     dirs: List[Path] = Nil,
     include_sessions: List[String] = Nil,
     session_ancestor: Option[String] = None,
-    session_requirements: Boolean = false,
-    session_focus: Boolean = false,
-    all_known: Boolean = false): Base_Info =
+    session_requirements: Boolean = false): Base_Info =
   {
     val full_sessions = load_structure(options, dirs = dirs)
 
@@ -529,22 +517,11 @@
       else load_structure(options, dirs = dirs, infos = infos1)
 
     val selected_sessions1 =
-    {
-      val sel_sessions1 = session1 :: session :: include_sessions
-      val select_sessions1 =
-        if (session_focus) {
-          full_sessions1.check_sessions(sel_sessions1)
-          full_sessions1.imports_descendants(sel_sessions1)
-        }
-        else sel_sessions1
-      full_sessions1.selection(Selection(sessions = select_sessions1))
-    }
+      full_sessions1.selection(Selection(sessions = session1 :: session :: include_sessions))
 
-    val sessions1 = if (all_known) full_sessions1 else selected_sessions1
-    val deps1 = Sessions.deps(sessions1, progress = progress)
-    val base1 = deps1(session1).copy(known = deps1.all_known)
+    val deps1 = Sessions.deps(selected_sessions1, progress = progress)
 
-    Base_Info(options, dirs, session1, deps1.sessions_structure, deps1.errors, base1, infos1)
+    Base_Info(options, dirs, session1, full_sessions1, deps1.errors, deps1(session1), infos1)
   }
 
 
@@ -701,6 +678,9 @@
     val build_graph = add_edges(info_graph, "parent", _.parent)
     val imports_graph = add_edges(build_graph, "imports", _.imports)
 
+    val session_positions: List[(String, Position.T)] =
+      (for ((name, (info, _)) <- info_graph.iterator) yield (name, info.pos)).toList
+
     val session_directories: Map[JFile, String] =
       (Map.empty[JFile, String] /:
         (for {
@@ -735,10 +715,12 @@
             }
           })
 
-    new Structure(session_directories, global_theories, build_graph, imports_graph)
+    new Structure(
+      session_positions, session_directories, global_theories, build_graph, imports_graph)
   }
 
   final class Structure private[Sessions](
+      val session_positions: List[(String, Position.T)],
       val session_directories: Map[JFile, String],
       val global_theories: Map[String, String],
       val build_graph: Graph[String, Info],
@@ -746,6 +728,10 @@
   {
     sessions_structure =>
 
+    def dest_session_directories: List[(String, String)] =
+      for ((file, session) <- session_directories.toList)
+        yield (File.standard_path(file), session)
+
     lazy val chapters: SortedMap[String, List[Info]] =
       (SortedMap.empty[String, List[Info]] /: build_graph.iterator)(
         { case (chs, (_, (info, _))) =>
@@ -811,7 +797,8 @@
       }
 
       new Structure(
-        session_directories, global_theories, restrict(build_graph), restrict(imports_graph))
+        session_positions, session_directories, global_theories,
+        restrict(build_graph), restrict(imports_graph))
     }
 
     def selection_deps(
diff -r 4c53227f4b73 -r 8c7706b053c7 src/Pure/Tools/build.ML
--- a/src/Pure/Tools/build.ML	Wed Sep 11 20:48:10 2019 +0200
+++ b/src/Pure/Tools/build.ML	Thu Sep 12 13:33:09 2019 +0200
@@ -152,7 +152,8 @@
   name: string,
   master_dir: Path.T,
   theories: (Options.T * (string * Position.T) list) list,
-  sessions: (string * Properties.T) list,
+  session_positions: (string * Properties.T) list,
+  session_directories: (string * string) list,
   doc_names: string list,
   global_theories: (string * string) list,
   loaded_theories: string list,
@@ -165,35 +166,39 @@
     val position = Position.of_properties o properties;
     val (symbol_codes, (command_timings, (do_output, (verbose, (browser_info,
       (document_files, (graph_file, (parent_name, (chapter, (name, (master_dir,
-      (theories, (sessions, (doc_names, (global_theories, (loaded_theories,
-      (known_theories, bibtex_entries))))))))))))))))) =
+      (theories, (session_positions, (session_directories, (doc_names, (global_theories,
+      (loaded_theories, (known_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 string)
+              (pair (list (pair string properties))
                 (pair (list (pair string string)) (pair (list string)
-                  (pair (list (pair string string)) (list string)))))))))))))))))
+                  (pair (list (pair string string)) (pair (list string)
+                    (pair (list (pair string string)) (list string))))))))))))))))))
       (YXML.parse_body yxml);
   in
     Args {symbol_codes = symbol_codes, command_timings = command_timings, do_output = do_output,
       verbose = verbose, browser_info = Path.explode browser_info,
       document_files = map (apply2 Path.explode) document_files,
       graph_file = Path.explode graph_file, parent_name = parent_name, chapter = chapter,
-      name = name, master_dir = Path.explode master_dir, theories = theories, sessions = sessions,
+      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}
   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, sessions,
-    doc_names, global_theories, loaded_theories, known_theories, bibtex_entries}) =
+    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}) =
   let
     val symbols = HTML.make_symbols symbol_codes;
 
     val _ =
       Resources.init_session_base
-        {sessions = sessions,
+        {session_positions = session_positions,
+         session_directories = session_directories,
          docs = doc_names,
          global_theories = global_theories,
          loaded_theories = loaded_theories,
diff -r 4c53227f4b73 -r 8c7706b053c7 src/Pure/Tools/build.scala
--- a/src/Pure/Tools/build.scala	Wed Sep 11 20:48:10 2019 +0200
+++ b/src/Pure/Tools/build.scala	Thu Sep 12 13:33:09 2019 +0200
@@ -197,6 +197,8 @@
   {
     val options = NUMA.policy_options(info.options, numa_node)
 
+    val sessions_structure = deps.sessions_structure
+
     private val graph_file = Isabelle_System.tmp_file("session_graph", "pdf")
     isabelle.graphview.Graph_File.write(options, graph_file, deps(name).session_graph_display)
 
@@ -216,15 +218,19 @@
                 pair(Path.encode, pair(list(pair(Path.encode, Path.encode)), pair(string,
                 pair(string, pair(string, pair(string, pair(Path.encode,
                 pair(list(pair(Options.encode, list(pair(string, properties)))),
-                pair(list(pair(string, properties)), pair(list(string),
+                pair(list(pair(string, properties)),
                 pair(list(pair(string, string)),
-                pair(list(string), pair(list(pair(string, string)), list(string))))))))))))))))))(
+                pair(list(string), pair(list(pair(string, string)),
+                pair(list(string), pair(list(pair(string, 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,
-                (info.theories, (base.known.sessions.toList, (base.doc_names,
-                (base.global_theories.toList, (base.loaded_theories.keys, (base.dest_known_theories,
-                info.bibtex_entries.map(_.info)))))))))))))))))))
+                (info.theories,
+                (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))))))))))))))))))))
             })
 
         val env =
@@ -238,7 +244,7 @@
             ML_Syntax.print_string_bytes(File.platform_path(store.output_heap(name)))
 
         if (pide && !Sessions.is_pure(name)) {
-          val resources = new Resources(deps(parent))
+          val resources = new Resources(sessions_structure, deps(parent))
           val session = new Session(options, resources)
           val handler = new Handler(progress, session, name)
           session.init_protocol_handler(handler)
@@ -246,7 +252,7 @@
           val session_result = Future.promise[Process_Result]
 
           Isabelle_Process.start(session, options, logic = parent, cwd = info.dir.file, env = env,
-            sessions_structure = Some(deps.sessions_structure), store = Some(store),
+            sessions_structure = Some(sessions_structure), store = Some(store),
             phase_changed =
             {
               case Session.Ready => session.protocol_command("build_session", args_yxml)
diff -r 4c53227f4b73 -r 8c7706b053c7 src/Pure/Tools/imports.scala
--- a/src/Pure/Tools/imports.scala	Wed Sep 11 20:48:10 2019 +0200
+++ b/src/Pure/Tools/imports.scala	Thu Sep 12 13:33:09 2019 +0200
@@ -99,21 +99,24 @@
     select_dirs: List[Path] = Nil,
     verbose: Boolean = false) =
   {
+    val sessions_structure =
+      Sessions.load_structure(options, dirs = dirs, select_dirs = select_dirs)
+
     val deps =
-      Sessions.load_structure(options, dirs = dirs, select_dirs = select_dirs).
-        selection_deps(options, selection, progress = progress, verbose = verbose).check_errors
+      sessions_structure.selection_deps(options, selection, progress = progress, verbose = verbose).
+        check_errors
 
     val root_keywords = Sessions.root_syntax.keywords
 
     if (operation_imports) {
       val report_imports: List[Report] =
-        deps.sessions_structure.build_topological_order.map((session_name: String) =>
+        sessions_structure.build_topological_order.map((session_name: String) =>
           {
-            val info = deps.sessions_structure(session_name)
+            val info = sessions_structure(session_name)
             val session_base = deps(session_name)
 
             val declared_imports =
-              deps.sessions_structure.imports_requirements(List(session_name)).toSet
+              sessions_structure.imports_requirements(List(session_name)).toSet
 
             val extra_imports =
               (for {
@@ -125,18 +128,18 @@
               } yield qualifier).toSet
 
             val loaded_imports =
-              deps.sessions_structure.imports_requirements(
+              sessions_structure.imports_requirements(
                 session_base.loaded_theories.keys.map(a =>
                   session_base.theory_qualifier(session_base.known.theories(a).name)))
               .toSet - session_name
 
             val minimal_imports =
               loaded_imports.filter(s1 =>
-                !loaded_imports.exists(s2 => deps.sessions_structure.imports_graph.is_edge(s1, s2)))
+                !loaded_imports.exists(s2 => sessions_structure.imports_graph.is_edge(s1, s2)))
 
             def make_result(set: Set[String]): Option[List[String]] =
               if (set.isEmpty) None
-              else Some(deps.sessions_structure.imports_topological_order.filter(set))
+              else Some(sessions_structure.imports_topological_order.filter(set))
 
             Report(info, declared_imports, make_result(extra_imports),
               if (loaded_imports == declared_imports - session_name) None
@@ -170,13 +173,13 @@
     if (operation_update) {
       progress.echo("\nUpdate theory imports" + update_message + ":")
       val updates =
-        deps.sessions_structure.build_topological_order.flatMap(session_name =>
+        sessions_structure.build_topological_order.flatMap(session_name =>
           {
-            val info = deps.sessions_structure(session_name)
+            val info = sessions_structure(session_name)
             val session_base = deps(session_name)
-            val session_resources = new Resources(session_base)
+            val session_resources = new Resources(sessions_structure, session_base)
             val imports_base = session_base.get_imports
-            val imports_resources = new Resources(imports_base)
+            val imports_resources = new Resources(sessions_structure, imports_base)
 
             def standard_import(qualifier: String, dir: String, s: String): String =
               imports_resources.standard_import(session_base, qualifier, dir, s)
diff -r 4c53227f4b73 -r 8c7706b053c7 src/Tools/VSCode/src/server.scala
--- a/src/Tools/VSCode/src/server.scala	Wed Sep 11 20:48:10 2019 +0200
+++ b/src/Tools/VSCode/src/server.scala	Thu Sep 12 13:33:09 2019 +0200
@@ -35,7 +35,6 @@
       var logic_ancestor: Option[String] = None
       var log_file: Option[Path] = None
       var logic_requirements = false
-      var logic_focus = false
       var dirs: List[Path] = Nil
       var include_sessions: List[String] = Nil
       var logic = default_logic
@@ -47,10 +46,9 @@
 Usage: isabelle vscode_server [OPTIONS]
 
   Options are:
-    -A NAME      ancestor session for options -R and -S (default: parent)
+    -A NAME      ancestor session for option -R (default: parent)
     -L FILE      logging on FILE
     -R NAME      build image with requirements from other sessions
-    -S NAME      like option -R, with focus on selected session
     -d DIR       include session directory
     -i NAME      include session in name-space of theories
     -l NAME      logic session name (default ISABELLE_LOGIC=""" + quote(default_logic) + """)
@@ -63,7 +61,6 @@
         "A:" -> (arg => logic_ancestor = Some(arg)),
         "L:" -> (arg => log_file = Some(Path.explode(File.standard_path(arg)))),
         "R:" -> (arg => { logic = arg; logic_requirements = true }),
-        "S:" -> (arg => { logic = arg; logic_requirements = true; logic_focus = true }),
         "d:" -> (arg => dirs = dirs ::: List(Path.explode(File.standard_path(arg)))),
         "i:" -> (arg => include_sessions = include_sessions ::: List(arg)),
         "l:" -> (arg => logic = arg),
@@ -79,8 +76,7 @@
       val server =
         new Server(channel, options, session_name = logic, session_dirs = dirs,
           include_sessions = include_sessions, session_ancestor = logic_ancestor,
-          session_requirements = logic_requirements, session_focus = logic_focus,
-          all_known = !logic_focus, modes = modes, log = log)
+          session_requirements = logic_requirements, modes = modes, log = log)
 
       // prevent spurious garbage on the main protocol channel
       val orig_out = System.out
@@ -107,8 +103,6 @@
   include_sessions: List[String] = Nil,
   session_ancestor: Option[String] = None,
   session_requirements: Boolean = false,
-  session_focus: Boolean = false,
-  all_known: Boolean = false,
   modes: List[String] = Nil,
   log: Logger = No_Logger)
 {
@@ -271,9 +265,9 @@
         val base_info =
           Sessions.base_info(
             options, session_name, dirs = session_dirs, include_sessions = include_sessions,
-            session_ancestor = session_ancestor, session_requirements = session_requirements,
-            session_focus = session_focus, all_known = all_known)
-        val session_base = base_info.check_base
+            session_ancestor = session_ancestor, session_requirements = session_requirements)
+
+        base_info.check_base
 
         def build(no_build: Boolean = false): Build.Results =
           Build.build(options, build_heap = true, no_build = no_build, dirs = session_dirs,
@@ -289,7 +283,7 @@
           if (!build().ok) { progress.echo(fail_msg); error(fail_msg) }
         }
 
-        val resources = new VSCode_Resources(options, session_base, log)
+        val resources = new VSCode_Resources(options, base_info, log)
           {
             override def commit(change: Session.Change): Unit =
               if (change.deps_changed || undefined_blobs(change.version.nodes).nonEmpty)
diff -r 4c53227f4b73 -r 8c7706b053c7 src/Tools/VSCode/src/vscode_resources.scala
--- a/src/Tools/VSCode/src/vscode_resources.scala	Wed Sep 11 20:48:10 2019 +0200
+++ b/src/Tools/VSCode/src/vscode_resources.scala	Thu Sep 12 13:33:09 2019 +0200
@@ -72,9 +72,9 @@
 
 class VSCode_Resources(
     val options: Options,
-    session_base: Sessions.Base,
+    session_base_info: Sessions.Base_Info,
     log: Logger = No_Logger)
-  extends Resources(session_base, log = log)
+  extends Resources(session_base_info.sessions_structure, session_base_info.check_base, log = log)
 {
   resources =>
 
diff -r 4c53227f4b73 -r 8c7706b053c7 src/Tools/jEdit/lib/Tools/jedit
--- a/src/Tools/jEdit/lib/Tools/jedit	Wed Sep 11 20:48:10 2019 +0200
+++ b/src/Tools/jEdit/lib/Tools/jedit	Thu Sep 12 13:33:09 2019 +0200
@@ -100,12 +100,11 @@
   echo "Usage: isabelle $PRG [OPTIONS] [FILES ...]"
   echo
   echo "  Options are:"
-  echo "    -A NAME      ancestor session for options -R and -S (default: parent)"
+  echo "    -A NAME      ancestor session for options -R (default: parent)"
   echo "    -D NAME=X    set JVM system property"
   echo "    -J OPTION    add JVM runtime option"
   echo "                 (default $JEDIT_JAVA_SYSTEM_OPTIONS $JEDIT_JAVA_OPTIONS)"
   echo "    -R NAME      build image with requirements from other sessions"
-  echo "    -S NAME      like option -R, with focus on selected session"
   echo "    -b           build only"
   echo "    -d DIR       include session directory"
   echo "    -f           fresh build"
@@ -146,7 +145,6 @@
 ML_PROCESS_POLICY=""
 JEDIT_LOGIC_ANCESTOR=""
 JEDIT_LOGIC_REQUIREMENTS=""
-JEDIT_LOGIC_FOCUS=""
 JEDIT_INCLUDE_SESSIONS=""
 JEDIT_SESSION_DIRS="-"
 JEDIT_LOGIC=""
@@ -157,7 +155,7 @@
 function getoptions()
 {
   OPTIND=1
-  while getopts "A:BFD:J:R:S:bd:fi:j:l:m:np:su" OPT
+  while getopts "A:BFD:J:R:bd:fi:j:l:m:np:su" OPT
   do
     case "$OPT" in
       A)
@@ -173,11 +171,6 @@
         JEDIT_LOGIC="$OPTARG"
         JEDIT_LOGIC_REQUIREMENTS="true"
         ;;
-      S)
-        JEDIT_LOGIC="$OPTARG"
-        JEDIT_LOGIC_REQUIREMENTS="true"
-        JEDIT_LOGIC_FOCUS="true"
-        ;;
       b)
         BUILD_ONLY=true
         ;;
@@ -426,7 +419,7 @@
 if [ "$BUILD_ONLY" = false ]
 then
   export JEDIT_SESSION_DIRS JEDIT_LOGIC JEDIT_LOGIC_ANCESTOR JEDIT_LOGIC_REQUIREMENTS \
-    JEDIT_LOGIC_FOCUS JEDIT_INCLUDE_SESSIONS JEDIT_PRINT_MODE JEDIT_NO_BUILD JEDIT_BUILD_MODE
+    JEDIT_INCLUDE_SESSIONS JEDIT_PRINT_MODE JEDIT_NO_BUILD JEDIT_BUILD_MODE
   export JEDIT_ML_PROCESS_POLICY="$ML_PROCESS_POLICY"
   classpath "$JEDIT_HOME/dist/jedit.jar"
   exec isabelle java -splash:"$(platform_path "$ISABELLE_HOME/lib/logo/isabelle.gif")" \
diff -r 4c53227f4b73 -r 8c7706b053c7 src/Tools/jEdit/src/jedit_resources.scala
--- a/src/Tools/jEdit/src/jedit_resources.scala	Wed Sep 11 20:48:10 2019 +0200
+++ b/src/Tools/jEdit/src/jedit_resources.scala	Thu Sep 12 13:33:09 2019 +0200
@@ -28,7 +28,7 @@
 }
 
 class JEdit_Resources private(val session_base_info: Sessions.Base_Info)
-  extends Resources(session_base_info.base.platform_path)
+  extends Resources(session_base_info.sessions_structure, session_base_info.base.platform_path)
 {
   def session_name: String = session_base_info.session
   def session_errors: List[String] = session_base_info.errors
diff -r 4c53227f4b73 -r 8c7706b053c7 src/Tools/jEdit/src/jedit_sessions.scala
--- a/src/Tools/jEdit/src/jedit_sessions.scala	Wed Sep 11 20:48:10 2019 +0200
+++ b/src/Tools/jEdit/src/jedit_sessions.scala	Thu Sep 12 13:33:09 2019 +0200
@@ -56,7 +56,6 @@
 
   def logic_ancestor: Option[String] = proper_string(Isabelle_System.getenv("JEDIT_LOGIC_ANCESTOR"))
   def logic_requirements: Boolean = Isabelle_System.getenv("JEDIT_LOGIC_REQUIREMENTS") == "true"
-  def logic_focus: Boolean = Isabelle_System.getenv("JEDIT_LOGIC_FOCUS") == "true"
   def logic_include_sessions: List[String] =
     space_explode(':', Isabelle_System.getenv("JEDIT_INCLUDE_SESSIONS"))
 
@@ -124,9 +123,7 @@
       include_sessions = logic_include_sessions,
       session = logic_name(options),
       session_ancestor = logic_ancestor,
-      session_requirements = logic_requirements,
-      session_focus = logic_focus,
-      all_known = !logic_focus)
+      session_requirements = logic_requirements)
 
   def session_build(
     options: Options, progress: Progress = No_Progress, no_build: Boolean = false): Int =