# HG changeset patch
# User wenzelm
# Date 1507816698 -7200
# Node ID c757690655486e0b8c14f2b02fadc5cf3ef34745
# Parent  a91b6d80c91104c12aa74fc1434528c4e475c762
more informative Imports.Report with actual session imports (minimized);

diff -r a91b6d80c911 -r c75769065548 NEWS
--- a/NEWS	Thu Oct 12 11:39:54 2017 +0200
+++ b/NEWS	Thu Oct 12 15:58:18 2017 +0200
@@ -78,6 +78,9 @@
 corresponding environment values into account, when determining the
 up-to-date status of a session.
 
+* Command-line tool "isabelle imports -I" also reports actual session
+imports. This helps to minimize the session dependency graph.
+
 
 New in Isabelle2017 (October 2017)
 ----------------------------------
diff -r a91b6d80c911 -r c75769065548 src/Doc/System/Sessions.thy
--- a/src/Doc/System/Sessions.thy	Thu Oct 12 11:39:54 2017 +0200
+++ b/src/Doc/System/Sessions.thy	Thu Oct 12 15:58:18 2017 +0200
@@ -466,7 +466,7 @@
   Options are:
     -B NAME      include session NAME and all descendants
     -D DIR       include session directory and select its sessions
-    -I           operation: report potential session imports
+    -I           operation: report session imports
     -M           operation: Mercurial repository check for theory files
     -R           operate on requirements of selected sessions
     -U           operation: update theory imports to use session qualifiers
@@ -495,12 +495,19 @@
   Option \<^verbatim>\<open>-v\<close> increases the general level of verbosity.
 
   \<^medskip>
-  Option \<^verbatim>\<open>-I\<close> determines potential session imports, which may be turned into
-  \isakeyword{sessions} within the corresponding \<^verbatim>\<open>ROOT\<close> file entry. Thus
-  theory imports from other sessions may use session-qualified names. For
-  example, adhoc \<^theory_text>\<open>imports\<close> \<^verbatim>\<open>"~~/src/HOL/Library/Multiset"\<close> may become formal
-  \<^theory_text>\<open>imports\<close> \<^verbatim>\<open>"HOL-Library.Multiset"\<close> after adding \isakeyword{sessions}
-  \<^verbatim>\<open>"HOL-Library"\<close> to the \<^verbatim>\<open>ROOT\<close> entry.
+  Option \<^verbatim>\<open>-I\<close> determines reports session imports:
+
+    \<^descr>[Potential session imports] are derived from old-style use of theory
+    files from other sessions via the directory structure. After declaring
+    those as \isakeyword{sessions} in the corresponding \<^verbatim>\<open>ROOT\<close> file entry, a
+    proper session-qualified theory name can be used (cf.\ option \<^verbatim>\<open>-U\<close>). For
+    example, adhoc \<^theory_text>\<open>imports\<close> \<^verbatim>\<open>"~~/src/HOL/Library/Multiset"\<close> becomes formal
+    \<^theory_text>\<open>imports\<close> \<^verbatim>\<open>"HOL-Library.Multiset"\<close> after adding \isakeyword{sessions}
+    \<^verbatim>\<open>"HOL-Library"\<close> to the \<^verbatim>\<open>ROOT\<close> entry.
+
+    \<^descr>[Actual session imports] are derived from the session qualifiers of all
+    currently imported theories. This helps to minimize dependencies in the
+    session import structure to what is actually required.
 
   \<^medskip>
   Option \<^verbatim>\<open>-M\<close> checks imported theories against the Mercurial repositories of
diff -r a91b6d80c911 -r c75769065548 src/Pure/Tools/imports.scala
--- a/src/Pure/Tools/imports.scala	Thu Oct 12 11:39:54 2017 +0200
+++ b/src/Pure/Tools/imports.scala	Thu Oct 12 15:58:18 2017 +0200
@@ -30,6 +30,23 @@
     }
 
 
+  /* report imports */
+
+  sealed case class Report(
+    info: Sessions.Info,
+    declared_imports: Set[String],
+    potential_imports: Option[List[String]],
+    actual_imports: Option[List[String]])
+  {
+    def print(keywords: Keyword.Keywords, result: List[String]): String =
+    {
+      def print_name(name: String): String = Token.quote_name(keywords, name)
+
+      "  session " + print_name(info.name) + ": " + result.map(print_name(_)).mkString(" ")
+    }
+  }
+
+
   /* update imports */
 
   sealed case class Update(range: Text.Range, old_text: String, new_text: String)
@@ -91,15 +108,16 @@
 
     val root_keywords = Sessions.root_syntax.keywords
 
-
     if (operation_imports) {
-      progress.echo("\nPotential session imports:")
-      selected.flatMap(session_name =>
+      val report_imports: List[Report] = selected.map((session_name: String) =>
       {
-        val info = full_sessions(session_name)
-        val session_resources = new Resources(deps(session_name))
+        val info = selected_sessions(session_name)
+        val session_base = deps(session_name)
+        val session_resources = new Resources(session_base)
 
-        val declared_imports = full_sessions.imports_requirements(List(session_name)).toSet
+        val declared_imports =
+          selected_sessions.imports_requirements(List(session_name)).toSet
+
         val extra_imports =
           (for {
             (_, a) <- session_resources.session_base.known.theories.iterator
@@ -109,12 +127,36 @@
             if !declared_imports.contains(qualifier)
           } yield qualifier).toSet
 
-        if (extra_imports.isEmpty) None
-        else Some((session_name, extra_imports.toList.sorted, declared_imports.size))
-      }).sortBy(_._3).foreach({ case (session_name, extra_imports, _) =>
-        progress.echo("session " + Token.quote_name(root_keywords, session_name) + ": " +
-          extra_imports.map(Token.quote_name(root_keywords, _)).mkString(" "))
+        val loaded_imports =
+          selected_sessions.imports_requirements(
+            session_base.loaded_theories.keys.map(a =>
+              session_resources.theory_qualifier(session_base.known.theories(a))))
+          .toSet - session_name
+
+        val minimal_imports =
+          loaded_imports.filter(s1 =>
+            !loaded_imports.exists(s2 => selected_sessions.imports_graph.is_edge(s1, s2)))
+
+        def make_result(set: Set[String]): Option[List[String]] =
+          if (set.isEmpty) None
+          else Some(selected_sessions.imports_topological_order.map(_.name).filter(set))
+
+        Report(info, declared_imports, make_result(extra_imports),
+          if (loaded_imports == declared_imports - session_name) None
+          else make_result(minimal_imports))
       })
+
+      progress.echo("\nPotential session imports:")
+      for {
+        report <- report_imports.sortBy(_.declared_imports.size)
+        potential_imports <- report.potential_imports
+      } progress.echo(report.print(root_keywords, potential_imports))
+
+      progress.echo("\nActual session imports:")
+      for {
+        report <- report_imports
+        actual_imports <- report.actual_imports
+      } progress.echo(report.print(root_keywords, actual_imports))
     }
 
     if (operation_repository_files) {
@@ -133,7 +175,7 @@
       val updates =
         selected.flatMap(session_name =>
         {
-          val info = full_sessions(session_name)
+          val info = selected_sessions(session_name)
           val session_base = deps(session_name)
           val session_resources = new Resources(session_base)
           val imports_base = session_base.get_imports
@@ -219,7 +261,7 @@
   Options are:
     -B NAME      include session NAME and all descendants
     -D DIR       include session directory and select its sessions
-    -I           operation: report potential session imports
+    -I           operation: report session imports
     -M           operation: Mercurial repository check for theory files
     -R           operate on requirements of selected sessions
     -U           operation: update theory imports to use session qualifiers