# HG changeset patch
# User wenzelm
# Date 1492981833 -7200
# Node ID 1070be5763725cefae548ab593a9c7418de6ec6d
# Parent  fcd599570afa4ad1b24b7e137d34846b93a8232c# Parent  c556c09765dd8cefceacb098a685cbd7ff070e3d
merged

diff -r fcd599570afa -r 1070be576372 Admin/Release/CHECKLIST
--- a/Admin/Release/CHECKLIST	Sun Apr 23 14:53:35 2017 +0200
+++ b/Admin/Release/CHECKLIST	Sun Apr 23 23:10:33 2017 +0200
@@ -11,6 +11,7 @@
 
 - check sources:
     isabelle check_sources '~~' '$AFP_BASE'
+    isabelle imports -M -a -d '~~/src/Benchmarks'
 
 - check ANNOUNCE, README, NEWS, COPYRIGHT, CONTRIBUTORS;
 
diff -r fcd599570afa -r 1070be576372 NEWS
--- a/NEWS	Sun Apr 23 14:53:35 2017 +0200
+++ b/NEWS	Sun Apr 23 23:10:33 2017 +0200
@@ -201,6 +201,13 @@
 a negative value means the current state in the ML heap image remains
 unchanged.
 
+* Command-line tool "isabelle imports" helps to maintain theory imports
+wrt. session structure. Examples:
+
+  isabelle imports -I -a
+  isabelle imports -U -a
+  isabelle imports -M -a -d '~~/src/Benchmarks'
+
 
 
 New in Isabelle2016-1 (December 2016)
diff -r fcd599570afa -r 1070be576372 src/HOL/Induct/Infinitely_Branching_Tree.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Induct/Infinitely_Branching_Tree.thy	Sun Apr 23 23:10:33 2017 +0200
@@ -0,0 +1,108 @@
+(*  Title:      HOL/Induct/Infinitely_Branching_Tree.thy
+    Author:     Stefan Berghofer, TU Muenchen
+    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
+*)
+
+section \<open>Infinitely branching trees\<close>
+
+theory Infinitely_Branching_Tree
+imports Main
+begin
+
+datatype 'a tree =
+    Atom 'a
+  | Branch "nat \<Rightarrow> 'a tree"
+
+primrec map_tree :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a tree \<Rightarrow> 'b tree"
+  where
+    "map_tree f (Atom a) = Atom (f a)"
+  | "map_tree f (Branch ts) = Branch (\<lambda>x. map_tree f (ts x))"
+
+lemma tree_map_compose: "map_tree g (map_tree f t) = map_tree (g \<circ> f) t"
+  by (induct t) simp_all
+
+primrec exists_tree :: "('a \<Rightarrow> bool) \<Rightarrow> 'a tree \<Rightarrow> bool"
+  where
+    "exists_tree P (Atom a) = P a"
+  | "exists_tree P (Branch ts) = (\<exists>x. exists_tree P (ts x))"
+
+lemma exists_map:
+  "(\<And>x. P x \<Longrightarrow> Q (f x)) \<Longrightarrow>
+    exists_tree P ts \<Longrightarrow> exists_tree Q (map_tree f ts)"
+  by (induct ts) auto
+
+
+subsection\<open>The Brouwer ordinals, as in ZF/Induct/Brouwer.thy.\<close>
+
+datatype brouwer = Zero | Succ brouwer | Lim "nat \<Rightarrow> brouwer"
+
+text \<open>Addition of ordinals\<close>
+primrec add :: "brouwer \<Rightarrow> brouwer \<Rightarrow> brouwer"
+  where
+    "add i Zero = i"
+  | "add i (Succ j) = Succ (add i j)"
+  | "add i (Lim f) = Lim (\<lambda>n. add i (f n))"
+
+lemma add_assoc: "add (add i j) k = add i (add j k)"
+  by (induct k) auto
+
+text \<open>Multiplication of ordinals\<close>
+primrec mult :: "brouwer \<Rightarrow> brouwer \<Rightarrow> brouwer"
+  where
+    "mult i Zero = Zero"
+  | "mult i (Succ j) = add (mult i j) i"
+  | "mult i (Lim f) = Lim (\<lambda>n. mult i (f n))"
+
+lemma add_mult_distrib: "mult i (add j k) = add (mult i j) (mult i k)"
+  by (induct k) (auto simp add: add_assoc)
+
+lemma mult_assoc: "mult (mult i j) k = mult i (mult j k)"
+  by (induct k) (auto simp add: add_mult_distrib)
+
+text \<open>We could probably instantiate some axiomatic type classes and use
+  the standard infix operators.\<close>
+
+
+subsection \<open>A WF Ordering for The Brouwer ordinals (Michael Compton)\<close>
+
+text \<open>To use the function package we need an ordering on the Brouwer
+  ordinals.  Start with a predecessor relation and form its transitive
+  closure.\<close>
+
+definition brouwer_pred :: "(brouwer \<times> brouwer) set"
+  where "brouwer_pred = (\<Union>i. {(m, n). n = Succ m \<or> (\<exists>f. n = Lim f \<and> m = f i)})"
+
+definition brouwer_order :: "(brouwer \<times> brouwer) set"
+  where "brouwer_order = brouwer_pred\<^sup>+"
+
+lemma wf_brouwer_pred: "wf brouwer_pred"
+  unfolding wf_def brouwer_pred_def
+  apply clarify
+  apply (induct_tac x)
+    apply blast+
+  done
+
+lemma wf_brouwer_order[simp]: "wf brouwer_order"
+  unfolding brouwer_order_def
+  by (rule wf_trancl[OF wf_brouwer_pred])
+
+lemma [simp]: "(j, Succ j) \<in> brouwer_order"
+  by (auto simp add: brouwer_order_def brouwer_pred_def)
+
+lemma [simp]: "(f n, Lim f) \<in> brouwer_order"
+  by (auto simp add: brouwer_order_def brouwer_pred_def)
+
+text \<open>Example of a general function\<close>
+function add2 :: "brouwer \<Rightarrow> brouwer \<Rightarrow> brouwer"
+  where
+    "add2 i Zero = i"
+  | "add2 i (Succ j) = Succ (add2 i j)"
+  | "add2 i (Lim f) = Lim (\<lambda>n. add2 i (f n))"
+  by pat_completeness auto
+termination
+  by (relation "inv_image brouwer_order snd") auto
+
+lemma add2_assoc: "add2 (add2 i j) k = add2 i (add2 j k)"
+  by (induct k) auto
+
+end
diff -r fcd599570afa -r 1070be576372 src/HOL/Induct/Tree.thy
--- a/src/HOL/Induct/Tree.thy	Sun Apr 23 14:53:35 2017 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,107 +0,0 @@
-(*  Title:      HOL/Induct/Tree.thy
-    Author:     Stefan Berghofer,  TU Muenchen
-    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
-*)
-
-section \<open>Infinitely branching trees\<close>
-
-theory Tree
-imports Main
-begin
-
-datatype 'a tree =
-    Atom 'a
-  | Branch "nat \<Rightarrow> 'a tree"
-
-primrec map_tree :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a tree \<Rightarrow> 'b tree"
-where
-  "map_tree f (Atom a) = Atom (f a)"
-| "map_tree f (Branch ts) = Branch (\<lambda>x. map_tree f (ts x))"
-
-lemma tree_map_compose: "map_tree g (map_tree f t) = map_tree (g \<circ> f) t"
-  by (induct t) simp_all
-
-primrec exists_tree :: "('a \<Rightarrow> bool) \<Rightarrow> 'a tree \<Rightarrow> bool"
-where
-  "exists_tree P (Atom a) = P a"
-| "exists_tree P (Branch ts) = (\<exists>x. exists_tree P (ts x))"
-
-lemma exists_map:
-  "(\<And>x. P x \<Longrightarrow> Q (f x)) \<Longrightarrow>
-    exists_tree P ts \<Longrightarrow> exists_tree Q (map_tree f ts)"
-  by (induct ts) auto
-
-
-subsection\<open>The Brouwer ordinals, as in ZF/Induct/Brouwer.thy.\<close>
-
-datatype brouwer = Zero | Succ brouwer | Lim "nat \<Rightarrow> brouwer"
-
-text \<open>Addition of ordinals\<close>
-primrec add :: "brouwer \<Rightarrow> brouwer \<Rightarrow> brouwer"
-where
-  "add i Zero = i"
-| "add i (Succ j) = Succ (add i j)"
-| "add i (Lim f) = Lim (\<lambda>n. add i (f n))"
-
-lemma add_assoc: "add (add i j) k = add i (add j k)"
-  by (induct k) auto
-
-text \<open>Multiplication of ordinals\<close>
-primrec mult :: "brouwer \<Rightarrow> brouwer \<Rightarrow> brouwer"
-where
-  "mult i Zero = Zero"
-| "mult i (Succ j) = add (mult i j) i"
-| "mult i (Lim f) = Lim (\<lambda>n. mult i (f n))"
-
-lemma add_mult_distrib: "mult i (add j k) = add (mult i j) (mult i k)"
-  by (induct k) (auto simp add: add_assoc)
-
-lemma mult_assoc: "mult (mult i j) k = mult i (mult j k)"
-  by (induct k) (auto simp add: add_mult_distrib)
-
-text \<open>We could probably instantiate some axiomatic type classes and use
-  the standard infix operators.\<close>
-
-
-subsection \<open>A WF Ordering for The Brouwer ordinals (Michael Compton)\<close>
-
-text \<open>To use the function package we need an ordering on the Brouwer
-  ordinals.  Start with a predecessor relation and form its transitive
-  closure.\<close>
-
-definition brouwer_pred :: "(brouwer \<times> brouwer) set"
-  where "brouwer_pred = (\<Union>i. {(m, n). n = Succ m \<or> (\<exists>f. n = Lim f \<and> m = f i)})"
-
-definition brouwer_order :: "(brouwer \<times> brouwer) set"
-  where "brouwer_order = brouwer_pred^+"
-
-lemma wf_brouwer_pred: "wf brouwer_pred"
-  unfolding wf_def brouwer_pred_def
-  apply clarify
-  apply (induct_tac x)
-  apply blast+
-  done
-
-lemma wf_brouwer_order[simp]: "wf brouwer_order"
-  unfolding brouwer_order_def
-  by (rule wf_trancl[OF wf_brouwer_pred])
-
-lemma [simp]: "(j, Succ j) \<in> brouwer_order"
-  by (auto simp add: brouwer_order_def brouwer_pred_def)
-
-lemma [simp]: "(f n, Lim f) \<in> brouwer_order"
-  by (auto simp add: brouwer_order_def brouwer_pred_def)
-
-text \<open>Example of a general function\<close>
-function add2 :: "brouwer \<Rightarrow> brouwer \<Rightarrow> brouwer"
-where
-  "add2 i Zero = i"
-| "add2 i (Succ j) = Succ (add2 i j)"
-| "add2 i (Lim f) = Lim (\<lambda>n. add2 i (f n))"
-by pat_completeness auto
-termination by (relation "inv_image brouwer_order snd") auto
-
-lemma add2_assoc: "add2 (add2 i j) k = add2 i (add2 j k)"
-  by (induct k) auto
-
-end
diff -r fcd599570afa -r 1070be576372 src/HOL/ROOT
--- a/src/HOL/ROOT	Sun Apr 23 14:53:35 2017 +0200
+++ b/src/HOL/ROOT	Sun Apr 23 23:10:33 2017 +0200
@@ -128,7 +128,7 @@
     Term
     SList
     ABexp
-    Tree
+    Infinitely_Branching_Tree
     Ordinals
     Sigma_Algebra
     Comb
@@ -565,6 +565,7 @@
     Bubblesort
     CTL
     Cartouche_Examples
+    Case_Product
     Chinese
     Classical
     Code_Binary_Nat_examples
diff -r fcd599570afa -r 1070be576372 src/HOL/ex/Case_Product.thy
--- a/src/HOL/ex/Case_Product.thy	Sun Apr 23 14:53:35 2017 +0200
+++ b/src/HOL/ex/Case_Product.thy	Sun Apr 23 23:10:33 2017 +0200
@@ -10,21 +10,17 @@
 begin
 
 text \<open>
-  The {@attribute case_product} attribute combines multiple case distinction
+  The @{attribute case_product} attribute combines multiple case distinction
   lemmas into a single case distinction lemma by building the product of all
   these case distinctions.
 \<close>
 
-lemmas nat_list_exhaust = nat.exhaust[case_product list.exhaust]
+lemmas nat_list_exhaust = nat.exhaust [case_product list.exhaust]
 
-text \<open>
-  The attribute honors preconditions
-\<close>
+text \<open>The attribute honours preconditions.\<close>
 
-lemmas trancl_acc_cases= trancl.cases[case_product acc.cases]
+lemmas trancl_acc_cases = trancl.cases [case_product acc.cases]
 
-text \<open>
-  Also, case names are generated based on the old names
-\<close>
+text \<open>Also, case names are generated based on the old names.\<close>
 
 end
diff -r fcd599570afa -r 1070be576372 src/Pure/General/mercurial.scala
--- a/src/Pure/General/mercurial.scala	Sun Apr 23 14:53:35 2017 +0200
+++ b/src/Pure/General/mercurial.scala	Sun Apr 23 23:10:33 2017 +0200
@@ -35,6 +35,19 @@
     hg
   }
 
+  def find_repository(start: Path, ssh: Option[SSH.Session] = None): Option[Repository] =
+  {
+    def find(root: Path): Option[Repository] =
+      if (is_repository(root, ssh)) Some(repository(root, ssh = ssh))
+      else if (root.is_root) None
+      else find(root + Path.parent)
+
+    ssh match {
+      case None => find(start.expand)
+      case Some(ssh) => find(ssh.expand_path(start))
+    }
+  }
+
   def clone_repository(
     source: String, root: Path, options: String = "", ssh: Option[SSH.Session] = None): Repository =
   {
diff -r fcd599570afa -r 1070be576372 src/Pure/General/path.scala
--- a/src/Pure/General/path.scala	Sun Apr 23 14:53:35 2017 +0200
+++ b/src/Pure/General/path.scala	Sun Apr 23 23:10:33 2017 +0200
@@ -119,6 +119,7 @@
 {
   def is_current: Boolean = elems.isEmpty
   def is_absolute: Boolean = elems.nonEmpty && elems.last.isInstanceOf[Path.Root]
+  def is_root: Boolean = elems match { case List(Path.Root(_)) => true case _ => false }
   def is_basic: Boolean = elems match { case List(Path.Basic(_)) => true case _ => false }
 
   def +(other: Path): Path = new Path((other.elems :\ elems)(Path.apply_elem))
diff -r fcd599570afa -r 1070be576372 src/Pure/System/isabelle_tool.scala
--- a/src/Pure/System/isabelle_tool.scala	Sun Apr 23 14:53:35 2017 +0200
+++ b/src/Pure/System/isabelle_tool.scala	Sun Apr 23 23:10:33 2017 +0200
@@ -108,6 +108,7 @@
       Build_Stats.isabelle_tool,
       Check_Sources.isabelle_tool,
       Doc.isabelle_tool,
+      Imports.isabelle_tool,
       ML_Process.isabelle_tool,
       NEWS.isabelle_tool,
       Options.isabelle_tool,
@@ -115,7 +116,6 @@
       Remote_DMG.isabelle_tool,
       Update_Cartouches.isabelle_tool,
       Update_Header.isabelle_tool,
-      Update_Imports.isabelle_tool,
       Update_Then.isabelle_tool,
       Update_Theorems.isabelle_tool,
       isabelle.vscode.Build_VSCode.isabelle_tool,
diff -r fcd599570afa -r 1070be576372 src/Pure/Thy/sessions.scala
--- a/src/Pure/Thy/sessions.scala	Sun Apr 23 14:53:35 2017 +0200
+++ b/src/Pure/Thy/sessions.scala	Sun Apr 23 23:10:33 2017 +0200
@@ -274,8 +274,7 @@
     val selected_sessions = full_sessions.selection(Selection(sessions = List(session)))._2
 
     if (all_known) {
-      val deps = Sessions.deps(
-        full_sessions, global_theories = global_theories, all_known = all_known)
+      val deps = Sessions.deps(full_sessions, global_theories = global_theories, all_known = true)
       deps(session).copy(known = deps.all_known)
     }
     else
@@ -449,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(_))
 
@@ -629,6 +631,12 @@
     if (is_session_dir(dir)) File.pwd() + dir.expand
     else error("Bad session root directory: " + dir.toString)
 
+  def directories(dirs: List[Path], select_dirs: List[Path]): List[(Boolean, Path)] =
+  {
+    val default_dirs = Isabelle_System.components().filter(is_session_dir(_))
+    (default_dirs ::: dirs).map((false, _)) ::: select_dirs.map((true, _))
+  }
+
   def load(options: Options, dirs: List[Path] = Nil, select_dirs: List[Path] = Nil): T =
   {
     def load_dir(select: Boolean, dir: Path): List[(String, Info)] =
@@ -656,11 +664,9 @@
       else Nil
     }
 
-    val default_dirs = Isabelle_System.components().filter(is_session_dir(_))
-
     make(
       for {
-        (select, dir) <- (default_dirs ::: dirs).map((false, _)) ::: select_dirs.map((true, _))
+        (select, dir) <- directories(dirs, select_dirs)
         info <- load_dir(select, check_session_dir(dir))
       } yield info)
   }
diff -r fcd599570afa -r 1070be576372 src/Pure/Tools/imports.scala
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/Tools/imports.scala	Sun Apr 23 23:10:33 2017 +0200
@@ -0,0 +1,273 @@
+/*  Title:      Pure/Tools/imports.scala
+    Author:     Makarius
+
+Maintain theory imports wrt. session structure.
+*/
+
+package isabelle
+
+
+import java.io.{File => JFile}
+
+
+object Imports
+{
+  /* manifest */
+
+  def manifest_files(start: Path, pred: JFile => Boolean = _ => true): List[JFile] =
+    Mercurial.find_repository(start) match {
+      case None =>
+        Output.warning("Ignoring directory " + start + " (no Mercurial repository)")
+        Nil
+      case Some(hg) =>
+        val start_path = start.file.getCanonicalFile.toPath
+        for {
+          name <- hg.manifest()
+          file = (hg.root + Path.explode(name)).file
+          if pred(file) && file.getCanonicalFile.toPath.startsWith(start_path)
+        } yield file
+    }
+
+
+  /* update imports */
+
+  sealed case class Update(range: Text.Range, old_text: String, new_text: String)
+  {
+    def edits: List[Text.Edit] =
+      Text.Edit.replace(range.start, old_text, new_text)
+
+    override def toString: String =
+      range.toString + ": " + old_text + " -> " + new_text
+  }
+
+  def update_name(keywords: Keyword.Keywords, pos: Position.T, update: String => String)
+    : Option[(JFile, Update)] =
+  {
+    val file =
+      pos match {
+        case Position.File(file) => Path.explode(file).file.getCanonicalFile
+        case _ => error("Missing file in position" + Position.here(pos))
+      }
+
+    val text = File.read(file)
+
+    val range =
+      pos match {
+        case Position.Range(symbol_range) => Symbol.Text_Chunk(text).decode(symbol_range)
+        case _ => error("Missing range in position" + Position.here(pos))
+      }
+
+    Token.read_name(keywords, range.substring(text)) match {
+      case Some(tok) =>
+        val s1 = tok.source
+        val s2 = Token.quote_name(keywords, update(tok.content))
+        if (s1 == s2) None else Some((file, Update(range, s1, s2)))
+      case None => error("Name token expected" + Position.here(pos))
+    }
+  }
+
+
+  /* collective operations */
+
+  def imports(
+    options: Options,
+    operation_imports: Boolean = false,
+    operation_manifest: Boolean = false,
+    operation_update: Boolean = false,
+    progress: Progress = No_Progress,
+    selection: Sessions.Selection = Sessions.Selection.empty,
+    dirs: List[Path] = Nil,
+    select_dirs: List[Path] = Nil,
+    verbose: Boolean = false) =
+  {
+    val full_sessions = Sessions.load(options, dirs, select_dirs)
+    val (selected, selected_sessions) = full_sessions.selection(selection)
+
+    val deps =
+      Sessions.deps(selected_sessions, progress = progress, verbose = verbose,
+        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 =
+        for {
+          (_, dir) <- Sessions.directories(dirs, select_dirs)
+          file <- manifest_files(dir, file => file.getName.endsWith(".thy"))
+          if deps.all_known.get_file(file).isEmpty
+        } yield file
+      unused_files.foreach(file => progress.echo("unused file " + quote(file.toString)))
+    }
+
+    if (operation_update) {
+      progress.echo("\nUpdate theory imports:")
+      val updates =
+        selected.flatMap(session_name =>
+        {
+          val info = full_sessions(session_name)
+          val session_base = deps(session_name)
+          val session_resources = new Resources(session_base)
+          val imports_resources = new Resources(session_base.get_imports)
+
+          def standard_import(qualifier: String, dir: String, s: String): String =
+          {
+            val name = imports_resources.import_name(qualifier, dir, s)
+            val file = Path.explode(name.node).file
+            val s1 =
+              imports_resources.session_base.known.get_file(file) match {
+                case Some(name1) if session_resources.theory_qualifier(name1) != qualifier =>
+                  name1.theory
+                case Some(name1) if Thy_Header.is_base_name(s) =>
+                  name1.theory_base_name
+                case _ => s
+              }
+            val name2 = imports_resources.import_name(qualifier, dir, s1)
+            if (name.node == name2.node) s1 else s
+          }
+
+          val updates_root =
+            for {
+              (_, pos) <- info.theories.flatMap(_._2)
+              upd <- update_name(root_keywords, pos,
+                standard_import(info.theory_qualifier, info.dir.implode, _))
+            } yield upd
+
+          val updates_theories =
+            for {
+              (_, name) <- session_base.known.theories_local.toList
+              (_, pos) <- session_resources.check_thy(name, Token.Pos.file(name.node)).imports
+              upd <- update_name(session_base.syntax.keywords, pos,
+                standard_import(session_resources.theory_qualifier(name), name.master_dir, _))
+            } yield upd
+
+          updates_root ::: updates_theories
+        })
+
+      val file_updates = (Multi_Map.empty[JFile, Update] /: updates)(_ + _)
+      val conflicts =
+        file_updates.iterator_list.flatMap({ case (file, upds) =>
+          Library.duplicates(upds.sortBy(_.range.start),
+            (x: Update, y: Update) => x.range overlaps y.range) match
+          {
+            case Nil => None
+            case bad => Some((file, bad))
+          }
+        })
+      if (conflicts.nonEmpty)
+        error(cat_lines(
+          conflicts.map({ case (file, bad) =>
+            "Conflicting updates for file " + file + bad.mkString("\n  ", "\n  ", "") })))
+
+      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 =>
+            Text.Edit.replace(upd.range.start, upd.old_text, upd.new_text))
+        val new_text =
+          (File.read(file) /: edits)({ case (text, edit) =>
+            edit.edit(text, 0) match {
+              case (None, text1) => text1
+              case (Some(_), _) => error("Failed to apply edit " + edit + " to file " + file)
+            }
+          })
+        File.write_backup2(Path.explode(File.standard_path(file)), new_text)
+      }
+    }
+  }
+
+
+  /* Isabelle tool wrapper */
+
+  val isabelle_tool =
+    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
+      var exclude_session_groups: List[String] = Nil
+      var all_sessions = false
+      var dirs: List[Path] = Nil
+      var session_groups: List[String] = Nil
+      var options = Options.init()
+      var verbose = false
+      var exclude_sessions: List[String] = Nil
+
+      val getopts = Getopts("""
+Usage: isabelle imports [OPTIONS] [SESSIONS ...]
+
+  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
+    -X NAME      exclude sessions from group NAME and all descendants
+    -a           select all sessions
+    -d DIR       include session directory
+    -g NAME      select session group NAME
+    -o OPTION    override Isabelle system OPTION (via NAME=VAL or NAME)
+    -v           verbose
+    -x NAME      exclude session NAME and all descendants
+
+  Maintain theory imports wrt. session structure. At least one operation
+  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),
+      "X:" -> (arg => exclude_session_groups = exclude_session_groups ::: List(arg)),
+      "a" -> (_ => all_sessions = true),
+      "d:" -> (arg => dirs = dirs ::: List(Path.explode(arg))),
+      "g:" -> (arg => session_groups = session_groups ::: List(arg)),
+      "o:" -> (arg => options = options + arg),
+      "v" -> (_ => verbose = true),
+      "x:" -> (arg => exclude_sessions = exclude_sessions ::: List(arg)))
+
+      val sessions = getopts(args)
+      if (args.isEmpty || !(operation_imports || operation_manifest || operation_update))
+        getopts.usage()
+
+      val selection =
+        Sessions.Selection(requirements, all_sessions, exclude_session_groups,
+          exclude_sessions, session_groups, sessions)
+
+      val progress = new Console_Progress(verbose = verbose)
+
+      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)
+    })
+}
diff -r fcd599570afa -r 1070be576372 src/Pure/Tools/update_imports.scala
--- a/src/Pure/Tools/update_imports.scala	Sun Apr 23 14:53:35 2017 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,206 +0,0 @@
-/*  Title:      Pure/Tools/update_imports.scala
-    Author:     Makarius
-
-Update theory imports to use session qualifiers.
-*/
-
-package isabelle
-
-
-import java.io.{File => JFile}
-
-
-object Update_Imports
-{
-  /* update imports */
-
-  sealed case class Update(range: Text.Range, old_text: String, new_text: String)
-  {
-    def edits: List[Text.Edit] =
-      Text.Edit.replace(range.start, old_text, new_text)
-
-    override def toString: String =
-      range.toString + ": " + old_text + " -> " + new_text
-  }
-
-  def update_name(keywords: Keyword.Keywords, pos: Position.T, update: String => String)
-    : Option[(JFile, Update)] =
-  {
-    val file =
-      pos match {
-        case Position.File(file) => Path.explode(file).file.getCanonicalFile
-        case _ => error("Missing file in position" + Position.here(pos))
-      }
-
-    val text = File.read(file)
-
-    val range =
-      pos match {
-        case Position.Range(symbol_range) => Symbol.Text_Chunk(text).decode(symbol_range)
-        case _ => error("Missing range in position" + Position.here(pos))
-      }
-
-    Token.read_name(keywords, range.substring(text)) match {
-      case Some(tok) =>
-        val s1 = tok.source
-        val s2 = Token.quote_name(keywords, update(tok.content))
-        if (s1 == s2) None else Some((file, Update(range, s1, s2)))
-      case None => error("Name token expected" + Position.here(pos))
-    }
-  }
-
-  def update_imports(
-    options: Options,
-    progress: Progress = No_Progress,
-    selection: Sessions.Selection = Sessions.Selection.empty,
-    dirs: List[Path] = Nil,
-    select_dirs: List[Path] = Nil,
-    verbose: Boolean = false): List[(JFile, Update)] =
-  {
-    val full_sessions = Sessions.load(options, dirs, select_dirs)
-    val (selected, selected_sessions) = full_sessions.selection(selection)
-
-    val deps =
-      Sessions.deps(selected_sessions, progress = progress, verbose = verbose,
-        global_theories = full_sessions.global_theories)
-
-    selected.flatMap(session_name =>
-    {
-      val info = full_sessions(session_name)
-      val session_base = deps(session_name)
-      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)
-        val file = Path.explode(name.node).file
-        val s1 =
-          imports_resources.session_base.known.get_file(file) match {
-            case Some(name1) if session_resources.theory_qualifier(name1) != qualifier =>
-              name1.theory
-            case Some(name1) if Thy_Header.is_base_name(s) =>
-              name1.theory_base_name
-            case _ => s
-          }
-        val name2 = imports_resources.import_name(qualifier, dir, s1)
-        if (name.node == name2.node) s1 else s
-      }
-
-      val updates_root =
-        for {
-          (_, pos) <- info.theories.flatMap(_._2)
-          upd <- update_name(Sessions.root_syntax.keywords, pos,
-            standard_import(info.theory_qualifier, info.dir.implode, _))
-        } yield upd
-
-      val updates_theories =
-        for {
-          (_, name) <- session_base.known.theories_local.toList
-          (_, pos) <- session_resources.check_thy(name, Token.Pos.file(name.node)).imports
-          upd <- update_name(session_base.syntax.keywords, pos,
-            standard_import(session_resources.theory_qualifier(name), name.master_dir, _))
-        } yield upd
-
-      updates_root ::: updates_theories
-    })
-  }
-
-  def apply_updates(updates: List[(JFile, Update)])
-  {
-    val file_updates = (Multi_Map.empty[JFile, Update] /: updates)(_ + _)
-    val conflicts =
-      file_updates.iterator_list.flatMap({ case (file, upds) =>
-        Library.duplicates(upds.sortBy(_.range.start),
-          (x: Update, y: Update) => x.range overlaps y.range) match
-        {
-          case Nil => None
-          case bad => Some((file, bad))
-        }
-      })
-    if (conflicts.nonEmpty)
-      error(cat_lines(
-        conflicts.map({ case (file, bad) =>
-          "Conflicting updates for file " + file + bad.mkString("\n  ", "\n  ", "") })))
-
-    for ((file, upds) <- file_updates.iterator_list) {
-      val edits =
-        upds.sortBy(upd => - upd.range.start).flatMap(upd =>
-          Text.Edit.replace(upd.range.start, upd.old_text, upd.new_text))
-      val new_text =
-        (File.read(file) /: edits)({ case (text, edit) =>
-          edit.edit(text, 0) match {
-            case (None, text1) => text1
-            case (Some(_), _) => error("Failed to apply edit " + edit + " to file " + file)
-          }
-        })
-      File.write_backup2(Path.explode(File.standard_path(file)), new_text)
-    }
-  }
-
-
-  /* Isabelle tool wrapper */
-
-  val isabelle_tool =
-    Isabelle_Tool("update_imports", "update theory imports to use session qualifiers", args =>
-    {
-      var select_dirs: List[Path] = Nil
-      var requirements = false
-      var exclude_session_groups: List[String] = Nil
-      var all_sessions = false
-      var dirs: List[Path] = Nil
-      var session_groups: List[String] = Nil
-      var options = Options.init()
-      var verbose = false
-      var exclude_sessions: List[String] = Nil
-
-      val getopts = Getopts("""
-Usage: isabelle update_imports [OPTIONS] [SESSIONS ...]
-
-  Options are:
-    -D DIR       include session directory and select its sessions
-    -R           operate on requirements of selected sessions
-    -X NAME      exclude sessions from group NAME and all descendants
-    -a           select all sessions
-    -d DIR       include session directory
-    -g NAME      select session group NAME
-    -o OPTION    override Isabelle system OPTION (via NAME=VAL or NAME)
-    -v           verbose
-    -x NAME      exclude session NAME and all descendants
-
-  Update theory imports to use session qualifiers.
-
-  Old versions of files are preserved by appending "~~".
-""",
-      "D:" -> (arg => select_dirs = select_dirs ::: List(Path.explode(arg))),
-      "R" -> (_ => requirements = true),
-      "X:" -> (arg => exclude_session_groups = exclude_session_groups ::: List(arg)),
-      "a" -> (_ => all_sessions = true),
-      "d:" -> (arg => dirs = dirs ::: List(Path.explode(arg))),
-      "g:" -> (arg => session_groups = session_groups ::: List(arg)),
-      "o:" -> (arg => options = options + arg),
-      "v" -> (_ => verbose = true),
-      "x:" -> (arg => exclude_sessions = exclude_sessions ::: List(arg)))
-
-      val sessions = getopts(args)
-      if (args.isEmpty) getopts.usage()
-
-      val selection =
-        Sessions.Selection(requirements, all_sessions, exclude_session_groups,
-          exclude_sessions, session_groups, sessions)
-
-      val progress = new Console_Progress(verbose = verbose)
-
-      val updates =
-        update_imports(options, progress = progress, selection = selection,
-          dirs = dirs, select_dirs = select_dirs, verbose = verbose)
-
-      apply_updates(updates)
-    })
-}
diff -r fcd599570afa -r 1070be576372 src/Pure/build-jars
--- a/src/Pure/build-jars	Sun Apr 23 14:53:35 2017 +0200
+++ b/src/Pure/build-jars	Sun Apr 23 23:10:33 2017 +0200
@@ -135,6 +135,7 @@
   Tools/check_keywords.scala
   Tools/debugger.scala
   Tools/doc.scala
+  Tools/imports.scala
   Tools/main.scala
   Tools/print_operation.scala
   Tools/profiling_report.scala
@@ -143,7 +144,6 @@
   Tools/task_statistics.scala
   Tools/update_cartouches.scala
   Tools/update_header.scala
-  Tools/update_imports.scala
   Tools/update_then.scala
   Tools/update_theorems.scala
   library.scala