# HG changeset patch
# User wenzelm
# Date 1505662660 -7200
# Node ID 41b64e53b6a16ada59b74683ed04ede268e49414
# Parent  e5188cb1c3d83d1179e6e4e9d23e15681a129215
more documentation;
tuned message;

diff -r e5188cb1c3d8 -r 41b64e53b6a1 NEWS
--- a/NEWS	Sat Sep 16 17:25:51 2017 +0200
+++ b/NEWS	Sun Sep 17 17:37:40 2017 +0200
@@ -306,7 +306,7 @@
 serves as example for alternative PIDE front-ends.
 
 * Command-line tool "isabelle imports" helps to maintain theory imports
-wrt. session structure. Examples:
+wrt. session structure. Examples for the main Isabelle distribution:
 
   isabelle imports -I -a
   isabelle imports -U -a
diff -r e5188cb1c3d8 -r 41b64e53b6a1 src/Doc/System/Sessions.thy
--- a/src/Doc/System/Sessions.thy	Sat Sep 16 17:25:51 2017 +0200
+++ b/src/Doc/System/Sessions.thy	Sun Sep 17 17:37:40 2017 +0200
@@ -440,4 +440,82 @@
   @{verbatim [display] \<open>isabelle build -D '$AFP' -R -v -n\<close>}
 \<close>
 
+
+section \<open>Maintain theory imports wrt.\ session structure\<close>
+
+text \<open>
+  The @{tool_def "imports"} tool helps to maintain theory imports wrt.\
+  session structure. It supports three main operations via options \<^verbatim>\<open>-I\<close>,
+  \<^verbatim>\<open>-M\<close>, \<^verbatim>\<open>-U\<close>. Its command-line usage is: @{verbatim [display]
+\<open>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 repository check for 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
+    -i           incremental update according to session graph structure
+    -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).\<close>}
+
+  \<^medskip>
+  The selection of sessions and session directories works as for @{tool build}
+  via options \<^verbatim>\<open>-D\<close>, \<^verbatim>\<open>-R\<close>, \<^verbatim>\<open>-X\<close>, \<^verbatim>\<open>-a\<close>, \<^verbatim>\<open>-d\<close>, \<^verbatim>\<open>-g\<close>, \<^verbatim>\<open>-x\<close> (see
+  \secref{sec:tool-build}).
+
+  \<^medskip>
+  Option \<^verbatim>\<open>-o\<close> overrides Isabelle system options as for @{tool build}
+  (see \secref{sec:tool-build}).
+
+  \<^medskip>
+  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.
+
+  \<^medskip>
+  Option \<^verbatim>\<open>-M\<close> checks imported theories against the Mercurial repositories of
+  the underlying session directories; non-repository directories are ignored.
+  This helps to find files that are accidentally ignored, e.g.\ due to
+  rearrangements of the session structure.
+
+  \<^medskip>
+  Option \<^verbatim>\<open>-U\<close> updates theory imports with old-style directory specifications
+  to canonical session-qualified theory names, according to the theory name
+  space imported via \isakeyword{sessions} within the \<^verbatim>\<open>ROOT\<close> specification.
+
+  Option \<^verbatim>\<open>-i\<close> modifies the meaning of option \<^verbatim>\<open>-U\<close> to proceed incrementally,
+  following to the session graph structure in bottom-up order. This may
+  lead to more accurate results in complex session hierarchies.
+\<close>
+
+subsubsection \<open>Examples\<close>
+
+text \<open>
+  Determine potential session imports for some project directory:
+  @{verbatim [display] \<open>isabelle imports -I -D 'some/where/My_Project'\<close>}
+
+  \<^smallskip>
+  Mercurial repository check for some project directory:
+  @{verbatim [display] \<open>isabelle imports -M -D 'some/where/My_Project'\<close>}
+
+  \<^smallskip>
+  Incremental update of theory imports for some project directory:
+  @{verbatim [display] \<open>isabelle imports -U -i -D 'some/where/My_Project'\<close>}
+\<close>
+
 end
diff -r e5188cb1c3d8 -r 41b64e53b6a1 src/Pure/Tools/imports.scala
--- a/src/Pure/Tools/imports.scala	Sat Sep 16 17:25:51 2017 +0200
+++ b/src/Pure/Tools/imports.scala	Sun Sep 17 17:37:40 2017 +0200
@@ -119,7 +119,7 @@
     }
 
     if (operation_repository_files) {
-      progress.echo("\nMercurial files check:")
+      progress.echo("\nMercurial repository check:")
       val unused_files =
         for {
           (_, dir) <- Sessions.directories(dirs, select_dirs)
@@ -235,7 +235,7 @@
   Options are:
     -D DIR       include session directory and select its sessions
     -I           operation: report potential session imports
-    -M           operation: Mercurial files check for imported theory files
+    -M           operation: Mercurial repository check for 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