src/Pure/Admin/news.scala
author wenzelm
Mon, 09 Oct 2017 17:09:08 +0200
changeset 66820 fc516da7ee4f
parent 65988 8040d2563593
permissions -rw-r--r--
some administrative support for AFP;
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")
65089
1d219d76873b clarified fonts;
wenzelm
parents: 65083
diff changeset
    17
    val target_fonts = target + Path.explode("fonts")
1d219d76873b clarified fonts;
wenzelm
parents: 65083
diff changeset
    18
    Isabelle_System.mkdirs(target_fonts)
62114
a7cf464933f7 generate HTML version of NEWS, with proper symbol rendering;
wenzelm
parents:
diff changeset
    19
65089
1d219d76873b clarified fonts;
wenzelm
parents: 65083
diff changeset
    20
    for (font <- Isabelle_System.fonts(html = true))
1d219d76873b clarified fonts;
wenzelm
parents: 65083
diff changeset
    21
      File.copy(font, target_fonts)
62114
a7cf464933f7 generate HTML version of NEWS, with proper symbol rendering;
wenzelm
parents:
diff changeset
    22
65988
8040d2563593 modernized generated HTML;
wenzelm
parents: 65089
diff changeset
    23
    HTML.write_document(target, "NEWS.html",
8040d2563593 modernized generated HTML;
wenzelm
parents: 65089
diff changeset
    24
      List(HTML.title("NEWS (" + Distribution.version + ")")),
8040d2563593 modernized generated HTML;
wenzelm
parents: 65089
diff changeset
    25
      List(
8040d2563593 modernized generated HTML;
wenzelm
parents: 65089
diff changeset
    26
        HTML.chapter("NEWS"),
8040d2563593 modernized generated HTML;
wenzelm
parents: 65089
diff changeset
    27
        HTML.source(Symbol.decode(File.read(Path.explode("~~/NEWS"))))))
62114
a7cf464933f7 generate HTML version of NEWS, with proper symbol rendering;
wenzelm
parents:
diff changeset
    28
  }
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
64369
6a9816764b37 proper Admin tool;
wenzelm
parents: 62114
diff changeset
    31
  /* Isabelle tool wrapper */
62114
a7cf464933f7 generate HTML version of NEWS, with proper symbol rendering;
wenzelm
parents:
diff changeset
    32
64369
6a9816764b37 proper Admin tool;
wenzelm
parents: 62114
diff changeset
    33
  val isabelle_tool =
64372
wenzelm
parents: 64369
diff changeset
    34
    Isabelle_Tool("news", "generate HTML version of the NEWS file",
wenzelm
parents: 64369
diff changeset
    35
      _ => generate_html(), admin = true)
62114
a7cf464933f7 generate HTML version of NEWS, with proper symbol rendering;
wenzelm
parents:
diff changeset
    36
}