# HG changeset patch
# User wenzelm
# Date 1492981610 -7200
# Node ID 94c514ea2846d727393b2dd3d2b818c1b66d0436
# Parent  3219a7ed669ca9460b69292c50ec5d96dc886580
support for potential session imports;

diff -r 3219a7ed669c -r 94c514ea2846 src/Pure/Thy/sessions.scala
--- a/src/Pure/Thy/sessions.scala	Sun Apr 23 22:00:15 2017 +0200
+++ b/src/Pure/Thy/sessions.scala	Sun Apr 23 23:06:50 2017 +0200
@@ -448,6 +448,9 @@
     def build_topological_order: List[Info] =
       build_graph.topological_order.map(apply(_))
 
+    def imports_ancestors(name: String): List[String] =
+      imports_graph.all_preds(List(name)).tail.reverse
+
     def imports_topological_order: List[Info] =
       imports_graph.topological_order.map(apply(_))
 
diff -r 3219a7ed669c -r 94c514ea2846 src/Pure/Tools/imports.scala
--- a/src/Pure/Tools/imports.scala	Sun Apr 23 22:00:15 2017 +0200
+++ b/src/Pure/Tools/imports.scala	Sun Apr 23 23:06:50 2017 +0200
@@ -71,6 +71,7 @@
 
   def imports(
     options: Options,
+    operation_imports: Boolean = false,
     operation_manifest: Boolean = false,
     operation_update: Boolean = false,
     progress: Progress = No_Progress,
@@ -87,6 +88,34 @@
         global_theories = full_sessions.global_theories,
         all_known = true)
 
+    val root_keywords = Sessions.root_syntax.keywords
+
+
+    if (operation_imports) {
+      progress.echo("\nPotential session imports:")
+      selected.sorted.foreach(session_name =>
+      {
+        val info = full_sessions(session_name)
+        val session_resources = new Resources(deps(session_name))
+
+        val declared_imports =
+          full_sessions.imports_ancestors(session_name).toSet + session_name
+        val extra_imports =
+          (for {
+            (_, a) <- session_resources.session_base.known.theories.iterator
+            if session_resources.theory_qualifier(a) == info.theory_qualifier
+            b <- deps.all_known.get_file(Path.explode(a.node).file)
+            qualifier = session_resources.theory_qualifier(b)
+            if !declared_imports.contains(qualifier)
+          } yield qualifier).toSet
+
+        if (extra_imports.nonEmpty) {
+          progress.echo("session " + Token.quote_name(root_keywords, session_name) + ": " +
+            extra_imports.toList.sorted.map(Token.quote_name(root_keywords, _)).mkString(" "))
+        }
+      })
+    }
+
     if (operation_manifest) {
       progress.echo("\nManifest check:")
       val unused_files =
@@ -108,12 +137,6 @@
           val session_resources = new Resources(session_base)
           val imports_resources = new Resources(session_base.get_imports)
 
-          val local_theories =
-            (for {
-              (_, name) <- session_base.known.theories_local.iterator
-              if session_resources.theory_qualifier(name) == info.theory_qualifier
-            } yield name).toSet
-
           def standard_import(qualifier: String, dir: String, s: String): String =
           {
             val name = imports_resources.import_name(qualifier, dir, s)
@@ -133,7 +156,7 @@
           val updates_root =
             for {
               (_, pos) <- info.theories.flatMap(_._2)
-              upd <- update_name(Sessions.root_syntax.keywords, pos,
+              upd <- update_name(root_keywords, pos,
                 standard_import(info.theory_qualifier, info.dir.implode, _))
             } yield upd
 
@@ -163,7 +186,7 @@
           conflicts.map({ case (file, bad) =>
             "Conflicting updates for file " + file + bad.mkString("\n  ", "\n  ", "") })))
 
-      for ((file, upds) <- file_updates.iterator_list) {
+      for ((file, upds) <- file_updates.iterator_list.toList.sortBy(p => p._1.toString)) {
         progress.echo("file " + quote(file.toString))
         val edits =
           upds.sortBy(upd => - upd.range.start).flatMap(upd =>
@@ -187,6 +210,7 @@
     Isabelle_Tool("imports", "maintain theory imports wrt. session structure", args =>
     {
       var select_dirs: List[Path] = Nil
+      var operation_imports = false
       var operation_manifest = false
       var requirements = false
       var operation_update = false
@@ -203,6 +227,7 @@
 
   Options are:
     -D DIR       include session directory and select its sessions
+    -I           operation: report potential session imports
     -M           operation: Mercurial manifest check for imported theory files
     -R           operate on requirements of selected sessions
     -U           operation: update theory imports to use session qualifiers
@@ -215,9 +240,10 @@
     -x NAME      exclude session NAME and all descendants
 
   Maintain theory imports wrt. session structure. At least one operation
-  needs to be specified (see option -U).
+  needs to be specified (see options -I -M -U).
 """,
       "D:" -> (arg => select_dirs = select_dirs ::: List(Path.explode(arg))),
+      "I" -> (_ => operation_imports = true),
       "M" -> (_ => operation_manifest = true),
       "R" -> (_ => requirements = true),
       "U" -> (_ => operation_update = true),
@@ -230,7 +256,7 @@
       "x:" -> (arg => exclude_sessions = exclude_sessions ::: List(arg)))
 
       val sessions = getopts(args)
-      if (args.isEmpty || !(operation_manifest || operation_update))
+      if (args.isEmpty || !(operation_imports || operation_manifest || operation_update))
         getopts.usage()
 
       val selection =
@@ -239,7 +265,8 @@
 
       val progress = new Console_Progress(verbose = verbose)
 
-      imports(options, operation_manifest = operation_manifest, operation_update = operation_update,
+      imports(options, operation_imports = operation_imports,
+        operation_manifest = operation_manifest, operation_update = operation_update,
         progress = progress, selection = selection, dirs = dirs, select_dirs = select_dirs,
         verbose = verbose)
     })