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)