clarified signature;
suppress already loaded theories;

--- a/src/Pure/PIDE/headless.scala	Sun Mar 03 18:45:08 2019 +0100
+++ b/src/Pure/PIDE/headless.scala	Sun Mar 03 19:12:28 2019 +0100
@@ -483,6 +483,18 @@
     def options: Options = session_base_info.options
 
 
+    /* dependencies */
+
+    def used_theories(
+      deps: Sessions.Deps, progress: Progress = No_Progress): List[Document.Node.Name] =
+    {
+      for {
+        (_, name) <- deps.used_theories_condition(options, progress = progress)
+        if !session_base.loaded_theory(name)
+      } yield name
+    }
+
+
     /* session */
 
     def start_session(print_mode: List[String] = Nil, progress: Progress = No_Progress): Session =

--- a/src/Pure/Thy/sessions.scala	Sun Mar 03 18:45:08 2019 +0100
+++ b/src/Pure/Thy/sessions.scala	Sun Mar 03 19:12:28 2019 +0100
@@ -200,7 +200,7 @@
     def imported_sources(name: String): List[SHA1.Digest] =
       session_bases(name).imported_sources.map(_._2)
 
-    def used_theories_condition(default_options: Options, warning: String => Unit = _ => ())
+    def used_theories_condition(default_options: Options, progress: Progress = No_Progress)
       : List[(Options, Document.Node.Name)] =
     {
       val default_skip_proofs = default_options.bool("skip_proofs")
@@ -208,7 +208,8 @@
         session_name <- sessions_structure.build_topological_order
         (options, name) <- session_bases(session_name).used_theories
         if {
-          def warn(msg: String): Unit = warning("Skipping theory " + name + "  (" + msg + ")")
+          def warn(msg: String): Unit =
+            progress.echo_warning("Skipping theory " + name + "  (" + msg + ")")
 
           val conditions =
             space_explode(',', options.string("condition")).

--- a/src/Pure/Tools/dump.scala	Sun Mar 03 18:45:08 2019 +0100
+++ b/src/Pure/Tools/dump.scala	Sun Mar 03 19:12:28 2019 +0100
@@ -87,12 +87,6 @@
         uniform_session = true, loading_sessions = true)
   }
 
-  def used_theories(options: Options, deps: Sessions.Deps, progress: Progress = No_Progress)
-    : List[Document.Node.Name] =
-  {
-    deps.used_theories_condition(options, progress.echo_warning).map(_._2)
-  }
-
 
   /* session */
 
@@ -158,7 +152,7 @@
 
     val session = resources.start_session(progress = progress)
     try {
-      val use_theories = used_theories(resources.options, deps).map(_.theory)
+      val use_theories = resources.used_theories(deps).map(_.theory)
       val use_theories_result =
         session.use_theories(use_theories, progress = progress, commit = Some(Consumer.apply _))