# HG changeset patch # User wenzelm # Date 1399450411 -7200 # Node ID 7f120d227ca578acbb594ecc2321e5099733efed # Parent 3e8cbb624cc543b5eba69a72c97c60491b881e32 tuned signature; diff -r 3e8cbb624cc5 -r 7f120d227ca5 lib/Tools/build --- a/lib/Tools/build Tue May 06 23:35:24 2014 +0200 +++ b/lib/Tools/build Wed May 07 10:13:31 2014 +0200 @@ -144,7 +144,7 @@ "$ISABELLE_TOOL" java "${JAVA_ARGS[@]}" isabelle.Build \ "$REQUIREMENTS" "$ALL_SESSIONS" "$BUILD_HEAP" "$CLEAN_BUILD" "$MAX_JOBS" \ "$LIST_FILES" "$NO_BUILD" "$SYSTEM_MODE" "$VERBOSE" \ - "${SELECT_DIRS[@]}" $'\n' "${INCLUDE_DIRS[@]}" $'\n' \ + "${INCLUDE_DIRS[@]}" $'\n' "${SELECT_DIRS[@]}" $'\n' \ "${SESSION_GROUPS[@]}" $'\n' "${BUILD_OPTIONS[@]}" $'\n' "$@" RC="$?" diff -r 3e8cbb624cc5 -r 7f120d227ca5 src/Pure/Tools/build.scala --- a/src/Pure/Tools/build.scala Tue May 06 23:35:24 2014 +0200 +++ b/src/Pure/Tools/build.scala Wed May 07 10:13:31 2014 +0200 @@ -288,7 +288,8 @@ if (is_session_dir(dir)) dir else error("Bad session root directory: " + dir.toString) - def find_sessions(options: Options, more_dirs: List[(Boolean, Path)]): Session_Tree = + def find_sessions(options: Options, dirs: List[Path] = Nil, select_dirs: List[Path] = Nil) + : Session_Tree = { def find_dir(select: Boolean, dir: Path): List[(String, Session_Info)] = find_root(select, dir) ::: find_roots(select, dir) @@ -320,13 +321,13 @@ else Nil } - val default_dirs = Isabelle_System.components().filter(is_session_dir(_)).map((false, _)) - - more_dirs foreach { case (_, dir) => check_session_dir(dir) } + val default_dirs = Isabelle_System.components().filter(is_session_dir(_)) + dirs.foreach(check_session_dir(_)) + select_dirs.foreach(check_session_dir(_)) Session_Tree( for { - (select, dir) <- default_dirs ::: more_dirs + (select, dir) <- (default_dirs ::: dirs).map((false, _)) ::: select_dirs.map((true, _)) info <- find_dir(select, dir) } yield info) } @@ -511,8 +512,7 @@ dirs: List[Path], sessions: List[String]): Deps = { - val (_, tree) = - find_sessions(options, dirs.map((false, _))).selection(false, false, Nil, sessions) + val (_, tree) = find_sessions(options, dirs = dirs).selection(false, false, Nil, sessions) dependencies(Ignore_Progress, inlined_files, false, false, tree) } @@ -722,7 +722,8 @@ all_sessions: Boolean = false, build_heap: Boolean = false, clean_build: Boolean = false, - more_dirs: List[(Boolean, Path)] = Nil, + dirs: List[Path] = Nil, + select_dirs: List[Path] = Nil, session_groups: List[String] = Nil, max_jobs: Int = 1, list_files: Boolean = false, @@ -733,7 +734,7 @@ { /* session tree and dependencies */ - val full_tree = find_sessions(options, more_dirs) + val full_tree = find_sessions(options, dirs, select_dirs) val (selected, selected_tree) = full_tree.selection(requirements, all_sessions, session_groups, sessions) @@ -972,7 +973,8 @@ all_sessions: Boolean = false, build_heap: Boolean = false, clean_build: Boolean = false, - more_dirs: List[(Boolean, Path)] = Nil, + dirs: List[Path] = Nil, + select_dirs: List[Path] = Nil, session_groups: List[String] = Nil, max_jobs: Int = 1, list_files: Boolean = false, @@ -983,8 +985,8 @@ { val results = build_results(options, progress, requirements, all_sessions, - build_heap, clean_build, more_dirs, session_groups, max_jobs, list_files, no_build, - system_mode, verbose, sessions) + build_heap, clean_build, dirs, select_dirs, session_groups, max_jobs, + list_files, no_build, system_mode, verbose, sessions) val rc = (0 /: results)({ case (rc1, (_, rc2)) => rc1 max rc2 }) if (rc != 0 && (verbose || !no_build)) { @@ -1012,16 +1014,13 @@ Properties.Value.Boolean(no_build) :: Properties.Value.Boolean(system_mode) :: Properties.Value.Boolean(verbose) :: - Command_Line.Chunks(select_dirs, include_dirs, session_groups, build_options, sessions) => + Command_Line.Chunks(dirs, select_dirs, session_groups, build_options, sessions) => val options = (Options.init() /: build_options)(_ + _) - val more_dirs = - select_dirs.map(d => (true, Path.explode(d))) ::: - include_dirs.map(d => (false, Path.explode(d))) val progress = new Console_Progress(verbose) progress.interrupt_handler { - build(options, progress, requirements, all_sessions, - build_heap, clean_build, more_dirs, session_groups, max_jobs, list_files, no_build, - system_mode, verbose, sessions) + build(options, progress, requirements, all_sessions, build_heap, clean_build, + dirs.map(Path.explode(_)), select_dirs.map(Path.explode(_)), session_groups, + max_jobs, list_files, no_build, system_mode, verbose, sessions) } case _ => error("Bad arguments:\n" + cat_lines(args)) } diff -r 3e8cbb624cc5 -r 7f120d227ca5 src/Pure/Tools/build_doc.scala --- a/src/Pure/Tools/build_doc.scala Tue May 06 23:35:24 2014 +0200 +++ b/src/Pure/Tools/build_doc.scala Wed May 07 10:13:31 2014 +0200 @@ -24,7 +24,7 @@ { val selection = for { - (name, info) <- Build.find_sessions(options, Nil).topological_order + (name, info) <- Build.find_sessions(options).topological_order if info.groups.contains("doc") doc = info.options.string("document_variants") if all_docs || docs.contains(doc) diff -r 3e8cbb624cc5 -r 7f120d227ca5 src/Pure/Tools/keywords.scala --- a/src/Pure/Tools/keywords.scala Tue May 06 23:35:24 2014 +0200 +++ b/src/Pure/Tools/keywords.scala Wed May 07 10:13:31 2014 +0200 @@ -150,7 +150,7 @@ def update_keywords(options: Options) { - val tree = Build.find_sessions(options, Nil) + val tree = Build.find_sessions(options) def chapter(ch: String): List[String] = for ((name, info) <- tree.topological_order if info.chapter == ch) yield name diff -r 3e8cbb624cc5 -r 7f120d227ca5 src/Pure/Tools/main.scala --- a/src/Pure/Tools/main.scala Tue May 06 23:35:24 2014 +0200 +++ b/src/Pure/Tools/main.scala Wed May 07 10:13:31 2014 +0200 @@ -41,13 +41,13 @@ else { val options = Options.init() val system_mode = mode == "" || mode == "system" - val more_dirs = Path.split(Isabelle_System.getenv("JEDIT_SESSION_DIRS")).map((false, _)) + val dirs = Path.split(Isabelle_System.getenv("JEDIT_SESSION_DIRS")) val session = Isabelle_System.default_logic( Isabelle_System.getenv("JEDIT_LOGIC"), options.string("jedit_logic")) if (Build.build(options = options, build_heap = true, no_build = true, - more_dirs = more_dirs, sessions = List(session)) == 0) + dirs = dirs, sessions = List(session)) == 0) system_dialog.return_code(0) else { system_dialog.title("Isabelle build (" + Isabelle_System.getenv("ML_IDENTIFIER") + ")") @@ -56,9 +56,8 @@ val (out, rc) = try { ("", - Build.build(options = options, progress = system_dialog, - build_heap = true, more_dirs = more_dirs, - system_mode = system_mode, sessions = List(session))) + Build.build(options = options, progress = system_dialog, build_heap = true, + dirs = dirs, system_mode = system_mode, sessions = List(session))) } catch { case exn: Throwable => diff -r 3e8cbb624cc5 -r 7f120d227ca5 src/Tools/jEdit/src/isabelle_logic.scala --- a/src/Tools/jEdit/src/isabelle_logic.scala Tue May 06 23:35:24 2014 +0200 +++ b/src/Tools/jEdit/src/isabelle_logic.scala Wed May 07 10:13:31 2014 +0200 @@ -71,8 +71,7 @@ def session_list(): List[String] = { - val dirs = session_dirs().map((false, _)) - val session_tree = Build.find_sessions(PIDE.options.value, dirs) + val session_tree = Build.find_sessions(PIDE.options.value, dirs = session_dirs()) val (main_sessions, other_sessions) = session_tree.topological_order.partition(p => p._2.groups.contains("main")) main_sessions.map(_._1).sorted ::: other_sessions.map(_._1).sorted