185 val jdk_component = |
185 val jdk_component = |
186 components.find(_.startsWith("jdk")) getOrElse error("Missing jdk component") |
186 components.find(_.startsWith("jdk")) getOrElse error("Missing jdk component") |
187 (components, jdk_component) |
187 (components, jdk_component) |
188 } |
188 } |
189 |
189 |
190 def activate_bundled_components(dir: Path, platform: Platform.Family.Value) |
190 def activate_components(dir: Path, platform: Platform.Family.Value, more_names: List[String]) |
191 { |
191 { |
|
192 def contrib_name(name: String): String = |
|
193 Components.contrib(name = name).implode |
|
194 |
192 val Bundled = new Bundled(platform = Some(platform)) |
195 val Bundled = new Bundled(platform = Some(platform)) |
193 Components.write_components(dir, |
196 Components.write_components(dir, |
194 Components.read_components(dir).flatMap(line => |
197 Components.read_components(dir).flatMap(line => |
195 line match { |
198 line match { |
196 case Bundled(name) => |
199 case Bundled(name) => |
197 if (Components.check_dir(Components.contrib(dir, name))) |
200 if (Components.check_dir(Components.contrib(dir, name))) Some(contrib_name(name)) |
198 Some(Components.contrib(name = name).implode) |
|
199 else None |
201 else None |
200 case _ => if (Bundled.detect(line)) None else Some(line) |
202 case _ => if (Bundled.detect(line)) None else Some(line) |
201 })) |
203 }) ::: more_names.map(contrib_name(_))) |
202 } |
204 } |
203 |
205 |
204 def make_contrib(dir: Path) |
206 def make_contrib(dir: Path) |
205 { |
207 { |
206 Isabelle_System.mkdirs(Components.contrib(dir)) |
208 Isabelle_System.mkdirs(Components.contrib(dir)) |
234 rev: String = "", |
236 rev: String = "", |
235 afp_rev: String = "", |
237 afp_rev: String = "", |
236 official_release: Boolean = false, |
238 official_release: Boolean = false, |
237 proper_release_name: Option[String] = None, |
239 proper_release_name: Option[String] = None, |
238 platform_families: List[Platform.Family.Value] = default_platform_families, |
240 platform_families: List[Platform.Family.Value] = default_platform_families, |
|
241 more_components: List[Path] = Nil, |
239 website: Option[Path] = None, |
242 website: Option[Path] = None, |
240 build_library: Boolean = false, |
243 build_library: Boolean = false, |
241 parallel_jobs: Int = 1, |
244 parallel_jobs: Int = 1, |
242 remote_mac: String = ""): Release = |
245 remote_mac: String = ""): Release = |
243 { |
246 { |
393 |
396 |
394 for (bundle_info <- bundle_infos) { |
397 for (bundle_info <- bundle_infos) { |
395 val bundle = |
398 val bundle = |
396 (if (remote_mac.isEmpty) bundle_info.fallback else None) getOrElse bundle_info.main |
399 (if (remote_mac.isEmpty) bundle_info.fallback else None) getOrElse bundle_info.main |
397 val bundle_archive = release.dist_dir + Path.explode(bundle) |
400 val bundle_archive = release.dist_dir + Path.explode(bundle) |
398 if (bundle_archive.is_file) |
401 if (bundle_archive.is_file && more_components.isEmpty) |
399 progress.echo_warning("Application bundle already exists: " + bundle_archive) |
402 progress.echo_warning("Application bundle already exists: " + bundle_archive) |
400 else { |
403 else { |
401 val isabelle_name = release.dist_name |
404 val isabelle_name = release.dist_name |
402 val platform = bundle_info.platform |
405 val platform = bundle_info.platform |
403 |
406 |
416 |
419 |
417 progress.echo("Bundled components:") |
420 progress.echo("Bundled components:") |
418 |
421 |
419 val contrib_dir = Components.contrib(isabelle_target) |
422 val contrib_dir = Components.contrib(isabelle_target) |
420 |
423 |
421 val (components, jdk_component) = get_bundled_components(isabelle_target, platform) |
424 val (bundled_components, jdk_component) = |
|
425 get_bundled_components(isabelle_target, platform) |
422 |
426 |
423 Components.resolve(other_isabelle.components_base(components_base), |
427 Components.resolve(other_isabelle.components_base(components_base), |
424 components, target_dir = Some(contrib_dir), progress = progress) |
428 bundled_components, target_dir = Some(contrib_dir), progress = progress) |
|
429 |
|
430 val more_components_names = |
|
431 more_components.map(Components.unpack(contrib_dir, _, progress = progress)) |
425 |
432 |
426 Components.purge(contrib_dir, platform) |
433 Components.purge(contrib_dir, platform) |
427 |
434 |
428 activate_bundled_components(isabelle_target, platform) |
435 activate_components(isabelle_target, platform, more_components_names) |
429 |
436 |
430 |
437 |
431 // Java parameters |
438 // Java parameters |
432 |
439 |
433 val java_options_title = "# Java runtime options" |
440 val java_options_title = "# Java runtime options" |
734 var components_base: Option[Path] = None |
741 var components_base: Option[Path] = None |
735 var remote_mac = "" |
742 var remote_mac = "" |
736 var official_release = false |
743 var official_release = false |
737 var proper_release_name: Option[String] = None |
744 var proper_release_name: Option[String] = None |
738 var website: Option[Path] = None |
745 var website: Option[Path] = None |
|
746 var more_components: List[Path] = Nil |
739 var parallel_jobs = 1 |
747 var parallel_jobs = 1 |
740 var build_library = false |
748 var build_library = false |
741 var options = Options.init() |
749 var options = Options.init() |
742 var platform_families = default_platform_families |
750 var platform_families = default_platform_families |
743 var rev = "" |
751 var rev = "" |
750 -C DIR base directory for Isabelle components (default: $ISABELLE_HOME_USER/../contrib) |
758 -C DIR base directory for Isabelle components (default: $ISABELLE_HOME_USER/../contrib) |
751 -M USER@HOST remote Mac OS X for dmg build |
759 -M USER@HOST remote Mac OS X for dmg build |
752 -O official release (not release-candidate) |
760 -O official release (not release-candidate) |
753 -R RELEASE proper release with name |
761 -R RELEASE proper release with name |
754 -W WEBSITE produce minimal website in given directory |
762 -W WEBSITE produce minimal website in given directory |
|
763 -c ARCHIVE clean bundling with additional component .tar.gz archive |
755 -j INT maximum number of parallel jobs (default 1) |
764 -j INT maximum number of parallel jobs (default 1) |
756 -l build library |
765 -l build library |
757 -o OPTION override Isabelle system OPTION (via NAME=VAL or NAME) |
766 -o OPTION override Isabelle system OPTION (via NAME=VAL or NAME) |
758 -p NAMES platform families (default: """ + default_platform_families.mkString(",") + """) |
767 -p NAMES platform families (default: """ + default_platform_families.mkString(",") + """) |
759 -r REV Mercurial changeset id (default: RELEASE or tip) |
768 -r REV Mercurial changeset id (default: RELEASE or tip) |
764 "C:" -> (arg => components_base = Some(Path.explode(arg))), |
773 "C:" -> (arg => components_base = Some(Path.explode(arg))), |
765 "M:" -> (arg => remote_mac = arg), |
774 "M:" -> (arg => remote_mac = arg), |
766 "O" -> (_ => official_release = true), |
775 "O" -> (_ => official_release = true), |
767 "R:" -> (arg => proper_release_name = Some(arg)), |
776 "R:" -> (arg => proper_release_name = Some(arg)), |
768 "W:" -> (arg => website = Some(Path.explode(arg))), |
777 "W:" -> (arg => website = Some(Path.explode(arg))), |
|
778 "c:" -> (arg => |
|
779 { |
|
780 val path = Path.explode(arg) |
|
781 Components.Archive.get_name(path.file_name) |
|
782 more_components = more_components ::: List(path) |
|
783 }), |
769 "j:" -> (arg => parallel_jobs = Value.Int.parse(arg)), |
784 "j:" -> (arg => parallel_jobs = Value.Int.parse(arg)), |
770 "l" -> (_ => build_library = true), |
785 "l" -> (_ => build_library = true), |
771 "o:" -> (arg => options = options + arg), |
786 "o:" -> (arg => options = options + arg), |
772 "p:" -> (arg => platform_families = space_explode(',', arg).map(Platform.Family.parse)), |
787 "p:" -> (arg => platform_families = space_explode(',', arg).map(Platform.Family.parse)), |
773 "r:" -> (arg => rev = arg)) |
788 "r:" -> (arg => rev = arg)) |
781 progress = progress, rev = rev, afp_rev = afp_rev, official_release = official_release, |
796 progress = progress, rev = rev, afp_rev = afp_rev, official_release = official_release, |
782 proper_release_name = proper_release_name, website = website, |
797 proper_release_name = proper_release_name, website = website, |
783 platform_families = |
798 platform_families = |
784 if (platform_families.isEmpty) default_platform_families |
799 if (platform_families.isEmpty) default_platform_families |
785 else platform_families, |
800 else platform_families, |
786 build_library = build_library, parallel_jobs = parallel_jobs, remote_mac = remote_mac) |
801 more_components = more_components, build_library = build_library, |
|
802 parallel_jobs = parallel_jobs, remote_mac = remote_mac) |
787 } |
803 } |
788 } |
804 } |
789 } |
805 } |