diff --git a/lib/html/library_index_content.template b/lib/html/library_index_content.template deleted file mode 100644 --- a/lib/html/library_index_content.template +++ /dev/null @@ -1,54 +0,0 @@ - - - - - diff --git a/lib/html/library_index_footer.template b/lib/html/library_index_footer.template deleted file mode 100644 --- a/lib/html/library_index_footer.template +++ /dev/null @@ -1,2 +0,0 @@ - - diff --git a/lib/html/library_index_header.template b/lib/html/library_index_header.template deleted file mode 100644 --- a/lib/html/library_index_header.template +++ /dev/null @@ -1,27 +0,0 @@ - - - - - - - The {ISABELLE} Library - - - -
- - - - - - -
[Isabelle] - - - - -
The {ISABELLE} Library
-
-
-
diff --git a/src/Pure/Admin/build_release.scala b/src/Pure/Admin/build_release.scala --- a/src/Pure/Admin/build_release.scala +++ b/src/Pure/Admin/build_release.scala @@ -1,907 +1,904 @@ /* Title: Pure/Admin/build_release.scala Author: Makarius Build full Isabelle distribution from repository. */ package isabelle object Build_Release { /** release info **/ sealed case class Bundle_Info( platform: Platform.Family.Value, platform_description: String, name: String) { def path: Path = Path.explode(name) } class Release private[Build_Release]( progress: Progress, val date: Date, val dist_name: String, val dist_dir: Path, val dist_version: String, val ident: String, val tags: String) { val isabelle: Path = Path.explode(dist_name) val isabelle_dir: Path = dist_dir + isabelle val isabelle_id: Path = isabelle_dir + Path.explode("etc/ISABELLE_ID") val isabelle_tags: Path = isabelle_dir + Path.explode("etc/ISABELLE_TAGS") val isabelle_identifier: Path = isabelle_dir + Path.explode("etc/ISABELLE_IDENTIFIER") val isabelle_archive: Path = dist_dir + Path.explode(dist_name + ".tar.gz") val isabelle_library_archive: Path = dist_dir + Path.explode(dist_name + "_library.tar.gz") def other_isabelle(dir: Path): Other_Isabelle = Other_Isabelle(dir + isabelle, isabelle_identifier = dist_name + "-build", progress = progress) def bundle_info(platform: Platform.Family.Value): Bundle_Info = platform match { case Platform.Family.linux => Bundle_Info(platform, "Linux", dist_name + "_linux.tar.gz") case Platform.Family.macos => Bundle_Info(platform, "macOS", dist_name + "_macos.tar.gz") case Platform.Family.windows => Bundle_Info(platform, "Windows", dist_name + ".exe") } } /** generated content **/ /* patch release */ def patch_release(release: Release): Unit = { val dir = release.isabelle_dir - File.change(dir + Path.explode("lib/html/library_index_header.template"), - _.replace("{ISABELLE}", release.dist_name)) - File.change(dir + Path.explode("README"), _.replace("some repository version of Isabelle", release.dist_version)) } /* ANNOUNCE */ def make_announce(release: Release): Unit = { File.write(release.isabelle_dir + Path.explode("ANNOUNCE"), """ IMPORTANT NOTE ============== This is a snapshot of Isabelle/""" + release.ident + """ from the repository. """) } /* NEWS */ def make_news(other_isabelle: Other_Isabelle, dist_version: String): Unit = { val target = other_isabelle.isabelle_home + Path.explode("doc") val target_fonts = Isabelle_System.make_directory(target + Path.explode("fonts")) other_isabelle.copy_fonts(target_fonts) HTML.write_document(target, "NEWS.html", List(HTML.title("NEWS (" + dist_version + ")")), List( HTML.chapter("NEWS"), HTML.source( Symbol.decode(File.read(other_isabelle.isabelle_home + Path.explode("NEWS")))))) } /* bundled components */ class Bundled(platform: Option[Platform.Family.Value] = None) { def detect(s: String): Boolean = s.startsWith("#bundled") && !s.startsWith("#bundled ") def apply(name: String): String = "#bundled" + (platform match { case None => "" case Some(plat) => "-" + plat }) + ":" + name private val Pattern1 = ("""^#bundled:(.*)$""").r private val Pattern2 = ("""^#bundled-(.*):(.*)$""").r def unapply(s: String): Option[String] = s match { case Pattern1(name) => Some(name) case Pattern2(Platform.Family(plat), name) if platform == Some(plat) => Some(name) case _ => None } } def record_bundled_components(dir: Path): Unit = { val catalogs = List("main", "bundled").map((_, new Bundled())) ::: default_platform_families.flatMap(platform => List(platform.toString, "bundled-" + platform.toString). map((_, new Bundled(platform = Some(platform))))) File.append(Components.components(dir), terminate_lines("#bundled components" :: (for { (catalog, bundled) <- catalogs.iterator path = Components.admin(dir) + Path.basic(catalog) if path.is_file line <- split_lines(File.read(path)) if line.nonEmpty && !line.startsWith("#") && !line.startsWith("jedit_build") } yield bundled(line)).toList)) } def get_bundled_components(dir: Path, platform: Platform.Family.Value): (List[String], String) = { val Bundled = new Bundled(platform = Some(platform)) val components = for { Bundled(name) <- Components.read_components(dir) if !name.startsWith("jedit_build") } yield name val jdk_component = components.find(_.startsWith("jdk")) getOrElse error("Missing jdk component") (components, jdk_component) } def activate_components( dir: Path, platform: Platform.Family.Value, more_names: List[String]): Unit = { def contrib_name(name: String): String = Components.contrib(name = name).implode val Bundled = new Bundled(platform = Some(platform)) Components.write_components(dir, Components.read_components(dir).flatMap(line => line match { case Bundled(name) => if (Components.check_dir(Components.contrib(dir, name))) Some(contrib_name(name)) else None case _ => if (Bundled.detect(line)) None else Some(line) }) ::: more_names.map(contrib_name)) } def make_contrib(dir: Path): Unit = { Isabelle_System.make_directory(Components.contrib(dir)) File.write(Components.contrib(dir, "README"), """This directory contains add-on components that contribute to the main Isabelle distribution. Separate licensing conditions apply, see each directory individually. """) } /** build release **/ private def execute(dir: Path, script: String): Unit = Isabelle_System.bash(script, cwd = dir.file).check private def execute_tar(dir: Path, args: String): Unit = Isabelle_System.gnutar(args, dir = dir).check /* build heaps on remote server */ private def remote_build_heaps( options: Options, platform: Platform.Family.Value, build_sessions: List[String], local_dir: Path): Unit = { val server_option = "build_host_" + platform.toString options.string(server_option) match { case SSH.Target(user, host) => using(SSH.open_session(options, host = host, user = user))(ssh => { Isabelle_System.with_tmp_file("tmp", "tar")(local_tmp_tar => { execute_tar(local_dir, "-cf " + File.bash_path(local_tmp_tar) + " .") ssh.with_tmp_dir(remote_dir => { val remote_tmp_tar = remote_dir + Path.basic("tmp.tar") ssh.write_file(remote_tmp_tar, local_tmp_tar) val remote_commands = List( "cd " + File.bash_path(remote_dir), "tar -xf tmp.tar", "./bin/isabelle build -o system_heaps -b -- " + Bash.strings(build_sessions), "tar -cf tmp.tar heaps") ssh.execute(remote_commands.mkString(" && ")).check ssh.read_file(remote_tmp_tar, local_tmp_tar) }) execute_tar(local_dir, "-xf " + File.bash_path(local_tmp_tar)) }) }) case s => error("Bad " + server_option + ": " + quote(s)) } } /* Isabelle application */ def make_isabelle_options(path: Path, options: List[String], line_ending: String = "\n"): Unit = { val title = "# Java runtime options" File.write(path, (title :: options).map(_ + line_ending).mkString) } def make_isabelle_app( platform: Platform.Family.Value, isabelle_target: Path, isabelle_name: String, jdk_component: String, classpath: List[Path], dock_icon: Boolean = false): Unit = { val script = """#!/usr/bin/env bash # # Author: Makarius # # Main Isabelle application script. # minimal Isabelle environment ISABELLE_HOME="$(cd "$(dirname "$0")"; cd "$(pwd -P)/../.."; pwd)" source "$ISABELLE_HOME/lib/scripts/isabelle-platform" #paranoia settings -- avoid intrusion of alien options unset "_JAVA_OPTIONS" unset "JAVA_TOOL_OPTIONS" #paranoia settings -- avoid problems of Java/Swing versus XIM/IBus etc. unset XMODIFIERS COMPONENT="$ISABELLE_HOME/contrib/""" + jdk_component + """" source "$COMPONENT/etc/settings" # main declare -a JAVA_OPTIONS=($(perl -p -e 's,#.*$,,g;' "$ISABELLE_HOME/Isabelle.options")) "$ISABELLE_HOME/bin/isabelle" env "$ISABELLE_HOME/lib/scripts/java-gui-setup" exec "$ISABELLE_JDK_HOME/bin/java" \ "-Disabelle.root=$ISABELLE_HOME" "${JAVA_OPTIONS[@]}" \ -classpath """" + classpath.map(p => "$ISABELLE_HOME/" + p.implode).mkString(":") + """" \ "-splash:$ISABELLE_HOME/lib/logo/isabelle.gif" \ """ + (if (dock_icon) """"-Xdock:icon=$ISABELLE_HOME/lib/logo/isabelle_transparent-128.png" \ """ else "") + """isabelle.Main "$@" """ val script_path = isabelle_target + Path.explode("lib/scripts/Isabelle_app") File.write(script_path, script) File.set_executable(script_path, true) val component_dir = isabelle_target + Path.explode("contrib/Isabelle_app") Isabelle_System.move_file( component_dir + Path.explode(Platform.standard_platform(platform)) + Path.explode("Isabelle"), isabelle_target + Path.explode(isabelle_name)) Isabelle_System.rm_tree(component_dir) } def make_isabelle_plist(path: Path, isabelle_name: String, isabelle_rev: String): Unit = { File.write(path, """ CFBundleDevelopmentRegion English CFBundleIconFile isabelle.icns CFBundleIdentifier de.tum.in.isabelle CFBundleDisplayName """ + isabelle_name + """ CFBundleInfoDictionaryVersion 6.0 CFBundleName """ + isabelle_name + """ CFBundlePackageType APPL CFBundleShortVersionString """ + isabelle_name + """ CFBundleSignature ???? CFBundleVersion """ + isabelle_rev + """ NSHumanReadableCopyright LSMinimumSystemVersion 10.11 LSApplicationCategoryType public.app-category.developer-tools NSHighResolutionCapable true NSSupportsAutomaticGraphicsSwitching true CFBundleDocumentTypes CFBundleTypeExtensions thy CFBundleTypeIconFile theory.icns CFBundleTypeName Isabelle theory file CFBundleTypeRole Editor LSTypeIsPackage """) } /* main */ private val default_platform_families: List[Platform.Family.Value] = List(Platform.Family.linux, Platform.Family.windows, Platform.Family.macos) def build_release(base_dir: Path, options: Options, components_base: Path = Components.default_components_base, progress: Progress = new Progress, rev: String = "", afp_rev: String = "", proper_release_name: Option[String] = None, platform_families: List[Platform.Family.Value] = default_platform_families, more_components: List[Path] = Nil, website: Option[Path] = None, build_sessions: List[String] = Nil, build_library: Boolean = false, parallel_jobs: Int = 1): Release = { val hg = Mercurial.repository(Path.ISABELLE_HOME) val release = { val date = Date.now() val dist_name = proper_release_name getOrElse ("Isabelle_" + Date.Format.date(date)) val dist_dir = (base_dir + Path.explode("dist-" + dist_name)).absolute val version = proper_string(rev) orElse proper_release_name getOrElse "tip" val ident = try { hg.id(version) } catch { case ERROR(msg) => cat_error("Bad repository version: " + version, msg) } val tags = hg.tags(rev = ident) val dist_version = proper_release_name match { case Some(name) => name + ": " + Date.Format("LLLL uuuu")(date) case None => "Isabelle repository snapshot " + ident + " " + Date.Format.date(date) } new Release(progress, date, dist_name, dist_dir, dist_version, ident, tags) } /* make distribution */ if (release.isabelle_archive.is_file) { progress.echo_warning("Release archive already exists: " + release.isabelle_archive) val archive_ident = Isabelle_System.with_tmp_dir("build_release")(tmp_dir => { val getsettings = release.isabelle + Path.explode("lib/scripts/getsettings") execute_tar(tmp_dir, "-xzf " + File.bash_path(release.isabelle_archive) + " " + File.bash_path(getsettings)) Isabelle_System.isabelle_id(root = tmp_dir + release.isabelle) }) if (release.ident != archive_ident) { error("Mismatch of release identification " + release.ident + " vs. archive " + archive_ident) } } else { progress.echo_warning("Producing release archive " + release.isabelle_archive + " ...") Isabelle_System.make_directory(release.dist_dir) if (release.isabelle_dir.is_dir) error("Directory " + release.isabelle_dir + " already exists") progress.echo_warning("Retrieving Mercurial repository version " + release.ident) hg.archive(release.isabelle_dir.expand.implode, rev = release.ident, options = "--type files") for (name <- List(".hg_archival.txt", ".hgtags", ".hgignore", "README_REPOSITORY")) { (release.isabelle_dir + Path.explode(name)).file.delete } progress.echo_warning("Preparing distribution " + quote(release.dist_name)) File.write(release.isabelle_id, release.ident) File.write(release.isabelle_tags, release.tags) File.write(release.isabelle_identifier, release.dist_name) patch_release(release) if (proper_release_name.isEmpty) make_announce(release) make_contrib(release.isabelle_dir) execute(release.isabelle_dir, """find . -print | xargs chmod -f u+rw""") record_bundled_components(release.isabelle_dir) /* build tools and documentation */ val other_isabelle = release.other_isabelle(release.dist_dir) other_isabelle.init_settings( other_isabelle.init_components(components_base = components_base, catalogs = List("main"))) other_isabelle.resolve_components(echo = true) try { val export_classpath = "export CLASSPATH=" + Bash.string(other_isabelle.getenv("ISABELLE_CLASSPATH")) + "\n" other_isabelle.bash(export_classpath + "./Admin/build all", echo = true).check other_isabelle.bash(export_classpath + "./bin/isabelle jedit -b", echo = true).check } catch { case ERROR(msg) => cat_error("Failed to build tools:", msg) } try { other_isabelle.bash( "./bin/isabelle build_doc -a -o system_heaps -j " + parallel_jobs, echo = true).check } catch { case ERROR(msg) => cat_error("Failed to build documentation:", msg) } make_news(other_isabelle, release.dist_version) for (name <- List("Admin", "browser_info", "heaps")) { Isabelle_System.rm_tree(other_isabelle.isabelle_home + Path.explode(name)) } other_isabelle.cleanup() progress.echo_warning("Creating distribution archive " + release.isabelle_archive) def execute_dist_name(script: String): Unit = Isabelle_System.bash(script, cwd = release.dist_dir.file, env = Isabelle_System.settings() + ("DIST_NAME" -> release.dist_name)).check execute_dist_name(""" set -e chmod -R a+r "$DIST_NAME" chmod -R u+w "$DIST_NAME" chmod -R g=o "$DIST_NAME" find "$DIST_NAME" -type f "(" -name "*.thy" -o -name "*.ML" -o -name "*.scala" ")" -print | xargs chmod -f u-w """) execute_tar(release.dist_dir, "-czf " + File.bash_path(release.isabelle_archive) + " " + Bash.string(release.dist_name)) execute_dist_name(""" set -e mv "$DIST_NAME" "${DIST_NAME}-old" mkdir "$DIST_NAME" mv "${DIST_NAME}-old/README" "${DIST_NAME}-old/NEWS" "${DIST_NAME}-old/ANNOUNCE" \ "${DIST_NAME}-old/COPYRIGHT" "${DIST_NAME}-old/CONTRIBUTORS" "$DIST_NAME" mkdir "$DIST_NAME/doc" mv "${DIST_NAME}-old/doc/"*.pdf \ "${DIST_NAME}-old/doc/"*.html \ "${DIST_NAME}-old/doc/"*.css \ "${DIST_NAME}-old/doc/fonts" \ "${DIST_NAME}-old/doc/Contents" "$DIST_NAME/doc" rm -f Isabelle && ln -sf "$DIST_NAME" Isabelle rm -rf "${DIST_NAME}-old" """) } /* make application bundles */ val bundle_infos = platform_families.map(release.bundle_info) for (bundle_info <- bundle_infos) { val isabelle_name = release.dist_name val platform = bundle_info.platform progress.echo("\nApplication bundle for " + platform) Isabelle_System.with_tmp_dir("build_release")(tmp_dir => { // release archive execute_tar(tmp_dir, "-xzf " + File.bash_path(release.isabelle_archive)) val other_isabelle = release.other_isabelle(tmp_dir) val isabelle_target = other_isabelle.isabelle_home // bundled components progress.echo("Bundled components:") val contrib_dir = Components.contrib(isabelle_target) val (bundled_components, jdk_component) = get_bundled_components(isabelle_target, platform) Components.resolve(components_base, bundled_components, target_dir = Some(contrib_dir), copy_dir = Some(release.dist_dir + Path.explode("contrib")), progress = progress) val more_components_names = more_components.map(Components.unpack(contrib_dir, _, progress = progress)) Components.purge(contrib_dir, platform) activate_components(isabelle_target, platform, more_components_names) // Java parameters val java_options: List[String] = (for { variable <- List( "ISABELLE_JAVA_SYSTEM_OPTIONS", "JEDIT_JAVA_SYSTEM_OPTIONS", "JEDIT_JAVA_OPTIONS") opt <- Word.explode(other_isabelle.getenv(variable)) } yield { val s = "-Dapple.awt.application.name=" if (opt.startsWith(s)) s + isabelle_name else opt }) ::: List("-Disabelle.jedit_server=" + isabelle_name) val classpath: List[Path] = { val base = isabelle_target.absolute Path.split(other_isabelle.getenv("ISABELLE_CLASSPATH")).map(path => { val abs_path = path.absolute File.relative_path(base, abs_path) match { case Some(rel_path) => rel_path case None => error("Bad ISABELLE_CLASSPATH element: " + abs_path) } }) ::: List(Path.explode("src/Tools/jEdit/dist/jedit.jar")) } val jedit_options = Path.explode("src/Tools/jEdit/etc/options") val jedit_props = Path.explode("src/Tools/jEdit/dist/properties/jEdit.props") // build heaps if (build_sessions.nonEmpty) { progress.echo("Building heaps ...") remote_build_heaps(options, platform, build_sessions, isabelle_target) } // application bundling platform match { case Platform.Family.linux => File.change(isabelle_target + jedit_options, _.replaceAll("jedit_reset_font_size : int =.*", "jedit_reset_font_size : int = 24")) File.change(isabelle_target + jedit_props, _.replaceAll("console.fontsize=.*", "console.fontsize=18") .replaceAll("helpviewer.fontsize=.*", "helpviewer.fontsize=18") .replaceAll("metal.primary.fontsize=.*", "metal.primary.fontsize=18") .replaceAll("metal.secondary.fontsize=.*", "metal.secondary.fontsize=18") .replaceAll("view.fontsize=.*", "view.fontsize=24") .replaceAll("view.gutter.fontsize=.*", "view.gutter.fontsize=16")) make_isabelle_options( isabelle_target + Path.explode("Isabelle.options"), java_options) make_isabelle_app(platform, isabelle_target, isabelle_name, jdk_component, classpath) val archive_name = isabelle_name + "_linux.tar.gz" progress.echo("Packaging " + archive_name + " ...") execute_tar(tmp_dir, "-czf " + File.bash_path(release.dist_dir + Path.explode(archive_name)) + " " + Bash.string(isabelle_name)) case Platform.Family.macos => File.change(isabelle_target + jedit_props, _.replaceAll("delete-line.shortcut=.*", "delete-line.shortcut=C+d") .replaceAll("delete.shortcut2=.*", "delete.shortcut2=A+d")) // macOS application bundle val app_contents = isabelle_target + Path.explode("Contents") for (icon <- List("lib/logo/isabelle.icns", "lib/logo/theory.icns")) { Isabelle_System.copy_file(isabelle_target + Path.explode(icon), Isabelle_System.make_directory(app_contents + Path.explode("Resources"))) } make_isabelle_plist( app_contents + Path.explode("Info.plist"), isabelle_name, release.ident) make_isabelle_app(platform, isabelle_target, isabelle_name, jdk_component, classpath, dock_icon = true) val isabelle_options = Path.explode("Isabelle.options") make_isabelle_options( isabelle_target + isabelle_options, java_options ::: List("-Disabelle.app=true")) // application archive val archive_name = isabelle_name + "_macos.tar.gz" progress.echo("Packaging " + archive_name + " ...") val isabelle_app = Path.explode(isabelle_name + ".app") Isabelle_System.move_file(tmp_dir + Path.explode(isabelle_name), tmp_dir + isabelle_app) execute_tar(tmp_dir, "-czf " + File.bash_path(release.dist_dir + Path.explode(archive_name)) + " " + File.bash_path(isabelle_app)) case Platform.Family.windows => File.change(isabelle_target + jedit_props, _.replaceAll("foldPainter=.*", "foldPainter=Square")) // application launcher Isabelle_System.move_file(isabelle_target + Path.explode("contrib/windows_app"), tmp_dir) val app_template = Path.explode("~~/Admin/Windows/launch4j") make_isabelle_options( isabelle_target + Path.explode(isabelle_name + ".l4j.ini"), java_options, line_ending = "\r\n") val isabelle_xml = Path.explode("isabelle.xml") val isabelle_exe = Path.explode(isabelle_name + ".exe") File.write(tmp_dir + isabelle_xml, File.read(app_template + isabelle_xml) .replace("{ISABELLE_NAME}", isabelle_name) .replace("{OUTFILE}", File.platform_path(isabelle_target + isabelle_exe)) .replace("{ICON}", File.platform_path(app_template + Path.explode("isabelle_transparent.ico"))) .replace("{SPLASH}", File.platform_path(app_template + Path.explode("isabelle.bmp"))) .replace("{CLASSPATH}", cat_lines(classpath.map(cp => " %EXEDIR%\\" + File.platform_path(cp).replace('/', '\\') + ""))) .replace("\\jdk\\", "\\" + jdk_component + "\\")) execute(tmp_dir, "\"windows_app/launch4j-${ISABELLE_PLATFORM_FAMILY}/launch4j\" isabelle.xml") Isabelle_System.copy_file(app_template + Path.explode("manifest.xml"), isabelle_target + isabelle_exe.ext("manifest")) // Cygwin setup val cygwin_template = Path.explode("~~/Admin/Windows/Cygwin") Isabelle_System.copy_file(cygwin_template + Path.explode("Cygwin-Terminal.bat"), isabelle_target) val cygwin_mirror = File.read(isabelle_target + Path.explode("contrib/cygwin/isabelle/cygwin_mirror")) val cygwin_bat = Path.explode("Cygwin-Setup.bat") File.write(isabelle_target + cygwin_bat, File.read(cygwin_template + cygwin_bat).replace("{MIRROR}", cygwin_mirror)) File.set_executable(isabelle_target + cygwin_bat, true) for (name <- List("isabelle/postinstall", "isabelle/rebaseall")) { val path = Path.explode(name) Isabelle_System.copy_file(cygwin_template + path, isabelle_target + Path.explode("contrib/cygwin") + path) } execute(isabelle_target, """find . -type f -not -name "*.exe" -not -name "*.dll" """ + (if (Platform.is_macos) "-perm +100" else "-executable") + " -print0 > contrib/cygwin/isabelle/executables") execute(isabelle_target, """find . -type l -exec echo "{}" ";" -exec readlink "{}" ";" """ + """> contrib/cygwin/isabelle/symlinks""") execute(isabelle_target, """find . -type l -exec rm "{}" ";" """) File.write(isabelle_target + Path.explode("contrib/cygwin/isabelle/uninitialized"), "") // executable archive (self-extracting 7z) val archive_name = isabelle_name + ".7z" val exe_archive = tmp_dir + Path.explode(archive_name) exe_archive.file.delete progress.echo("Packaging " + archive_name + " ...") execute(tmp_dir, "7z -y -bd a " + File.bash_path(exe_archive) + " " + Bash.string(isabelle_name)) if (!exe_archive.is_file) error("Failed to create archive: " + exe_archive) val sfx_exe = tmp_dir + Path.explode("windows_app/7zsd_All_x64.sfx") val sfx_txt = File.read(Path.explode("~~/Admin/Windows/Installer/sfx.txt")) .replace("{ISABELLE_NAME}", isabelle_name) Bytes.write(release.dist_dir + isabelle_exe, Bytes.read(sfx_exe) + Bytes(sfx_txt) + Bytes.read(exe_archive)) File.set_executable(release.dist_dir + isabelle_exe, true) } }) progress.echo("DONE") } /* minimal website */ for (dir <- website) { val website_platform_bundles = for { bundle_info <- bundle_infos if (release.dist_dir + bundle_info.path).is_file } yield (bundle_info.name, bundle_info) val isabelle_link = HTML.link(Isabelle_Cronjob.isabelle_repos_source + "/rev/" + release.ident, HTML.text("Isabelle/" + release.ident)) val afp_link = HTML.link(AFP.repos_source + "/rev/" + afp_rev, HTML.text("AFP/" + afp_rev)) HTML.write_document(dir, "index.html", List(HTML.title(release.dist_name)), List( HTML.section(release.dist_name), HTML.subsection("Platforms"), HTML.itemize( website_platform_bundles.map({ case (bundle, bundle_info) => List(HTML.link(bundle, HTML.text(bundle_info.platform_description))) })), HTML.subsection("Repositories"), HTML.itemize( List(List(isabelle_link)) ::: (if (afp_rev == "") Nil else List(List(afp_link)))))) for ((bundle, _) <- website_platform_bundles) Isabelle_System.copy_file(release.dist_dir + Path.explode(bundle), dir) } /* HTML library */ if (build_library) { if (release.isabelle_library_archive.is_file) { progress.echo_warning("Library archive already exists: " + release.isabelle_library_archive) } else { Isabelle_System.with_tmp_dir("build_release")(tmp_dir => { val bundle = release.dist_dir + Path.explode(release.dist_name + "_" + Platform.family + ".tar.gz") execute_tar(tmp_dir, "-xzf " + File.bash_path(bundle)) val other_isabelle = release.other_isabelle(tmp_dir) Isabelle_System.make_directory(other_isabelle.etc) File.write(other_isabelle.etc_preferences, "ML_system_64 = true\n") other_isabelle.bash("bin/isabelle build -f -j " + parallel_jobs + " -o browser_info -o document=pdf -o document_variants=document:outline=/proof,/ML" + " -o system_heaps -c -a -d '~~/src/Benchmarks'", echo = true).check other_isabelle.isabelle_home_user.file.delete execute(tmp_dir, "chmod -R a+r " + Bash.string(release.dist_name)) execute(tmp_dir, "chmod -R g=o " + Bash.string(release.dist_name)) execute_tar(tmp_dir, "-czf " + File.bash_path(release.isabelle_library_archive) + " " + Bash.string(release.dist_name + "/browser_info")) }) } } release } /** command line entry point **/ def main(args: Array[String]): Unit = { Command_Line.tool { var afp_rev = "" var components_base: Path = Components.default_components_base var proper_release_name: Option[String] = None var website: Option[Path] = None var build_sessions: List[String] = Nil var more_components: List[Path] = Nil var parallel_jobs = 1 var build_library = false var options = Options.init() var platform_families = default_platform_families var rev = "" val getopts = Getopts(""" Usage: Admin/build_release [OPTIONS] BASE_DIR Options are: -A REV corresponding AFP changeset id -C DIR base directory for Isabelle components (default: """ + Components.default_components_base + """) -R RELEASE proper release with name -W WEBSITE produce minimal website in given directory -b SESSIONS build platform-specific session images (separated by commas) -c ARCHIVE clean bundling with additional component .tar.gz archive -j INT maximum number of parallel jobs (default 1) -l build library -o OPTION override Isabelle system OPTION (via NAME=VAL or NAME) -p NAMES platform families (default: """ + default_platform_families.mkString(",") + """) -r REV Mercurial changeset id (default: RELEASE or tip) Build Isabelle release in base directory, using the local repository clone. """, "A:" -> (arg => afp_rev = arg), "C:" -> (arg => components_base = Path.explode(arg)), "R:" -> (arg => proper_release_name = Some(arg)), "W:" -> (arg => website = Some(Path.explode(arg))), "b:" -> (arg => build_sessions = space_explode(',', arg)), "c:" -> (arg => { val path = Path.explode(arg) Components.Archive.get_name(path.file_name) more_components = more_components ::: List(path) }), "j:" -> (arg => parallel_jobs = Value.Int.parse(arg)), "l" -> (_ => build_library = true), "o:" -> (arg => options = options + arg), "p:" -> (arg => platform_families = space_explode(',', arg).map(Platform.Family.parse)), "r:" -> (arg => rev = arg)) val more_args = getopts(args) val base_dir = more_args match { case List(base_dir) => base_dir case _ => getopts.usage() } val progress = new Console_Progress() if (platform_families.contains(Platform.Family.windows) && !Isabelle_System.bash("7z i").ok) error("Building for windows requires 7z") build_release(Path.explode(base_dir), options, components_base = components_base, progress = progress, rev = rev, afp_rev = afp_rev, proper_release_name = proper_release_name, website = website, platform_families = if (platform_families.isEmpty) default_platform_families else platform_families, more_components = more_components, build_sessions = build_sessions, build_library = build_library, parallel_jobs = parallel_jobs) } } } diff --git a/src/Pure/PIDE/xml.scala b/src/Pure/PIDE/xml.scala --- a/src/Pure/PIDE/xml.scala +++ b/src/Pure/PIDE/xml.scala @@ -1,457 +1,458 @@ /* Title: Pure/PIDE/xml.scala Author: Makarius Untyped XML trees and basic data representation. */ package isabelle object XML { /** XML trees **/ /* datatype representation */ type Attribute = Properties.Entry type Attributes = Properties.T sealed abstract class Tree { override def toString: String = string_of_tree(this) } type Body = List[Tree] case class Elem(markup: Markup, body: Body) extends Tree { private lazy val hash: Int = (markup, body).hashCode() override def hashCode(): Int = hash def name: String = markup.name def update_attributes(more_attributes: Attributes): Elem = if (more_attributes.isEmpty) this else Elem(markup.update_properties(more_attributes), body) def + (att: Attribute): Elem = Elem(markup + att, body) } case class Text(content: String) extends Tree { private lazy val hash: Int = content.hashCode() override def hashCode(): Int = hash } def elem(markup: Markup): XML.Elem = XML.Elem(markup, Nil) def elem(name: String, body: Body): XML.Elem = XML.Elem(Markup(name, Nil), body) def elem(name: String): XML.Elem = XML.Elem(Markup(name, Nil), Nil) val no_text: Text = Text("") val newline: Text = Text("\n") /* name space */ object Namespace { def apply(prefix: String, target: String): Namespace = new Namespace(prefix, target) } final class Namespace private(prefix: String, target: String) { def apply(name: String): String = prefix + ":" + name val attribute: XML.Attribute = ("xmlns:" + prefix, target) override def toString: String = attribute.toString } /* wrapped elements */ val XML_ELEM = "xml_elem" val XML_NAME = "xml_name" val XML_BODY = "xml_body" object Wrapped_Elem { def apply(markup: Markup, body1: Body, body2: Body): XML.Elem = XML.Elem(Markup(XML_ELEM, (XML_NAME, markup.name) :: markup.properties), XML.Elem(Markup(XML_BODY, Nil), body1) :: body2) def unapply(tree: Tree): Option[(Markup, Body, Body)] = tree match { case XML.Elem(Markup(XML_ELEM, (XML_NAME, name) :: props), XML.Elem(Markup(XML_BODY, Nil), body1) :: body2) => Some(Markup(name, props), body1, body2) case _ => None } } object Root_Elem { def apply(body: Body): XML.Elem = XML.Elem(Markup(XML_ELEM, Nil), body) def unapply(tree: Tree): Option[Body] = tree match { case XML.Elem(Markup(XML_ELEM, Nil), body) => Some(body) case _ => None } } /* traverse text */ def traverse_text[A](body: Body)(a: A)(op: (A, String) => A): A = { def traverse(x: A, t: Tree): A = t match { case XML.Wrapped_Elem(_, _, ts) => ts.foldLeft(x)(traverse) case XML.Elem(_, ts) => ts.foldLeft(x)(traverse) case XML.Text(s) => op(x, s) } body.foldLeft(a)(traverse) } def text_length(body: Body): Int = traverse_text(body)(0) { case (n, s) => n + s.length } /* text content */ def content(body: Body): String = { val text = new StringBuilder(text_length(body)) traverse_text(body)(()) { case (_, s) => text.append(s) } text.toString } def content(tree: Tree): String = content(List(tree)) /** string representation **/ val header: String = "\n" def output_char(s: StringBuilder, c: Char, permissive: Boolean = false): Unit = { c match { case '<' => s ++= "<" case '>' => s ++= ">" case '&' => s ++= "&" case '"' if !permissive => s ++= """ case '\'' if !permissive => s ++= "'" case _ => s += c } } def output_string(s: StringBuilder, str: String, permissive: Boolean = false): Unit = { if (str == null) s ++= str else str.iterator.foreach(output_char(s, _, permissive = permissive)) } def output_elem(s: StringBuilder, markup: Markup, end: Boolean = false): Unit = { s += '<' s ++= markup.name for ((a, b) <- markup.properties) { s += ' ' s ++= a s += '=' s += '"' output_string(s, b) s += '"' } if (end) s += '/' s += '>' } def output_elem_end(s: StringBuilder, name: String): Unit = { s += '<' s += '/' s ++= name s += '>' } def string_of_body(body: Body): String = { val s = new StringBuilder def tree(t: Tree): Unit = t match { case XML.Elem(markup, Nil) => output_elem(s, markup, end = true) case XML.Elem(markup, ts) => output_elem(s, markup) ts.foreach(tree) output_elem_end(s, markup.name) case XML.Text(txt) => output_string(s, txt) } body.foreach(tree) s.toString } def string_of_tree(tree: XML.Tree): String = string_of_body(List(tree)) + def text(s: String): String = string_of_tree(XML.Text(s)) /** cache **/ object Cache { def make( xz: XZ.Cache = XZ.Cache.make(), max_string: Int = isabelle.Cache.default_max_string, initial_size: Int = isabelle.Cache.default_initial_size): Cache = new Cache(xz, max_string, initial_size) val none: Cache = make(XZ.Cache.none, max_string = 0) } class Cache private[XML](val xz: XZ.Cache, max_string: Int, initial_size: Int) extends isabelle.Cache(max_string, initial_size) { protected def cache_props(x: Properties.T): Properties.T = { if (x.isEmpty) x else lookup(x) match { case Some(y) => y case None => store(x.map(p => (Library.isolate_substring(p._1).intern, cache_string(p._2)))) } } protected def cache_markup(x: Markup): Markup = { lookup(x) match { case Some(y) => y case None => x match { case Markup(name, props) => store(Markup(cache_string(name), cache_props(props))) } } } protected def cache_tree(x: XML.Tree): XML.Tree = { lookup(x) match { case Some(y) => y case None => x match { case XML.Elem(markup, body) => store(XML.Elem(cache_markup(markup), cache_body(body))) case XML.Text(text) => store(XML.Text(cache_string(text))) } } } protected def cache_body(x: XML.Body): XML.Body = { if (x.isEmpty) x else lookup(x) match { case Some(y) => y case None => x.map(cache_tree) } } // support hash-consing def tree0(x: XML.Tree): XML.Tree = if (no_cache) x else synchronized { lookup(x) getOrElse store(x) } // main methods def props(x: Properties.T): Properties.T = if (no_cache) x else synchronized { cache_props(x) } def markup(x: Markup): Markup = if (no_cache) x else synchronized { cache_markup(x) } def tree(x: XML.Tree): XML.Tree = if (no_cache) x else synchronized { cache_tree(x) } def body(x: XML.Body): XML.Body = if (no_cache) x else synchronized { cache_body(x) } def elem(x: XML.Elem): XML.Elem = if (no_cache) x else synchronized { cache_tree(x).asInstanceOf[XML.Elem] } } /** XML as data representation language **/ abstract class Error(s: String) extends Exception(s) class XML_Atom(s: String) extends Error(s) class XML_Body(body: XML.Body) extends Error("") object Encode { type T[A] = A => XML.Body type V[A] = PartialFunction[A, (List[String], XML.Body)] type P[A] = PartialFunction[A, List[String]] /* atomic values */ def long_atom(i: Long): String = Library.signed_string_of_long(i) def int_atom(i: Int): String = Library.signed_string_of_int(i) def bool_atom(b: Boolean): String = if (b) "1" else "0" def unit_atom(u: Unit) = "" /* structural nodes */ private def node(ts: XML.Body): XML.Tree = XML.Elem(Markup(":", Nil), ts) private def vector(xs: List[String]): XML.Attributes = xs.zipWithIndex.map({ case (x, i) => (int_atom(i), x) }) private def tagged(tag: Int, data: (List[String], XML.Body)): XML.Tree = XML.Elem(Markup(int_atom(tag), vector(data._1)), data._2) /* representation of standard types */ val tree: T[XML.Tree] = (t => List(t)) val properties: T[Properties.T] = (props => List(XML.Elem(Markup(":", props), Nil))) val string: T[String] = (s => if (s.isEmpty) Nil else List(XML.Text(s))) val long: T[Long] = (x => string(long_atom(x))) val int: T[Int] = (x => string(int_atom(x))) val bool: T[Boolean] = (x => string(bool_atom(x))) val unit: T[Unit] = (x => string(unit_atom(x))) def pair[A, B](f: T[A], g: T[B]): T[(A, B)] = (x => List(node(f(x._1)), node(g(x._2)))) def triple[A, B, C](f: T[A], g: T[B], h: T[C]): T[(A, B, C)] = (x => List(node(f(x._1)), node(g(x._2)), node(h(x._3)))) def list[A](f: T[A]): T[List[A]] = (xs => xs.map((x: A) => node(f(x)))) def option[A](f: T[A]): T[Option[A]] = { case None => Nil case Some(x) => List(node(f(x))) } def variant[A](fs: List[V[A]]): T[A] = { case x => val (f, tag) = fs.iterator.zipWithIndex.find(p => p._1.isDefinedAt(x)).get List(tagged(tag, f(x))) } } object Decode { type T[A] = XML.Body => A type V[A] = (List[String], XML.Body) => A type P[A] = PartialFunction[List[String], A] /* atomic values */ def long_atom(s: String): Long = try { java.lang.Long.parseLong(s) } catch { case e: NumberFormatException => throw new XML_Atom(s) } def int_atom(s: String): Int = try { Integer.parseInt(s) } catch { case e: NumberFormatException => throw new XML_Atom(s) } def bool_atom(s: String): Boolean = if (s == "1") true else if (s == "0") false else throw new XML_Atom(s) def unit_atom(s: String): Unit = if (s == "") () else throw new XML_Atom(s) /* structural nodes */ private def node(t: XML.Tree): XML.Body = t match { case XML.Elem(Markup(":", Nil), ts) => ts case _ => throw new XML_Body(List(t)) } private def vector(atts: XML.Attributes): List[String] = atts.iterator.zipWithIndex.map( { case ((a, x), i) => if (int_atom(a) == i) x else throw new XML_Atom(a) }).toList private def tagged(t: XML.Tree): (Int, (List[String], XML.Body)) = t match { case XML.Elem(Markup(name, atts), ts) => (int_atom(name), (vector(atts), ts)) case _ => throw new XML_Body(List(t)) } /* representation of standard types */ val tree: T[XML.Tree] = { case List(t) => t case ts => throw new XML_Body(ts) } val properties: T[Properties.T] = { case List(XML.Elem(Markup(":", props), Nil)) => props case ts => throw new XML_Body(ts) } val string: T[String] = { case Nil => "" case List(XML.Text(s)) => s case ts => throw new XML_Body(ts) } val long: T[Long] = (x => long_atom(string(x))) val int: T[Int] = (x => int_atom(string(x))) val bool: T[Boolean] = (x => bool_atom(string(x))) val unit: T[Unit] = (x => unit_atom(string(x))) def pair[A, B](f: T[A], g: T[B]): T[(A, B)] = { case List(t1, t2) => (f(node(t1)), g(node(t2))) case ts => throw new XML_Body(ts) } def triple[A, B, C](f: T[A], g: T[B], h: T[C]): T[(A, B, C)] = { case List(t1, t2, t3) => (f(node(t1)), g(node(t2)), h(node(t3))) case ts => throw new XML_Body(ts) } def list[A](f: T[A]): T[List[A]] = (ts => ts.map(t => f(node(t)))) def option[A](f: T[A]): T[Option[A]] = { case Nil => None case List(t) => Some(f(node(t))) case ts => throw new XML_Body(ts) } def variant[A](fs: List[V[A]]): T[A] = { case List(t) => val (tag, (xs, ts)) = tagged(t) val f = try { fs(tag) } catch { case _: IndexOutOfBoundsException => throw new XML_Body(List(t)) } f(xs, ts) case ts => throw new XML_Body(ts) } } } diff --git a/src/Pure/Thy/presentation.scala b/src/Pure/Thy/presentation.scala --- a/src/Pure/Thy/presentation.scala +++ b/src/Pure/Thy/presentation.scala @@ -1,793 +1,875 @@ /* Title: Pure/Thy/present.scala Author: Makarius HTML/PDF presentation of theory documents. */ package isabelle import scala.collection.immutable.SortedMap object Presentation { /** HTML documents **/ val fonts_path = Path.explode("fonts") sealed case class HTML_Document(title: String, content: String) def html_context(fonts_url: String => String = HTML.fonts_url()): HTML_Context = new HTML_Context(fonts_url) final class HTML_Context private[Presentation](fonts_url: String => String) { def init_fonts(dir: Path): Unit = { val fonts_dir = Isabelle_System.make_directory(dir + fonts_path) for (entry <- Isabelle_Fonts.fonts(hidden = true)) Isabelle_System.copy_file(entry.path, fonts_dir) } def head(title: String, rest: XML.Body = Nil): XML.Tree = HTML.div("head", HTML.chapter(title) :: rest) def source(body: XML.Body): XML.Tree = HTML.pre("source", body) def contents(heading: String, items: List[XML.Body], css_class: String = "contents") : List[XML.Elem] = { if (items.isEmpty) Nil else List(HTML.div(css_class, List(HTML.section(heading), HTML.itemize(items)))) } def output_document(title: String, body: XML.Body): String = HTML.output_document( List( HTML.style(HTML.fonts_css(fonts_url) + "\n\n" + File.read(HTML.isabelle_css)), HTML.title(title)), List(HTML.source(body)), css = "", structural = false) def html_document(title: String, body: XML.Body): HTML_Document = HTML_Document(title, output_document(title, body)) } /* presentation elements */ sealed case class Elements( html: Markup.Elements = Markup.Elements.empty, entity: Markup.Elements = Markup.Elements.empty, language: Markup.Elements = Markup.Elements.empty) val elements1: Elements = Elements( html = Rendering.foreground_elements ++ Rendering.text_color_elements + Markup.NUMERAL + Markup.COMMENT + Markup.ENTITY + Markup.LANGUAGE, entity = Markup.Elements(Markup.THEORY)) val elements2: Elements = Elements( html = elements1.html ++ Rendering.markdown_elements, language = Markup.Elements(Markup.Language.DOCUMENT)) /* HTML */ private val div_elements = Set(HTML.div.name, HTML.pre.name, HTML.par.name, HTML.list.name, HTML.enum.name, HTML.descr.name) def make_html( elements: Elements, entity_link: (Properties.T, XML.Body) => Option[XML.Tree], xml: XML.Body): XML.Body = { def html_div(html: XML.Body): Boolean = html exists { case XML.Elem(markup, body) => div_elements.contains(markup.name) || html_div(body) case XML.Text(_) => false } def html_class(c: String, html: XML.Body): XML.Body = if (c == "") html else if (html_div(html)) List(HTML.div(c, html)) else List(HTML.span(c, html)) def html_body(xml_body: XML.Body): XML.Body = xml_body flatMap { case XML.Wrapped_Elem(markup, _, body) => html_body(List(XML.Elem(markup, body))) case XML.Elem(Markup(Markup.ENTITY, props @ Markup.Kind(kind)), body) => val body1 = html_body(body) if (elements.entity(kind)) { entity_link(props, body1) match { case Some(link) => List(link) case None => body1 } } else body1 case XML.Elem(Markup(Markup.LANGUAGE, Markup.Name(name)), body) => html_class(if (elements.language(name)) name else "", html_body(body)) case XML.Elem(Markup(Markup.MARKDOWN_PARAGRAPH, _), body) => List(HTML.par(html_body(body))) case XML.Elem(Markup(Markup.MARKDOWN_ITEM, _), body) => List(HTML.item(html_body(body))) case XML.Elem(Markup(Markup.Markdown_Bullet.name, _), _) => Nil case XML.Elem(Markup.Markdown_List(kind), body) => if (kind == Markup.ENUMERATE) List(HTML.enum(html_body(body))) else List(HTML.list(html_body(body))) case XML.Elem(markup, body) => val name = markup.name val html = markup.properties match { case Markup.Kind(kind) if kind == Markup.COMMAND || kind == Markup.KEYWORD => html_class(kind, html_body(body)) case _ => html_body(body) } Rendering.foreground.get(name) orElse Rendering.text_color.get(name) match { case Some(c) => html_class(c.toString, html) case None => html_class(name, html) } case XML.Text(text) => HTML.text(Symbol.decode(text)) } html_body(xml) } /* PIDE HTML document */ def html_document( resources: Resources, snapshot: Document.Snapshot, html_context: HTML_Context, elements: Elements, plain_text: Boolean = false): HTML_Document = { require(!snapshot.is_outdated, "document snapshot outdated") val name = snapshot.node_name if (plain_text) { val title = "File " + Symbol.cartouche_decoded(name.path.file_name) val body = HTML.text(snapshot.node.source) html_context.html_document(title, body) } else { resources.html_document(snapshot) getOrElse { val title = if (name.is_theory) "Theory " + quote(name.theory_base_name) else "File " + Symbol.cartouche_decoded(name.path.file_name) val body = make_html(elements, (_, _) => None, snapshot.xml_markup(elements = elements.html)) html_context.html_document(title, body) } } } /** PDF LaTeX documents **/ /* document info */ abstract class Document_Name { def name: String def path: Path = Path.basic(name) override def toString: String = name } object Document_Variant { def parse(name: String, tags: String): Document_Variant = Document_Variant(name, Library.space_explode(',', tags)) def parse(opt: String): Document_Variant = Library.space_explode('=', opt) match { case List(name) => Document_Variant(name, Nil) case List(name, tags) => parse(name, tags) case _ => error("Malformed document variant: " + quote(opt)) } } sealed case class Document_Variant(name: String, tags: List[String]) extends Document_Name { def print_tags: String = tags.mkString(",") def print: String = if (tags.isEmpty) name else name + "=" + print_tags def latex_sty: String = Library.terminate_lines( tags.map(tag => tag.toList match { case '/' :: cs => "\\isafoldtag{" + cs.mkString + "}" case '-' :: cs => "\\isadroptag{" + cs.mkString + "}" case '+' :: cs => "\\isakeeptag{" + cs.mkString + "}" case cs => "\\isakeeptag{" + cs.mkString + "}" })) } sealed case class Document_Input(name: String, sources: SHA1.Digest) extends Document_Name sealed case class Document_Output(name: String, sources: SHA1.Digest, log_xz: Bytes, pdf: Bytes) extends Document_Name { def log: String = log_xz.uncompress().text def log_lines: List[String] = split_lines(log) def write(db: SQL.Database, session_name: String): Unit = write_document(db, session_name, this) } /* SQL data model */ object Data { val session_name = SQL.Column.string("session_name").make_primary_key val name = SQL.Column.string("name").make_primary_key val sources = SQL.Column.string("sources") val log_xz = SQL.Column.bytes("log_xz") val pdf = SQL.Column.bytes("pdf") val table = SQL.Table("isabelle_documents", List(session_name, name, sources, log_xz, pdf)) def where_equal(session_name: String, name: String = ""): SQL.Source = "WHERE " + Data.session_name.equal(session_name) + (if (name == "") "" else " AND " + Data.name.equal(name)) } def read_documents(db: SQL.Database, session_name: String): List[Document_Input] = { val select = Data.table.select(List(Data.name, Data.sources), Data.where_equal(session_name)) db.using_statement(select)(stmt => stmt.execute_query().iterator(res => { val name = res.string(Data.name) val sources = res.string(Data.sources) Document_Input(name, SHA1.fake(sources)) }).toList) } def read_document(db: SQL.Database, session_name: String, name: String): Option[Document_Output] = { val select = Data.table.select(sql = Data.where_equal(session_name, name)) db.using_statement(select)(stmt => { val res = stmt.execute_query() if (res.next()) { val name = res.string(Data.name) val sources = res.string(Data.sources) val log_xz = res.bytes(Data.log_xz) val pdf = res.bytes(Data.pdf) Some(Document_Output(name, SHA1.fake(sources), log_xz, pdf)) } else None }) } def write_document(db: SQL.Database, session_name: String, doc: Document_Output): Unit = { db.using_statement(Data.table.insert())(stmt => { stmt.string(1) = session_name stmt.string(2) = doc.name stmt.string(3) = doc.sources.toString stmt.bytes(4) = doc.log_xz stmt.bytes(5) = doc.pdf stmt.execute() }) } /* presentation context */ object Context { val none: Context = new Context { def enabled: Boolean = false } val standard: Context = new Context { def enabled: Boolean = true } def dir(path: Path): Context = new Context { def enabled: Boolean = true override def dir(store: Sessions.Store): Path = path } def make(s: String): Context = if (s == ":") standard else dir(Path.explode(s)) } abstract class Context private { def enabled: Boolean def enabled(info: Sessions.Info): Boolean = enabled || info.browser_info def dir(store: Sessions.Store): Path = store.presentation_dir def dir(store: Sessions.Store, info: Sessions.Info): Path = dir(store) + Path.explode(info.chapter_session) } /** HTML presentation **/ /* maintain chapter index */ private val sessions_path = Path.basic(".sessions") private def read_sessions(dir: Path): List[(String, String)] = { val path = dir + sessions_path if (path.is_file) { import XML.Decode._ list(pair(string, string))(Symbol.decode_yxml(File.read(path))) } else Nil } private def write_sessions(dir: Path, sessions: List[(String, String)]): Unit = { import XML.Encode._ File.write(dir + sessions_path, YXML.string_of_body(list(pair(string, string))(sessions))) } def update_chapter_index( browser_info: Path, chapter: String, new_sessions: List[(String, String)]): Unit = { val dir = Isabelle_System.make_directory(browser_info + Path.basic(chapter)) val sessions0 = try { read_sessions(dir) } catch { case _: XML.Error => Nil } val sessions = (SortedMap.empty[String, String] ++ sessions0 ++ new_sessions).toList write_sessions(dir, sessions) val title = "Isabelle/" + chapter + " sessions" HTML.write_document(dir, "index.html", List(HTML.title(title + Isabelle_System.isabelle_heading())), HTML.chapter(title) :: (if (sessions.isEmpty) Nil else List(HTML.div("sessions", List(HTML.description( sessions.map({ case (name, description) => val descr = Symbol.trim_blank_lines(description) (List(HTML.link(name + "/index.html", HTML.text(name))), if (descr == "") Nil else HTML.break ::: List(HTML.pre(HTML.text(descr)))) }))))))) } def make_global_index(browser_info: Path): Unit = { if (!(browser_info + Path.explode("index.html")).is_file) { Isabelle_System.make_directory(browser_info) Isabelle_System.copy_file(Path.explode("~~/lib/logo/isabelle.gif"), browser_info + Path.explode("isabelle.gif")) + val title = "The " + XML.text(Isabelle_System.isabelle_name()) + " Library" File.write(browser_info + Path.explode("index.html"), - File.read(Path.explode("~~/lib/html/library_index_header.template")) + - File.read(Path.explode("~~/lib/html/library_index_content.template")) + - File.read(Path.explode("~~/lib/html/library_index_footer.template"))) +""" + + + + + + """ + title + """ + + + +
+ + + + + + +
[Isabelle] + + + + +
""" + title + """
+
+
+
+ + + + + + + +""") } } /* present session */ val session_graph_path = Path.explode("session_graph.pdf") val readme_path = Path.explode("README.html") val files_path = Path.explode("files") def html_name(name: Document.Node.Name): String = name.theory_base_name + ".html" def theory_link(deps: Sessions.Deps, session0: String, name: Document.Node.Name, body: XML.Body): Option[XML.Tree] = { val session1 = deps(session0).theory_qualifier(name) val info0 = deps.sessions_structure.get(session0) val info1 = deps.sessions_structure.get(session1) if (info0.isDefined && info1.isDefined) { Some(HTML.link(info0.get.relative_path(info1.get) + html_name(name), body)) } else None } def session_html( resources: Resources, session: String, deps: Sessions.Deps, db_context: Sessions.Database_Context, progress: Progress = new Progress, verbose: Boolean = false, html_context: HTML_Context, elements: Elements, presentation: Context): Unit = { val info = deps.sessions_structure(session) val options = info.options val base = deps(session) val session_dir = presentation.dir(db_context.store, info) html_context.init_fonts(session_dir) Bytes.write(session_dir + session_graph_path, graphview.Graph_File.make_pdf(options, base.session_graph_display)) val documents = for { doc <- info.document_variants document <- db_context.input_database(session)(read_document(_, _, doc.name)) } yield { if (verbose) progress.echo("Presenting document " + session + "/" + doc.name) Bytes.write(session_dir + doc.path.pdf, document.pdf) doc } val view_links = { val deps_link = HTML.link(session_graph_path, HTML.text("theory dependencies")) val readme_links = if ((info.dir + readme_path).is_file) { Isabelle_System.copy_file(info.dir + readme_path, session_dir + readme_path) List(HTML.link(readme_path, HTML.text("README"))) } else Nil val document_links = documents.map(doc => HTML.link(doc.path.pdf, HTML.text(doc.name))) Library.separate(HTML.break ::: HTML.nl, (deps_link :: readme_links ::: document_links). map(link => HTML.text("View ") ::: List(link))).flatten } val theories: List[XML.Body] = { var seen_files = List.empty[(Path, String, Document.Node.Name)] def entity_link(props: Properties.T, body: XML.Body): Option[XML.Tree] = (props, props, props) match { case (Markup.Kind(Markup.THEORY), Markup.Name(theory), Position.Def_File(thy_file)) => val node_name = resources.file_node(Path.explode(thy_file), theory = theory) theory_link(deps, session, node_name, body) case _ => None } sealed case class Theory( name: Document.Node.Name, command: Command, files_html: List[(Path, XML.Tree)], html: XML.Tree) def read_theory(name: Document.Node.Name): Option[Theory] = { progress.expose_interrupt() if (verbose) progress.echo("Presenting theory " + name) for (command <- Build_Job.read_theory(db_context, resources, session, name.theory)) yield { val snapshot = Document.State.init.snippet(command) val files_html = for { (src_path, xml) <- snapshot.xml_markup_blobs(elements = elements.html) if xml.nonEmpty } yield { progress.expose_interrupt() if (verbose) progress.echo("Presenting file " + src_path) (src_path, html_context.source(make_html(elements, entity_link, xml))) } val html = html_context.source( make_html(elements, entity_link, snapshot.xml_markup(elements = elements.html))) Theory(name, command, files_html, html) } } for (thy <- Par_List.map(read_theory, base.session_theories).flatten) yield { val files = for { (src_path, file_html) <- thy.files_html } yield { val file_name = (files_path + src_path.squash.html).implode seen_files.find(p => p._1 == src_path || p._2 == file_name) match { case None => seen_files ::= (src_path, file_name, thy.name) case Some((_, _, thy_name1)) => error("Incoherent use of file name " + src_path + " as " + quote(file_name) + " in theory " + thy_name1 + " vs. " + thy.name) } val file_path = session_dir + Path.explode(file_name) html_context.init_fonts(file_path.dir) val file_title = "File " + Symbol.cartouche_decoded(src_path.implode_short) HTML.write_document(file_path.dir, file_path.file_name, List(HTML.title(file_title)), List(html_context.head(file_title), file_html)) List(HTML.link(file_name, HTML.text(file_title))) } val thy_title = "Theory " + thy.name.theory_base_name HTML.write_document(session_dir, html_name(thy.name), List(HTML.title(thy_title)), List(html_context.head(thy_title), thy.html)) List(HTML.link(html_name(thy.name), HTML.text(thy.name.theory_base_name) ::: (if (files.isEmpty) Nil else List(HTML.itemize(files))))) } } val title = "Session " + session HTML.write_document(session_dir, "index.html", List(HTML.title(title + Isabelle_System.isabelle_heading())), html_context.head(title, List(HTML.par(view_links))) :: html_context.contents("Theories", theories)) } /** build documents **/ val session_tex_path = Path.explode("session.tex") def tex_name(name: Document.Node.Name): String = name.theory_base_name + ".tex" def document_tex_name(name: Document.Node.Name): String = "document/" + tex_name(name) class Build_Error(val log_lines: List[String], val message: String) extends Exn.User_Error(message) def build_documents( session: String, deps: Sessions.Deps, db_context: Sessions.Database_Context, progress: Progress = new Progress, output_sources: Option[Path] = None, output_pdf: Option[Path] = None, verbose: Boolean = false, verbose_latex: Boolean = false): List[Document_Output] = { /* session info */ val info = deps.sessions_structure(session) val hierarchy = deps.sessions_structure.hierarchy(session) val options = info.options val base = deps(session) val graph_pdf = graphview.Graph_File.make_pdf(options, base.session_graph_display) /* prepare document directory */ lazy val tex_files = for (name <- base.session_theories ::: base.document_theories) yield { val entry = db_context.get_export(hierarchy, name.theory, document_tex_name(name)) Path.basic(tex_name(name)) -> entry.uncompressed } def prepare_dir1(dir: Path, doc: Document_Variant): (Path, String) = { val doc_dir = dir + Path.basic(doc.name) Isabelle_System.make_directory(doc_dir) Isabelle_System.bash("isabelle latex -o sty", cwd = doc_dir.file).check File.write(doc_dir + Path.explode("isabelletags.sty"), doc.latex_sty) for ((base_dir, src) <- info.document_files) { Isabelle_System.copy_file_base(info.dir + base_dir, src, doc_dir) } File.write(doc_dir + session_tex_path, Library.terminate_lines( base.session_theories.map(name => "\\input{" + tex_name(name) + "}"))) for ((path, tex) <- tex_files) Bytes.write(doc_dir + path, tex) val root1 = "root_" + doc.name val root = if ((doc_dir + Path.explode(root1).tex).is_file) root1 else "root" (doc_dir, root) } def prepare_dir2(dir: Path, doc: Document_Variant): Unit = { val doc_dir = dir + Path.basic(doc.name) // non-deterministic, but irrelevant Bytes.write(doc_dir + session_graph_path, graph_pdf) } /* produce documents */ val documents = for (doc <- info.documents) yield { Isabelle_System.with_tmp_dir("document")(tmp_dir => { progress.echo("Preparing " + session + "/" + doc.name + " ...") val start = Time.now() // prepare sources val (doc_dir, root) = prepare_dir1(tmp_dir, doc) val digests = File.find_files(doc_dir.file, follow_links = true).map(SHA1.digest) val sources = SHA1.digest_set(digests) prepare_dir2(tmp_dir, doc) for (dir <- output_sources) { prepare_dir1(dir, doc) prepare_dir2(dir, doc) } // old document from database val old_document = for { old_doc <- db_context.input_database(session)(read_document(_, _, doc.name)) if old_doc.sources == sources } yield { Bytes.write(doc_dir + doc.path.pdf, old_doc.pdf) old_doc } old_document getOrElse { // bash scripts def root_bash(ext: String): String = Bash.string(root + "." + ext) def latex_bash(fmt: String = "pdf", ext: String = "tex"): String = "isabelle latex -o " + Bash.string(fmt) + " " + Bash.string(root + "." + ext) def bash(items: String*): Process_Result = progress.bash(items.mkString(" && "), cwd = doc_dir.file, echo = verbose_latex, watchdog = Time.seconds(0.5)) // prepare document val result = if ((doc_dir + Path.explode("build")).is_file) { bash("./build pdf " + Bash.string(doc.name)) } else { bash( latex_bash(), "{ [ ! -f " + root_bash("bib") + " ] || " + latex_bash("bbl") + "; }", "{ [ ! -f " + root_bash("idx") + " ] || " + latex_bash("idx") + "; }", latex_bash(), latex_bash()) } // result val root_pdf = Path.basic(root).pdf val result_path = doc_dir + root_pdf val log_lines = result.out_lines ::: result.err_lines val errors = (if (result.ok) Nil else List(result.err)) ::: Latex.latex_errors(doc_dir, root) ::: Bibtex.bibtex_errors(doc_dir, root) if (errors.nonEmpty) { val message = Exn.cat_message( (errors ::: List("Failed to build document " + quote(doc.name))):_*) throw new Build_Error(log_lines, message) } else if (!result_path.is_file) { val message = "Bad document result: expected to find " + root_pdf throw new Build_Error(log_lines, message) } else { val stop = Time.now() val timing = stop - start progress.echo("Finished " + session + "/" + doc.name + " (" + timing.message_hms + " elapsed time)") val log_xz = Bytes(cat_lines(log_lines)).compress() val pdf = Bytes.read(result_path) Document_Output(doc.name, sources, log_xz, pdf) } } }) } for (dir <- output_pdf; doc <- documents) { Isabelle_System.make_directory(dir) val path = dir + doc.path.pdf Bytes.write(path, doc.pdf) progress.echo("Document at " + path.absolute) } documents } /* Isabelle tool wrapper */ val isabelle_tool = Isabelle_Tool("document", "prepare session theory document", Scala_Project.here, args => { var output_sources: Option[Path] = None var output_pdf: Option[Path] = None var verbose_latex = false var dirs: List[Path] = Nil var options = Options.init() var verbose_build = false val getopts = Getopts( """ Usage: isabelle document [OPTIONS] SESSION Options are: -O DIR output directory for LaTeX sources and resulting PDF -P DIR output directory for resulting PDF -S DIR output directory for LaTeX sources -V verbose latex -d DIR include session directory -o OPTION override Isabelle system OPTION (via NAME=VAL or NAME) -v verbose build Prepare the theory document of a session. """, "O:" -> (arg => { val dir = Path.explode(arg) output_sources = Some(dir) output_pdf = Some(dir) }), "P:" -> (arg => { output_pdf = Some(Path.explode(arg)) }), "S:" -> (arg => { output_sources = Some(Path.explode(arg)) }), "V" -> (_ => verbose_latex = true), "d:" -> (arg => dirs = dirs ::: List(Path.explode(arg))), "o:" -> (arg => options = options + arg), "v" -> (_ => verbose_build = true)) val more_args = getopts(args) val session = more_args match { case List(a) => a case _ => getopts.usage() } val progress = new Console_Progress(verbose = verbose_build) val store = Sessions.store(options) progress.interrupt_handler { val res = Build.build(options, selection = Sessions.Selection.session(session), dirs = dirs, progress = progress, verbose = verbose_build) if (!res.ok) error("Failed to build session " + quote(session)) val deps = Sessions.load_structure(options + "document=pdf", dirs = dirs). selection_deps(Sessions.Selection.session(session)) if (output_sources.isEmpty && output_pdf.isEmpty) { progress.echo_warning("No output directory") } using(store.open_database_context())(db_context => build_documents(session, deps, db_context, progress = progress, output_sources = output_sources, output_pdf = output_pdf, verbose = true, verbose_latex = verbose_latex)) } }) }