--- 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