more documentation;
authorwenzelm
Sun Sep 17 17:37:40 2017 +0200 (20 months ago)
changeset 6667141b64e53b6a1
parent 66670 e5188cb1c3d8
child 66672 75694b28ef08
more documentation;
tuned message;
NEWS
src/Doc/System/Sessions.thy
src/Pure/Tools/imports.scala
     1.1 --- a/NEWS	Sat Sep 16 17:25:51 2017 +0200
     1.2 +++ b/NEWS	Sun Sep 17 17:37:40 2017 +0200
     1.3 @@ -306,7 +306,7 @@
     1.4  serves as example for alternative PIDE front-ends.
     1.5  
     1.6  * Command-line tool "isabelle imports" helps to maintain theory imports
     1.7 -wrt. session structure. Examples:
     1.8 +wrt. session structure. Examples for the main Isabelle distribution:
     1.9  
    1.10    isabelle imports -I -a
    1.11    isabelle imports -U -a
     2.1 --- a/src/Doc/System/Sessions.thy	Sat Sep 16 17:25:51 2017 +0200
     2.2 +++ b/src/Doc/System/Sessions.thy	Sun Sep 17 17:37:40 2017 +0200
     2.3 @@ -440,4 +440,82 @@
     2.4    @{verbatim [display] \<open>isabelle build -D '$AFP' -R -v -n\<close>}
     2.5  \<close>
     2.6  
     2.7 +
     2.8 +section \<open>Maintain theory imports wrt.\ session structure\<close>
     2.9 +
    2.10 +text \<open>
    2.11 +  The @{tool_def "imports"} tool helps to maintain theory imports wrt.\
    2.12 +  session structure. It supports three main operations via options \<^verbatim>\<open>-I\<close>,
    2.13 +  \<^verbatim>\<open>-M\<close>, \<^verbatim>\<open>-U\<close>. Its command-line usage is: @{verbatim [display]
    2.14 +\<open>Usage: isabelle imports [OPTIONS] [SESSIONS ...]
    2.15 +
    2.16 +  Options are:
    2.17 +    -D DIR       include session directory and select its sessions
    2.18 +    -I           operation: report potential session imports
    2.19 +    -M           operation: Mercurial repository check for theory files
    2.20 +    -R           operate on requirements of selected sessions
    2.21 +    -U           operation: update theory imports to use session qualifiers
    2.22 +    -X NAME      exclude sessions from group NAME and all descendants
    2.23 +    -a           select all sessions
    2.24 +    -d DIR       include session directory
    2.25 +    -g NAME      select session group NAME
    2.26 +    -i           incremental update according to session graph structure
    2.27 +    -o OPTION    override Isabelle system OPTION (via NAME=VAL or NAME)
    2.28 +    -v           verbose
    2.29 +    -x NAME      exclude session NAME and all descendants
    2.30 +
    2.31 +  Maintain theory imports wrt. session structure. At least one operation
    2.32 +  needs to be specified (see options -I -M -U).\<close>}
    2.33 +
    2.34 +  \<^medskip>
    2.35 +  The selection of sessions and session directories works as for @{tool build}
    2.36 +  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
    2.37 +  \secref{sec:tool-build}).
    2.38 +
    2.39 +  \<^medskip>
    2.40 +  Option \<^verbatim>\<open>-o\<close> overrides Isabelle system options as for @{tool build}
    2.41 +  (see \secref{sec:tool-build}).
    2.42 +
    2.43 +  \<^medskip>
    2.44 +  Option \<^verbatim>\<open>-v\<close> increases the general level of verbosity.
    2.45 +
    2.46 +  \<^medskip>
    2.47 +  Option \<^verbatim>\<open>-I\<close> determines potential session imports, which may be turned into
    2.48 +  \isakeyword{sessions} within the corresponding \<^verbatim>\<open>ROOT\<close> file entry. Thus
    2.49 +  theory imports from other sessions may use session-qualified names. For
    2.50 +  example, adhoc \<^theory_text>\<open>imports\<close> \<^verbatim>\<open>"~~/src/HOL/Library/Multiset"\<close> may become formal
    2.51 +  \<^theory_text>\<open>imports\<close> \<^verbatim>\<open>"HOL-Library.Multiset"\<close> after adding \isakeyword{sessions}
    2.52 +  \<^verbatim>\<open>"HOL-Library"\<close> to the \<^verbatim>\<open>ROOT\<close> entry.
    2.53 +
    2.54 +  \<^medskip>
    2.55 +  Option \<^verbatim>\<open>-M\<close> checks imported theories against the Mercurial repositories of
    2.56 +  the underlying session directories; non-repository directories are ignored.
    2.57 +  This helps to find files that are accidentally ignored, e.g.\ due to
    2.58 +  rearrangements of the session structure.
    2.59 +
    2.60 +  \<^medskip>
    2.61 +  Option \<^verbatim>\<open>-U\<close> updates theory imports with old-style directory specifications
    2.62 +  to canonical session-qualified theory names, according to the theory name
    2.63 +  space imported via \isakeyword{sessions} within the \<^verbatim>\<open>ROOT\<close> specification.
    2.64 +
    2.65 +  Option \<^verbatim>\<open>-i\<close> modifies the meaning of option \<^verbatim>\<open>-U\<close> to proceed incrementally,
    2.66 +  following to the session graph structure in bottom-up order. This may
    2.67 +  lead to more accurate results in complex session hierarchies.
    2.68 +\<close>
    2.69 +
    2.70 +subsubsection \<open>Examples\<close>
    2.71 +
    2.72 +text \<open>
    2.73 +  Determine potential session imports for some project directory:
    2.74 +  @{verbatim [display] \<open>isabelle imports -I -D 'some/where/My_Project'\<close>}
    2.75 +
    2.76 +  \<^smallskip>
    2.77 +  Mercurial repository check for some project directory:
    2.78 +  @{verbatim [display] \<open>isabelle imports -M -D 'some/where/My_Project'\<close>}
    2.79 +
    2.80 +  \<^smallskip>
    2.81 +  Incremental update of theory imports for some project directory:
    2.82 +  @{verbatim [display] \<open>isabelle imports -U -i -D 'some/where/My_Project'\<close>}
    2.83 +\<close>
    2.84 +
    2.85  end
     3.1 --- a/src/Pure/Tools/imports.scala	Sat Sep 16 17:25:51 2017 +0200
     3.2 +++ b/src/Pure/Tools/imports.scala	Sun Sep 17 17:37:40 2017 +0200
     3.3 @@ -119,7 +119,7 @@
     3.4      }
     3.5  
     3.6      if (operation_repository_files) {
     3.7 -      progress.echo("\nMercurial files check:")
     3.8 +      progress.echo("\nMercurial repository check:")
     3.9        val unused_files =
    3.10          for {
    3.11            (_, dir) <- Sessions.directories(dirs, select_dirs)
    3.12 @@ -235,7 +235,7 @@
    3.13    Options are:
    3.14      -D DIR       include session directory and select its sessions
    3.15      -I           operation: report potential session imports
    3.16 -    -M           operation: Mercurial files check for imported theory files
    3.17 +    -M           operation: Mercurial repository check for theory files
    3.18      -R           operate on requirements of selected sessions
    3.19      -U           operation: update theory imports to use session qualifiers
    3.20      -X NAME      exclude sessions from group NAME and all descendants