src/Doc/System/Sessions.thy

   Inform about the status of all sessions required for AFP, without building
   anything yet:
   @{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