equal
deleted
inserted
replaced
460 override def toString: String = rc.toString |
460 override def toString: String = rc.toString |
461 } |
461 } |
462 |
462 |
463 def build( |
463 def build( |
464 options: Options, |
464 options: Options, |
465 selection: Sessions.Selection, |
465 selection: Sessions.Selection = Sessions.Selection.empty, |
466 progress: Progress = new Progress, |
466 progress: Progress = new Progress, |
467 check_unknown_files: Boolean = false, |
467 check_unknown_files: Boolean = false, |
468 build_heap: Boolean = false, |
468 build_heap: Boolean = false, |
469 clean_build: Boolean = false, |
469 clean_build: Boolean = false, |
470 dirs: List[Path] = Nil, |
470 dirs: List[Path] = Nil, |
883 } |
883 } |
884 |
884 |
885 val results = |
885 val results = |
886 progress.interrupt_handler { |
886 progress.interrupt_handler { |
887 build(options, |
887 build(options, |
888 Sessions.Selection( |
888 selection = Sessions.Selection( |
889 requirements = requirements, |
889 requirements = requirements, |
890 all_sessions = all_sessions, |
890 all_sessions = all_sessions, |
891 base_sessions = base_sessions, |
891 base_sessions = base_sessions, |
892 exclude_session_groups = exclude_session_groups, |
892 exclude_session_groups = exclude_session_groups, |
893 exclude_sessions = exclude_sessions, |
893 exclude_sessions = exclude_sessions, |
934 fresh: Boolean = false, |
934 fresh: Boolean = false, |
935 strict: Boolean = false): Int = |
935 strict: Boolean = false): Int = |
936 { |
936 { |
937 val selection = Sessions.Selection.session(logic) |
937 val selection = Sessions.Selection.session(logic) |
938 val rc = |
938 val rc = |
939 if (!fresh && |
939 if (!fresh && build(options, selection = selection, |
940 build(options, selection, build_heap = build_heap, no_build = true, dirs = dirs).ok) 0 |
940 build_heap = build_heap, no_build = true, dirs = dirs).ok) 0 |
941 else { |
941 else { |
942 progress.echo("Build started for Isabelle/" + logic + " ...") |
942 progress.echo("Build started for Isabelle/" + logic + " ...") |
943 Build.build(options, selection, progress = progress, build_heap = build_heap, |
943 Build.build(options, selection = selection, progress = progress, |
944 fresh_build = fresh, dirs = dirs).rc |
944 build_heap = build_heap, fresh_build = fresh, dirs = dirs).rc |
945 } |
945 } |
946 if (strict && rc != 0) error("Failed to build Isabelle/" + logic) else rc |
946 if (strict && rc != 0) error("Failed to build Isabelle/" + logic) else rc |
947 } |
947 } |
948 } |
948 } |