# HG changeset patch
# User wenzelm
# Date 1452374537 -3600
# Node ID a7cf464933f778844dd50fe7df96b1ae50cdf733
# Parent  16de2a9b5b3d7acc809bc31880f7c34373a161f3
generate HTML version of NEWS, with proper symbol rendering;

diff -r 16de2a9b5b3d -r a7cf464933f7 Admin/lib/Tools/makedist
--- a/Admin/lib/Tools/makedist	Sat Jan 09 22:00:22 2016 +0100
+++ b/Admin/lib/Tools/makedist	Sat Jan 09 22:22:17 2016 +0100
@@ -196,6 +196,8 @@
 
 rm -rf Admin browser_info heaps
 
+./bin/isabelle java isabelle.NEWS
+
 
 # create archive
 
diff -r 16de2a9b5b3d -r a7cf464933f7 NEWS
--- a/NEWS	Sat Jan 09 22:00:22 2016 +0100
+++ b/NEWS	Sat Jan 09 22:22:17 2016 +0100
@@ -1,7 +1,7 @@
 Isabelle NEWS -- history of user-relevant changes
 =================================================
 
-(Note: Isabelle/jEdit shows a tree-view of this file in Sidekick.)
+(Note: Isabelle/jEdit shows a tree-view of the NEWS file in Sidekick.)
 
 
 New in Isabelle2016 (February 2016)
diff -r 16de2a9b5b3d -r a7cf464933f7 src/Pure/Tools/news.scala
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/Tools/news.scala	Sat Jan 09 22:22:17 2016 +0100
@@ -0,0 +1,38 @@
+/*  Title:      Pure/Tools/news.scala
+    Author:     Makarius
+
+Support for the NEWS file.
+*/
+
+package isabelle
+
+
+object NEWS
+{
+  /* generate HTML version */
+
+  def generate_html()
+  {
+    val target = Path.explode("~~/doc")
+
+    File.write(target + Path.explode("NEWS.html"),
+      HTML.begin_document("NEWS") +
+      "\n<div class=\"source\">\n<pre class=\"source\">" +
+      HTML.output(Symbol.decode(File.read(Path.explode("~~/NEWS")))) +
+      "</pre>\n" +
+      HTML.end_document)
+
+    for (font <- Path.split(Isabelle_System.getenv_strict("ISABELLE_FONTS")))
+      File.copy(font, target)
+
+    File.copy(Path.explode("~~/etc/isabelle.css"), target)
+  }
+
+
+  /* command line entry point */
+
+  def main(args: Array[String])
+  {
+    Command_Line.tool0 { generate_html() }
+  }
+}
diff -r 16de2a9b5b3d -r a7cf464933f7 src/Pure/build-jars
--- a/src/Pure/build-jars	Sat Jan 09 22:00:22 2016 +0100
+++ b/src/Pure/build-jars	Sat Jan 09 22:22:17 2016 +0100
@@ -100,6 +100,7 @@
   Tools/doc.scala
   Tools/main.scala
   Tools/ml_statistics.scala
+  Tools/news.scala
   Tools/print_operation.scala
   Tools/simplifier_trace.scala
   Tools/task_statistics.scala