src/Pure/Admin/news.scala
author wenzelm
Mon, 24 Oct 2016 12:01:36 +0200
changeset 64369 6a9816764b37
parent 62114 src/Pure/Tools/news.scala@a7cf464933f7
child 64372 7ffd2be0a1e8
permissions -rw-r--r--
proper Admin tool;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
64369
6a9816764b37 proper Admin tool;
wenzelm
parents: 62114
diff changeset
     1
/*  Title:      Pure/Admin/news.scala
62114
a7cf464933f7 generate HTML version of NEWS, with proper symbol rendering;
wenzelm
parents:
diff changeset
     2
    Author:     Makarius
a7cf464933f7 generate HTML version of NEWS, with proper symbol rendering;
wenzelm
parents:
diff changeset
     3
a7cf464933f7 generate HTML version of NEWS, with proper symbol rendering;
wenzelm
parents:
diff changeset
     4
Support for the NEWS file.
a7cf464933f7 generate HTML version of NEWS, with proper symbol rendering;
wenzelm
parents:
diff changeset
     5
*/
a7cf464933f7 generate HTML version of NEWS, with proper symbol rendering;
wenzelm
parents:
diff changeset
     6
a7cf464933f7 generate HTML version of NEWS, with proper symbol rendering;
wenzelm
parents:
diff changeset
     7
package isabelle
a7cf464933f7 generate HTML version of NEWS, with proper symbol rendering;
wenzelm
parents:
diff changeset
     8
a7cf464933f7 generate HTML version of NEWS, with proper symbol rendering;
wenzelm
parents:
diff changeset
     9
a7cf464933f7 generate HTML version of NEWS, with proper symbol rendering;
wenzelm
parents:
diff changeset
    10
object NEWS
a7cf464933f7 generate HTML version of NEWS, with proper symbol rendering;
wenzelm
parents:
diff changeset
    11
{
a7cf464933f7 generate HTML version of NEWS, with proper symbol rendering;
wenzelm
parents:
diff changeset
    12
  /* generate HTML version */
a7cf464933f7 generate HTML version of NEWS, with proper symbol rendering;
wenzelm
parents:
diff changeset
    13
a7cf464933f7 generate HTML version of NEWS, with proper symbol rendering;
wenzelm
parents:
diff changeset
    14
  def generate_html()
a7cf464933f7 generate HTML version of NEWS, with proper symbol rendering;
wenzelm
parents:
diff changeset
    15
  {
a7cf464933f7 generate HTML version of NEWS, with proper symbol rendering;
wenzelm
parents:
diff changeset
    16
    val target = Path.explode("~~/doc")
a7cf464933f7 generate HTML version of NEWS, with proper symbol rendering;
wenzelm
parents:
diff changeset
    17
a7cf464933f7 generate HTML version of NEWS, with proper symbol rendering;
wenzelm
parents:
diff changeset
    18
    File.write(target + Path.explode("NEWS.html"),
a7cf464933f7 generate HTML version of NEWS, with proper symbol rendering;
wenzelm
parents:
diff changeset
    19
      HTML.begin_document("NEWS") +
a7cf464933f7 generate HTML version of NEWS, with proper symbol rendering;
wenzelm
parents:
diff changeset
    20
      "\n<div class=\"source\">\n<pre class=\"source\">" +
a7cf464933f7 generate HTML version of NEWS, with proper symbol rendering;
wenzelm
parents:
diff changeset
    21
      HTML.output(Symbol.decode(File.read(Path.explode("~~/NEWS")))) +
a7cf464933f7 generate HTML version of NEWS, with proper symbol rendering;
wenzelm
parents:
diff changeset
    22
      "</pre>\n" +
a7cf464933f7 generate HTML version of NEWS, with proper symbol rendering;
wenzelm
parents:
diff changeset
    23
      HTML.end_document)
a7cf464933f7 generate HTML version of NEWS, with proper symbol rendering;
wenzelm
parents:
diff changeset
    24
a7cf464933f7 generate HTML version of NEWS, with proper symbol rendering;
wenzelm
parents:
diff changeset
    25
    for (font <- Path.split(Isabelle_System.getenv_strict("ISABELLE_FONTS")))
a7cf464933f7 generate HTML version of NEWS, with proper symbol rendering;
wenzelm
parents:
diff changeset
    26
      File.copy(font, target)
a7cf464933f7 generate HTML version of NEWS, with proper symbol rendering;
wenzelm
parents:
diff changeset
    27
a7cf464933f7 generate HTML version of NEWS, with proper symbol rendering;
wenzelm
parents:
diff changeset
    28
    File.copy(Path.explode("~~/etc/isabelle.css"), target)
a7cf464933f7 generate HTML version of NEWS, with proper symbol rendering;
wenzelm
parents:
diff changeset
    29
  }
a7cf464933f7 generate HTML version of NEWS, with proper symbol rendering;
wenzelm
parents:
diff changeset
    30
a7cf464933f7 generate HTML version of NEWS, with proper symbol rendering;
wenzelm
parents:
diff changeset
    31
64369
6a9816764b37 proper Admin tool;
wenzelm
parents: 62114
diff changeset
    32
  /* Isabelle tool wrapper */
62114
a7cf464933f7 generate HTML version of NEWS, with proper symbol rendering;
wenzelm
parents:
diff changeset
    33
64369
6a9816764b37 proper Admin tool;
wenzelm
parents: 62114
diff changeset
    34
  val isabelle_tool =
6a9816764b37 proper Admin tool;
wenzelm
parents: 62114
diff changeset
    35
    Isabelle_Tool("news", "generate HTML version of the NEWS file", args =>
6a9816764b37 proper Admin tool;
wenzelm
parents: 62114
diff changeset
    36
    {
6a9816764b37 proper Admin tool;
wenzelm
parents: 62114
diff changeset
    37
      Command_Line.tool0 { generate_html() }
6a9816764b37 proper Admin tool;
wenzelm
parents: 62114
diff changeset
    38
    }, admin = true)
62114
a7cf464933f7 generate HTML version of NEWS, with proper symbol rendering;
wenzelm
parents:
diff changeset
    39
}