# HG changeset patch # User wenzelm # Date 1345721187 -7200 # Node ID 1621b3f26095fcce523f3bb28e6938a45469b8ba # Parent 44a6967240b77866d20197cddc4aae81a86d7298 added build option -l (list files); diff -r 44a6967240b7 -r 1621b3f26095 doc-src/System/Thy/Sessions.thy --- 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 *} diff -r 44a6967240b7 -r 1621b3f26095 doc-src/System/Thy/document/Sessions.tex --- 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% % diff -r 44a6967240b7 -r 1621b3f26095 lib/Tools/build --- 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="$?" diff -r 44a6967240b7 -r 1621b3f26095 src/Pure/System/build.scala --- 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)) } }