697 for { |
697 for { |
698 bundle_info <- bundle_infos |
698 bundle_info <- bundle_infos |
699 if (release.dist_dir + bundle_info.path).is_file |
699 if (release.dist_dir + bundle_info.path).is_file |
700 } yield (bundle_info.name, bundle_info) |
700 } yield (bundle_info.name, bundle_info) |
701 |
701 |
|
702 val isabelle_link = |
|
703 HTML.link(Isabelle_Cronjob.isabelle_repos_source + "/rev/" + release.ident, |
|
704 HTML.text("Isabelle/" + release.ident)) |
702 val afp_link = |
705 val afp_link = |
703 HTML.link(AFP.repos_source + "/rev/" + afp_rev, HTML.text("AFP/" + afp_rev)) |
706 HTML.link(AFP.repos_source + "/rev/" + afp_rev, HTML.text("AFP/" + afp_rev)) |
704 |
707 |
705 HTML.write_document(dir, "index.html", |
708 HTML.write_document(dir, "index.html", |
706 List(HTML.title(release.dist_name)), |
709 List(HTML.title(release.dist_name)), |
707 List( |
710 List( |
708 HTML.chapter(release.dist_name + " (" + release.ident + ")"), |
711 HTML.section(release.dist_name + " (" + release.ident + ")"), |
|
712 HTML.subsection("Platforms"), |
709 HTML.itemize( |
713 HTML.itemize( |
710 website_platform_bundles.map({ case (bundle, bundle_info) => |
714 website_platform_bundles.map({ case (bundle, bundle_info) => |
711 List(HTML.link(bundle, HTML.text(bundle_info.platform_description))) }))) ::: |
715 List(HTML.link(bundle, HTML.text(bundle_info.platform_description))) })), |
712 (if (afp_rev == "") Nil else List(HTML.par(HTML.text("See also ") ::: List(afp_link))))) |
716 HTML.subsection("Repositories"), |
|
717 HTML.itemize( |
|
718 List(List(isabelle_link)) ::: (if (afp_rev == "") Nil else List(List(afp_link)))))) |
713 |
719 |
714 for ((bundle, _) <- website_platform_bundles) |
720 for ((bundle, _) <- website_platform_bundles) |
715 File.copy(release.dist_dir + Path.explode(bundle), dir) |
721 File.copy(release.dist_dir + Path.explode(bundle), dir) |
716 } |
722 } |
717 |
723 |