--- a/doc-src/System/Thy/Sessions.thy Thu Aug 23 13:03:29 2012 +0200
+++ b/doc-src/System/Thy/Sessions.thy Thu Aug 23 13:26:27 2012 +0200
@@ -189,6 +189,7 @@
-d DIR include session directory
-g NAME select session group NAME
-j INT maximum number of parallel jobs (default 1)
+ -l list session source files
-n no build -- test dependencies only
-o OPTION override session configuration OPTION
(via NAME=VAL or NAME)
@@ -265,7 +266,9 @@
@{setting ISABELLE_OUTPUT} (which is normally in @{setting
ISABELLE_HOME_USER}, i.e.\ the user's home directory).
- \medskip Option @{verbatim "-v"} enables verbose mode.
+ \medskip Option @{verbatim "-v"} increases the general level of
+ verbosity. Option @{verbatim "-l"} lists the source files that
+ contribute to a session.
*}
subsubsection {* Examples *}
--- a/doc-src/System/Thy/document/Sessions.tex Thu Aug 23 13:03:29 2012 +0200
+++ b/doc-src/System/Thy/document/Sessions.tex Thu Aug 23 13:26:27 2012 +0200
@@ -302,6 +302,7 @@
-d DIR include session directory
-g NAME select session group NAME
-j INT maximum number of parallel jobs (default 1)
+ -l list session source files
-n no build -- test dependencies only
-o OPTION override session configuration OPTION
(via NAME=VAL or NAME)
@@ -373,7 +374,9 @@
\verb|$ISABELLE_HOME/heaps| instead of the default location
\hyperlink{setting.ISABELLE-OUTPUT}{\mbox{\isa{\isatt{ISABELLE{\isaliteral{5F}{\isacharunderscore}}OUTPUT}}}} (which is normally in \hyperlink{setting.ISABELLE-HOME-USER}{\mbox{\isa{\isatt{ISABELLE{\isaliteral{5F}{\isacharunderscore}}HOME{\isaliteral{5F}{\isacharunderscore}}USER}}}}, i.e.\ the user's home directory).
- \medskip Option \verb|-v| enables verbose mode.%
+ \medskip Option \verb|-v| increases the general level of
+ verbosity. Option \verb|-l| lists the source files that
+ contribute to a session.%
\end{isamarkuptext}%
\isamarkuptrue%
%
--- a/lib/Tools/build Thu Aug 23 13:03:29 2012 +0200
+++ b/lib/Tools/build Thu Aug 23 13:26:27 2012 +0200
@@ -33,6 +33,7 @@
echo " -d DIR include session directory"
echo " -g NAME select session group NAME"
echo " -j INT maximum number of parallel jobs (default 1)"
+ echo " -l list session source files"
echo " -n no build -- test dependencies only"
echo " -o OPTION override session configuration OPTION (via NAME=VAL or NAME)"
echo " -s system build mode: produce output in ISABELLE_HOME"
@@ -65,12 +66,13 @@
declare -a INCLUDE_DIRS=()
declare -a SESSION_GROUPS=()
MAX_JOBS=1
+LIST_FILES=false
NO_BUILD=false
eval "declare -a BUILD_OPTIONS=($ISABELLE_BUILD_OPTIONS)"
SYSTEM_MODE=false
VERBOSE=false
-while getopts "D:abcd:g:j:no:sv" OPT
+while getopts "D:abcd:g:j:lno:sv" OPT
do
case "$OPT" in
D)
@@ -95,6 +97,9 @@
check_number "$OPTARG"
MAX_JOBS="$OPTARG"
;;
+ l)
+ LIST_FILES="true"
+ ;;
n)
NO_BUILD="true"
;;
@@ -131,7 +136,7 @@
"$ISABELLE_TOOL" java isabelle.Build \
"$ALL_SESSIONS" "$BUILD_HEAP" "$CLEAN_BUILD" "$MAX_JOBS" \
- "$NO_BUILD" "$SYSTEM_MODE" "$VERBOSE" \
+ "$LIST_FILES" "$NO_BUILD" "$SYSTEM_MODE" "$VERBOSE" \
"${SELECT_DIRS[@]}" $'\n' "${INCLUDE_DIRS[@]}" $'\n' \
"${SESSION_GROUPS[@]}" $'\n' "${BUILD_OPTIONS[@]}" $'\n' "$@"
RC="$?"
--- a/src/Pure/System/build.scala Thu Aug 23 13:03:29 2012 +0200
+++ b/src/Pure/System/build.scala Thu Aug 23 13:26:27 2012 +0200
@@ -328,7 +328,7 @@
def sources(name: String): List[SHA1.Digest] = deps(name).sources.map(_._2)
}
- def dependencies(verbose: Boolean, tree: Session_Tree): Deps =
+ def dependencies(verbose: Boolean, list_files: Boolean, tree: Session_Tree): Deps =
Deps((Map.empty[String, Session_Content] /: tree.topological_order)(
{ case (deps, (name, info)) =>
val (preloaded, parent_syntax, parent_errors) =
@@ -341,7 +341,7 @@
}
val thy_info = new Thy_Info(new Thy_Load(preloaded, parent_syntax))
- if (verbose) {
+ if (verbose || list_files) {
val groups =
if (info.groups.isEmpty) ""
else info.groups.mkString(" (", " ", ")")
@@ -362,6 +362,10 @@
val uses = h.uses.map(p => (Path.explode(n.dir) + Path.explode(p._1)).expand)
thy :: uses
}).flatten ::: info.files.map(file => info.dir + file)
+
+ if (list_files)
+ echo(cat_lines(all_files.map(_.implode).sorted.map(" " + _)))
+
val sources =
try { all_files.map(p => (p, SHA1.digest(p))) }
catch {
@@ -378,7 +382,7 @@
{
val (_, tree) =
find_sessions(Options.init(), dirs.map((false, _))).required(false, Nil, List(session))
- dependencies(false, tree)(session)
+ dependencies(false, false, tree)(session)
}
def outer_syntax(session: String): Outer_Syntax =
@@ -531,6 +535,7 @@
more_dirs: List[(Boolean, Path)] = Nil,
session_groups: List[String] = Nil,
max_jobs: Int = 1,
+ list_files: Boolean = false,
no_build: Boolean = false,
build_options: List[String] = Nil,
system_mode: Boolean = false,
@@ -540,7 +545,7 @@
val options = (Options.init() /: build_options)(_ + _)
val (descendants, tree) =
find_sessions(options, more_dirs).required(all_sessions, session_groups, sessions)
- val deps = dependencies(verbose, tree)
+ val deps = dependencies(verbose, list_files, tree)
val queue = Queue(tree)
def make_stamp(name: String): String =
@@ -692,6 +697,7 @@
Properties.Value.Boolean(build_heap) ::
Properties.Value.Boolean(clean_build) ::
Properties.Value.Int(max_jobs) ::
+ Properties.Value.Boolean(list_files) ::
Properties.Value.Boolean(no_build) ::
Properties.Value.Boolean(system_mode) ::
Properties.Value.Boolean(verbose) ::
@@ -700,7 +706,7 @@
select_dirs.map(d => (true, Path.explode(d))) :::
include_dirs.map(d => (false, Path.explode(d)))
build(all_sessions, build_heap, clean_build, dirs, session_groups,
- max_jobs, no_build, build_options, system_mode, verbose, sessions)
+ max_jobs, list_files, no_build, build_options, system_mode, verbose, sessions)
case _ => error("Bad arguments:\n" + cat_lines(args))
}
}