# HG changeset patch # User wenzelm # Date 1674420778 -3600 # Node ID 96879e303ea33af52fa2bec5c5e71e9a9698379a # Parent 2f09dc0e6dda6bfef9fe0bdd569b5d5c89a00ec0 clarified modules (again, in contrast to f8f065e20837); diff -r 2f09dc0e6dda -r 96879e303ea3 src/Pure/Admin/build_release.scala --- a/src/Pure/Admin/build_release.scala Sun Jan 22 21:22:51 2023 +0100 +++ b/src/Pure/Admin/build_release.scala Sun Jan 22 21:52:58 2023 +0100 @@ -388,6 +388,24 @@ } + /* NEWS */ + + private def make_news(other_isabelle: Other_Isabelle): Unit = { + val news_file = other_isabelle.isabelle_home + Path.explode("NEWS") + val doc_dir = other_isabelle.isabelle_home + Path.explode("doc") + val fonts_dir = Isabelle_System.make_directory(doc_dir + Path.explode("fonts")) + + Isabelle_Fonts.make_entries(getenv = other_isabelle.getenv, hidden = true). + foreach(entry => Isabelle_System.copy_file(entry.path, fonts_dir)) + + HTML.write_document(doc_dir, "NEWS.html", + List(HTML.title("NEWS")), + List( + HTML.chapter("NEWS"), + HTML.source(Symbol.decode(File.read(news_file))))) + } + + /* main */ def use_release_archive( @@ -466,7 +484,7 @@ } catch { case ERROR(msg) => cat_error("Failed to build documentation:", msg) } - other_isabelle.make_news() + make_news(other_isabelle) for (name <- List("Admin", "browser_info", "heaps")) { Isabelle_System.rm_tree(other_isabelle.isabelle_home + Path.explode(name)) diff -r 2f09dc0e6dda -r 96879e303ea3 src/Pure/Admin/other_isabelle.scala --- a/src/Pure/Admin/other_isabelle.scala Sun Jan 22 21:22:51 2023 +0100 +++ b/src/Pure/Admin/other_isabelle.scala Sun Jan 22 21:52:58 2023 +0100 @@ -63,23 +63,6 @@ val etc_preferences: Path = etc + Path.explode("preferences") - /* NEWS */ - - def make_news(): Unit = { - val doc_dir = isabelle_home + Path.explode("doc") - val fonts_dir = Isabelle_System.make_directory(doc_dir + Path.explode("fonts")) - - Isabelle_Fonts.make_entries(getenv = getenv, hidden = true). - foreach(entry => Isabelle_System.copy_file(entry.path, fonts_dir)) - - HTML.write_document(doc_dir, "NEWS.html", - List(HTML.title("NEWS")), - List( - HTML.chapter("NEWS"), - HTML.source(Symbol.decode(File.read(isabelle_home + Path.explode("NEWS")))))) - } - - /* components */ def init_components(