# HG changeset patch # User wenzelm # Date 1540139553 -7200 # Node ID 68816d1c73a75fdbf3de88cfb24008943b49a26b # Parent 9456ba57372921de2aab4ee3e43b1a5a74304d17 eliminated "isabelle makedist" -- prefer Scala over bash/perl scripting; eliminated "isabelle news"; roper title in NEWS.html; more robust build of documentation, using proper Other_Isabelle settings: avoid conflict with enclosing ISABELLE_OCAML / ISABELLE_GHC; misc tuning and clarification; diff -r 9456ba573729 -r 68816d1c73a7 Admin/lib/Tools/makedist --- a/Admin/lib/Tools/makedist Sun Oct 21 14:35:46 2018 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,246 +0,0 @@ -#!/usr/bin/env bash -# -# Author: Makarius -# -# DESCRIPTION: make Isabelle distribution from repository - -## global parameters - -umask 022 - -HG="${HG:-hg}" - -DISTPREFIX="${DISTPREFIX:-$HOME/tmp/isadist}" - - -## diagnostics - -PRG="$(basename "$0")" - -function usage() -{ - echo - echo "Usage: isabelle $PRG [OPTIONS] [VERSION]" - echo - echo " Options are:" - echo " -O official release (not release-candidate)" - echo " -d DIR global directory prefix (default: \"$DISTPREFIX\")" - echo " -j INT maximum number of parallel jobs (default 1)" - echo " -r RELEASE proper release with name" - echo - echo " Make Isabelle distribution from the local repository clone." - echo - echo " VERSION identifies the snapshot, using usual Mercurial terminology;" - echo " the default is RELEASE if given, otherwise \"tip\"." - echo - echo " Add-on components are that of the running Isabelle version!" - echo - exit 1 -} - -function fail() -{ - echo "$1" >&2 - exit 2 -} - -function check_number() -{ - [ -n "$1" -a -z "$(echo "$1" | tr -d '[0-9]')" ] || fail "Bad number: \"$1\"" -} - - -## process command line - -# options - -OFFICIAL_RELEASE="false" -JOBS="" -RELEASE="" - -while getopts "Od:j:r:" OPT -do - case "$OPT" in - O) - OFFICIAL_RELEASE="true" - ;; - d) - DISTPREFIX="$OPTARG" - ;; - j) - check_number "$OPTARG" - JOBS="-j $OPTARG" - ;; - r) - RELEASE="$OPTARG" - ;; - \?) - usage - ;; - esac -done - -shift $(($OPTIND - 1)) - - -# args - -VERSION="" -[ "$#" -gt 0 ] && { VERSION="$1"; shift; } -[ -z "$VERSION" ] && VERSION="$RELEASE" -[ -z "$VERSION" ] && VERSION="tip" - -[ "$#" -gt 0 ] && usage - -IDENT=$("$HG" --repository "$ISABELLE_HOME" id -r "$VERSION" -i) -[ -z "$IDENT" ] && fail "Bad repository version: \"$VERSION\"" - - -## main - -# dist name - -DATE=$(env LC_ALL=C date "+%d-%b-%Y") -DISTDATE=$(env LC_ALL=C date "+%B %Y") - -if [ -z "$RELEASE" ]; then - DISTNAME="Isabelle_$DATE" - DISTVERSION="Isabelle repository snapshot $IDENT $DATE" -else - DISTNAME="$RELEASE" - DISTVERSION="$DISTNAME: $DISTDATE" -fi - -DISTPREFIX="$(cd "$DISTPREFIX"; pwd)" -DISTBASE="$DISTPREFIX/dist-$DISTNAME" -mkdir -p "$DISTBASE" || fail "Unable to create distribution base dir \"$DISTBASE\"" - -DIR="$DISTBASE/$DISTNAME" -[ -e "$DIR" ] && fail "Directory \"$DIR\" already exists" - -rm -f "$DISTPREFIX/ISABELLE_DIST" "$DISTPREFIX/ISABELLE_IDENT" - - -# retrieve repository archive - -echo "### Retrieving Mercurial repository version $VERSION" - -"$HG" --repository "$ISABELLE_HOME" archive --type files -r "$IDENT" "$DIR" || \ - fail "Failed to retrieve $VERSION" - -rm -f "$DIR/.hg_archival.txt" -rm -f "$DIR/.hgtags" -rm -f "$DIR/.hgignore" -rm -f "$DIR/README_REPOSITORY" - - -# partial context switch to new version - -cd "$DIR" - -unset ISABELLE_SETTINGS_PRESENT -unset ISABELLE_SITE_SETTINGS_PRESENT - -if [ -z "$RELEASE" ]; then - { - echo - echo "IMPORTANT NOTE" - echo "==============" - echo - echo "This is a snapshot of Isabelle/${IDENT} from the repository." - echo - } >ANNOUNCE -fi - -if [ -n "$RELEASE" -a "$OFFICIAL_RELEASE" = true ]; then - IS_OFFICIAL="true" -else - IS_OFFICIAL="false" -fi - -perl -pi \ - -e "s,val is_identified = false,val is_identified = true,g;" \ - -e "s,val is_official = false,val is_official = ${IS_OFFICIAL},g;" \ - src/Pure/System/distribution.ML src/Pure/System/distribution.scala - -perl -pi -e "s,ISABELLE_ID=\"\",ISABELLE_ID=\"$IDENT\",g" lib/scripts/getsettings -perl -pi -e "s,ISABELLE_IDENTIFIER=\"\",ISABELLE_IDENTIFIER=\"$DISTNAME\",g" lib/scripts/getsettings -perl -pi -e "s,{ISABELLE},$DISTNAME,g" lib/html/library_index_header.template -perl -pi -e "s,repository version,$DISTVERSION,g" \ - src/Pure/System/distribution.ML src/Pure/System/distribution.scala lib/Tools/version -perl -pi -e "s,some repository version of Isabelle,$DISTVERSION,g" README - -mkdir -p contrib -cat >contrib/README </dev/null && function tar() { gnutar "$@"; } - -echo "### Creating archive" - -cd "$DISTBASE" - -echo "$DISTBASE/$DISTNAME.tar.gz" > "$DISTPREFIX/ISABELLE_DIST" -echo "$IDENT" > "$DISTPREFIX/ISABELLE_IDENT" - -chown -R "$LOGNAME" "$DISTNAME" -chmod -R g=o "$DISTNAME" -chmod -R u+w "$DISTNAME" -find "$DISTNAME" -type f "(" -name '*.scala' -o -name '*.ML' -o -name '*.thy' ")" -print | xargs chmod -f u-w - -echo "$DISTBASE/$DISTNAME.tar.gz" -tar -c -z -f "$DISTNAME.tar.gz" "$DISTNAME" -[ "$?" = 0 ] || exit "$?" - - -# cleanup dist - -mv "$DISTNAME" "${DISTNAME}-old" -mkdir "$DISTNAME" - -mv "${DISTNAME}-old/README" "${DISTNAME}-old/NEWS" "${DISTNAME}-old/ANNOUNCE" \ - "${DISTNAME}-old/COPYRIGHT" "${DISTNAME}-old/CONTRIBUTORS" "$DISTNAME" -mkdir "$DISTNAME/doc" -mv "${DISTNAME}-old/doc/"*.pdf \ - "${DISTNAME}-old/doc/"*.html \ - "${DISTNAME}-old/doc/"*.css \ - "${DISTNAME}-old/doc/fonts" \ - "${DISTNAME}-old/doc/Contents" "$DISTNAME/doc" - -rm -f Isabelle && ln -sf "$DISTNAME" Isabelle - -rm -rf "${DISTNAME}-old" diff -r 9456ba573729 -r 68816d1c73a7 src/Pure/Admin/build_release.scala --- a/src/Pure/Admin/build_release.scala Sun Oct 21 14:35:46 2018 +0200 +++ b/src/Pure/Admin/build_release.scala Sun Oct 21 18:32:33 2018 +0200 @@ -9,6 +9,101 @@ object Build_Release { + /** generated content **/ + + /* patch release */ + + private def change_file(dir: Path, name: String, f: String => String) + { + val file = dir + Path.explode(name) + File.write(file, f(File.read(file))) + } + + def patch_release( + dir: Path, ident: String, is_official: Boolean, dist_name: String, dist_version: String) + { + for (name <- List("src/Pure/System/distribution.ML", "src/Pure/System/distribution.scala")) + { + change_file(dir, name, + s => + s.replaceAll("val is_identified = false", "val is_identified = true") + .replaceAll("val is_official = false", "val is_official = " + is_official)) + } + + change_file(dir, "lib/scripts/getsettings", + s => + s.replaceAll("ISABELLE_ID=\"\"", "ISABELLE_ID=" + quote(ident)) + .replaceAll("ISABELLE_IDENTIFIER=\"\"", "ISABELLE_IDENTIFIER=" + quote(dist_name))) + + change_file(dir, "lib/html/library_index_header.template", + s => s.replaceAll("""\{ISABELLE\}""", dist_name)) + + for { + name <- + List( + "src/Pure/System/distribution.ML", + "src/Pure/System/distribution.scala", + "lib/Tools/version") } + { + change_file(dir, name, s => s.replaceAll("repository version", dist_version)) + } + + change_file(dir, "README", + s => s.replaceAll("some repository version of Isabelle", dist_version)) + } + + + /* ANNOUNCE */ + + def make_announce(dir: Path, ident: String) + { + File.write(dir + Path.explode("ANNOUNCE"), +""" +IMPORTANT NOTE +============== + +This is a snapshot of Isabelle/""" + ident + """ from the repository. + +""") + } + + + /* NEWS */ + + def make_news(other_isabelle: Other_Isabelle, dist_version: String) + { + val target = other_isabelle.isabelle_home + Path.explode("doc") + val target_fonts = target + Path.explode("fonts") + Isabelle_System.mkdirs(target_fonts) + + for (font <- other_isabelle.fonts(html = true)) + File.copy(font, 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")))))) + } + + + /* contrib */ + + def make_contrib(dir: Path) + { + Isabelle_System.mkdirs(dir + Path.explode("contrib")) + File.write(dir + Path.explode("contrib/README"), +"""This directory contains add-on components that contribute to the main +Isabelle distribution. Separate licensing conditions apply, see each +directory individually. +""") + } + + + + /** build_release **/ + sealed case class Bundle_Info( platform_family: String, platform_description: String, @@ -20,22 +115,35 @@ sealed case class Release( date: Date, - name: String, + dist_name: String, dist_dir: Path, - dist_archive: Path, - dist_library_archive: Path, - id: String) + ident: String) { + val isabelle_dir: Path = dist_dir + Path.explode(dist_name) + 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") + + val other_isabelle_identifier: String = dist_name + "-build" + val bundle_infos: List[Bundle_Info] = - List(Bundle_Info("linux", "Linux", name + "_app.tar.gz", None), - Bundle_Info("windows", "Windows", name + ".exe", None), - Bundle_Info("macos", "Mac OS X", name + ".dmg", Some(name + "_dmg.tar.gz"))) + List(Bundle_Info("linux", "Linux", dist_name + "_app.tar.gz", None), + Bundle_Info("windows", "Windows", dist_name + ".exe", None), + Bundle_Info("macos", "Mac OS X", dist_name + ".dmg", Some(dist_name + "_dmg.tar.gz"))) def bundle_info(platform_family: String): Bundle_Info = bundle_infos.find(bundle_info => bundle_info.platform_family == platform_family) getOrElse error("Unknown platform family " + quote(platform_family)) + + def execute_dist_name(dir: Path, script: String): Unit = + Isabelle_System.bash(script, cwd = dir.file, + env = Isabelle_System.settings() + ("DIST_NAME" -> dist_name)).check } + 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, cwd = dir.file).check private val default_platform_families = List("linux", "windows", "macos") @@ -44,60 +152,168 @@ rev: String = "", afp_rev: String = "", official_release: Boolean = false, - release_name: String = "", + proper_release_name: Option[String] = None, platform_families: List[String] = default_platform_families, website: Option[Path] = None, build_library: Boolean = false, parallel_jobs: Int = 1, remote_mac: String = ""): Release = { - /* release info */ - - Isabelle_System.mkdirs(base_dir) + /* make distribution */ val release = { - val date = Date.now() - val name = proper_string(release_name) getOrElse ("Isabelle_" + Date.Format.date(date)) - val dist_dir = base_dir + Path.explode("dist-" + name) - val dist_archive = dist_dir + Path.explode(name + ".tar.gz") - val dist_library_archive = dist_dir + Path.explode(name + "_library.tar.gz") - Release(date, name, dist_dir, dist_archive, dist_library_archive, "") - } + 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 + Release(date, dist_name, dist_dir, "") + } - val bundle_infos = platform_families.map(release.bundle_info(_)) - - - /* make distribution */ - - val jobs_option = " -j" + parallel_jobs.toString - - val release_id = - { val isabelle_ident_file = base_dir + Path.explode("ISABELLE_IDENT") val isabelle_dist_file = base_dir + Path.explode("ISABELLE_DIST") - if (release.dist_archive.is_file && - isabelle_ident_file.is_file && isabelle_dist_file.is_file && - File.eq(Path.explode(Library.trim_line(File.read(isabelle_dist_file))), - release.dist_archive)) { - progress.echo("### Release archive already exists: " + release.dist_archive.implode) - } - else { - progress.echo("Producing release archive " + release.dist_archive.implode + " ...") - progress.bash( - "isabelle makedist -d " + File.bash_path(base_dir) + jobs_option + - (if (official_release) " -O" else "") + - (if (release_name != "") " -r " + Bash.string(release_name) else "") + - (if (rev != "") " " + Bash.string(rev) else ""), - echo = true).check - } - Library.trim_line(File.read(isabelle_ident_file)) + val release_ident = + if (release.isabelle_archive.is_file && + isabelle_ident_file.is_file && isabelle_dist_file.is_file && + File.eq(Path.explode(Library.trim_line(File.read(isabelle_dist_file))), + release.isabelle_archive)) { + progress.echo("### Release archive already exists: " + release.isabelle_archive.implode) + File.read(isabelle_ident_file) + } + else { + progress.echo("Producing release archive " + release.isabelle_archive.implode + " ...") + + Isabelle_System.mkdirs(release.dist_dir) + + val hg = Mercurial.repository(Path.explode("$ISABELLE_HOME")) + val version = proper_release_name orElse proper_string(rev) getOrElse "tip" + val ident = + try { hg.id(version) } + catch { case ERROR(_) => error("Bad repository version: " + quote(version)) } + + val dist_version = + if (proper_release_name.isDefined) { + proper_release_name.get + ": " + Date.Format("LLLL uuuu")(release.date) + } + else "Isabelle repository snapshot " + ident + " " + Date.Format.date(release.date) + + if (release.isabelle_dir.is_dir) + error("Directory " + release.isabelle_dir + " already exists") + + isabelle_ident_file.file.delete + isabelle_dist_file.file.delete + + + progress.echo("### Retrieving Mercurial repository version " + quote(version)) + + try { + hg.archive(release.isabelle_dir.expand.implode, rev = ident, options = "--type files") + } + catch { case ERROR(_) => error("Failed to retrieve " + version + "(" + ident + ")") } + + for (name <- List(".hg_archival.txt", ".hgtags", ".hgignore", "README_REPOSITORY")) { + (release.isabelle_dir + Path.explode(name)).file.delete + } + + + progress.echo("### Preparing distribution " + quote(release.dist_name)) + + patch_release(release.isabelle_dir, ident, + proper_release_name.isDefined && official_release, release.dist_name, dist_version) + + if (proper_release_name.isEmpty) make_announce(release.isabelle_dir, ident) + + make_contrib(release.isabelle_dir) + + execute(release.isabelle_dir, + """find . "(" -name "*.thy" -o -name "*.ML" -o -name "*.scala" ")" -print | xargs chmod -f -x""") + execute(release.isabelle_dir, + """find . -print | xargs chmod -f u+rw""") + + + /* build tools and documentation */ + + val other_isabelle = + Other_Isabelle(release.isabelle_dir, + isabelle_identifier = release.other_isabelle_identifier, + progress = progress) + + other_isabelle.init_settings( + (base_dir.absolute + Path.explode("contrib")).implode, nonfree = false, Nil) + 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(_) => error("Failed to build tools") } + + try { + other_isabelle.bash( + "./bin/isabelle build_doc -a -s -j " + parallel_jobs, echo = true).check + } + catch { case ERROR(_) => error("Failed to build documentation") } + + make_news(other_isabelle, 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("### Creating distribution archive " + release.isabelle_archive) + + release.execute_dist_name(release.dist_dir, """ +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, "--owner=root --group=root -czf " + + File.bash_path(release.isabelle_archive) + " " + Bash.string(release.dist_name)) + + release.execute_dist_name(release.dist_dir, """ +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" +""") + + File.write(isabelle_dist_file, release.isabelle_archive.implode) + File.write(isabelle_ident_file, ident) + ident + } + + release.copy(ident = release_ident) } /* make application bundles */ + val bundle_infos = platform_families.map(release.bundle_info(_)) + for (bundle_info <- bundle_infos) { val bundle = (if (remote_mac.isEmpty) bundle_info.fallback else None) getOrElse bundle_info.main @@ -108,7 +324,7 @@ progress.echo( "\nApplication bundle for " + bundle_info.platform_family + ": " + bundle_archive.implode) progress.bash( - "isabelle makedist_bundle " + File.bash_path(release.dist_archive) + + "isabelle makedist_bundle " + File.bash_path(release.isabelle_archive) + " " + Bash.string(bundle_info.platform_family) + (if (remote_mac == "") "" else " " + Bash.string(remote_mac)), echo = true).check @@ -122,17 +338,16 @@ val website_platform_bundles = for { bundle_info <- bundle_infos - bundle <- - bundle_info.names.find(name => (release.dist_dir + Path.explode(name)).is_file) + bundle <- bundle_info.names.find(name => (release.dist_dir + Path.explode(name)).is_file) } yield (bundle, bundle_info) val afp_link = HTML.link(AFP.repos_source + "/commits/" + afp_rev, HTML.text("AFP/" + afp_rev)) HTML.write_document(dir, "index.html", - List(HTML.title(release.name)), + List(HTML.title(release.dist_name)), List( - HTML.chapter(release.name + " (" + release_id + ")"), + HTML.chapter(release.dist_name + " (" + release.ident + ")"), HTML.itemize( website_platform_bundles.map({ case (bundle, bundle_info) => List(HTML.link(bundle, HTML.text(bundle_info.platform_description))) }))) ::: @@ -146,45 +361,40 @@ /* HTML library */ if (build_library) { - if (release.dist_library_archive.is_file) - progress.echo("### Library archive already exists: " + - release.dist_library_archive.implode) + if (release.isabelle_library_archive.is_file) { + progress.echo( + "### Library archive already exists: " + release.isabelle_library_archive.implode) + } else { Isabelle_System.with_tmp_dir("build_release")(tmp_dir => { - def execute(script: String): Unit = - Isabelle_System.bash(script, cwd = tmp_dir.file).check - def execute_tar(args: String): Unit = - Isabelle_System.gnutar(args, cwd = tmp_dir.file).check - - val name = release.name + val name = release.dist_name val platform = Isabelle_System.getenv_strict("ISABELLE_PLATFORM_FAMILY") val bundle = release.dist_dir + Path.explode(name + "_" + platform + ".tar.gz") - execute_tar("xzf " + File.bash_path(bundle)) + execute_tar(tmp_dir, "-xzf " + File.bash_path(bundle)) val other_isabelle = Other_Isabelle(tmp_dir + Path.explode(name), - isabelle_identifier = name + "-build", progress = progress) + isabelle_identifier = release.other_isabelle_identifier, progress = progress) Isabelle_System.mkdirs(other_isabelle.etc) File.write(other_isabelle.etc_preferences, "ML_system_64 = true\n") - other_isabelle.bash("bin/isabelle build" + jobs_option + + other_isabelle.bash("bin/isabelle build -j " + parallel_jobs + " -o browser_info -o document=pdf -o document_variants=document:outline=/proof,/ML" + " -s -c -a -d '~~/src/Benchmarks'", echo = true).check other_isabelle.isabelle_home_user.file.delete - execute("chmod -R a+r " + Bash.string(name)) - execute("chmod -R g=o " + Bash.string(name)) - execute_tar("--owner=root --group=root -czf " + - File.bash_path(release.dist_library_archive) + + execute(tmp_dir, "chmod -R a+r " + Bash.string(name)) + execute(tmp_dir, "chmod -R g=o " + Bash.string(name)) + execute_tar(tmp_dir, "--owner=root --group=root -czf " + + File.bash_path(release.isabelle_library_archive) + " " + Bash.string(name + "/browser_info")) }) } } - - release.copy(id = release_id) + release } @@ -197,7 +407,7 @@ var afp_rev = "" var remote_mac = "" var official_release = false - var release_name = "" + var proper_release_name: Option[String] = None var website: Option[Path] = None var parallel_jobs = 1 var build_library = false @@ -223,7 +433,7 @@ "A:" -> (arg => afp_rev = arg), "M:" -> (arg => remote_mac = arg), "O" -> (_ => official_release = true), - "R:" -> (arg => release_name = arg), + "R:" -> (arg => proper_release_name = Some(arg)), "W:" -> (arg => website = Some(Path.explode(arg))), "j:" -> (arg => parallel_jobs = Value.Int.parse(arg)), "l" -> (_ => build_library = true), @@ -236,9 +446,11 @@ val progress = new Console_Progress() build_release(Path.explode(base_dir), progress = progress, rev = rev, afp_rev = afp_rev, - official_release = official_release, release_name = release_name, website = website, + official_release = official_release, proper_release_name = proper_release_name, + website = website, platform_families = - if (platform_families.isEmpty) default_platform_families else platform_families, + if (platform_families.isEmpty) default_platform_families + else platform_families, build_library = build_library, parallel_jobs = parallel_jobs, remote_mac = remote_mac) } } diff -r 9456ba573729 -r 68816d1c73a7 src/Pure/Admin/news.scala --- a/src/Pure/Admin/news.scala Sun Oct 21 14:35:46 2018 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,36 +0,0 @@ -/* Title: Pure/Admin/news.scala - Author: Makarius - -Support for the NEWS file. -*/ - -package isabelle - - -object NEWS -{ - /* generate HTML version */ - - def generate_html() - { - val target = Path.explode("~~/doc") - val target_fonts = target + Path.explode("fonts") - Isabelle_System.mkdirs(target_fonts) - - for (font <- Isabelle_System.fonts(html = true)) - File.copy(font, target_fonts) - - HTML.write_document(target, "NEWS.html", - List(HTML.title("NEWS (" + Distribution.version + ")")), - List( - HTML.chapter("NEWS"), - HTML.source(Symbol.decode(File.read(Path.explode("~~/NEWS")))))) - } - - - /* Isabelle tool wrapper */ - - val isabelle_tool = - Isabelle_Tool("news", "generate HTML version of the NEWS file", - _ => generate_html(), admin = true) -} diff -r 9456ba573729 -r 68816d1c73a7 src/Pure/Admin/other_isabelle.scala --- a/src/Pure/Admin/other_isabelle.scala Sun Oct 21 14:35:46 2018 +0200 +++ b/src/Pure/Admin/other_isabelle.scala Sun Oct 21 18:32:33 2018 +0200 @@ -61,12 +61,22 @@ val etc_settings: Path = etc + Path.explode("settings") val etc_preferences: Path = etc + Path.explode("preferences") + def fonts(html: Boolean = false): List[Path] = + Isabelle_System.fonts(html = html, get = getenv(_)) - /* init settings */ + + /* settings */ + + def clean_settings(): Boolean = + if (!etc_settings.is_file) true + else if (File.read(etc_settings).startsWith("# generated by Isabelle")) { + etc_settings.file.delete; true + } + else false def init_settings(components_base: String, nonfree: Boolean, more_settings: List[String]) { - if (etc_settings.is_file && !File.read(etc_settings).startsWith("# generated by Isabelle")) + if (!clean_settings()) error("Cannot proceed with existing user settings file: " + etc_settings) Isabelle_System.mkdirs(etc_settings.dir) @@ -94,4 +104,14 @@ File.append(etc_settings, "\n" + cat_lines(settings.map(terminate_lines(_)))) } + + + /* cleanup */ + + def cleanup() + { + clean_settings() + etc.file.delete + isabelle_home_user.file.delete + } } diff -r 9456ba573729 -r 68816d1c73a7 src/Pure/System/isabelle_system.scala --- a/src/Pure/System/isabelle_system.scala Sun Oct 21 14:35:46 2018 +0200 +++ b/src/Pure/System/isabelle_system.scala Sun Oct 21 18:32:33 2018 +0200 @@ -349,13 +349,13 @@ /* fonts */ - def fonts(html: Boolean = false): List[Path] = + def fonts(html: Boolean = false, get: String => String = getenv_strict(_)): List[Path] = { val variables = if (html) List("ISABELLE_FONTS", "ISABELLE_FONTS_HTML") else List("ISABELLE_FONTS") for { variable <- variables - path <- Path.split(Isabelle_System.getenv_strict(variable)) + path <- Path.split(get(variable)) } yield path } diff -r 9456ba573729 -r 68816d1c73a7 src/Pure/System/isabelle_tool.scala --- a/src/Pure/System/isabelle_tool.scala Sun Oct 21 14:35:46 2018 +0200 +++ b/src/Pure/System/isabelle_tool.scala Sun Oct 21 18:32:33 2018 +0200 @@ -114,7 +114,6 @@ Imports.isabelle_tool, Mkroot.isabelle_tool, ML_Process.isabelle_tool, - NEWS.isabelle_tool, Options.isabelle_tool, Present.isabelle_tool, Profiling_Report.isabelle_tool, diff -r 9456ba573729 -r 68816d1c73a7 src/Pure/build-jars --- a/src/Pure/build-jars Sun Oct 21 14:35:46 2018 +0200 +++ b/src/Pure/build-jars Sun Oct 21 18:32:33 2018 +0200 @@ -23,7 +23,6 @@ Admin/isabelle_cronjob.scala Admin/isabelle_devel.scala Admin/jenkins.scala - Admin/news.scala Admin/other_isabelle.scala Admin/remote_dmg.scala Concurrent/consumer_thread.scala