| author | wenzelm |
| Sat, 03 Mar 2018 13:23:09 +0100 | |
| changeset 67753 | f28aee3ad1e6 |
| parent 65988 | 8040d2563593 |
| permissions | -rw-r--r-- |
| 64369 | 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 | 17 |
val target_fonts = target + Path.explode("fonts")
|
18 |
Isabelle_System.mkdirs(target_fonts) |
|
|
62114
a7cf464933f7
generate HTML version of NEWS, with proper symbol rendering;
wenzelm
parents:
diff
changeset
|
19 |
|
| 65089 | 20 |
for (font <- Isabelle_System.fonts(html = true)) |
21 |
File.copy(font, target_fonts) |
|
|
62114
a7cf464933f7
generate HTML version of NEWS, with proper symbol rendering;
wenzelm
parents:
diff
changeset
|
22 |
|
| 65988 | 23 |
HTML.write_document(target, "NEWS.html", |
24 |
List(HTML.title("NEWS (" + Distribution.version + ")")),
|
|
25 |
List( |
|
26 |
HTML.chapter("NEWS"),
|
|
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 | 31 |
/* Isabelle tool wrapper */ |
|
62114
a7cf464933f7
generate HTML version of NEWS, with proper symbol rendering;
wenzelm
parents:
diff
changeset
|
32 |
|
| 64369 | 33 |
val isabelle_tool = |
| 64372 | 34 |
Isabelle_Tool("news", "generate HTML version of the NEWS file",
|
35 |
_ => generate_html(), admin = true) |
|
|
62114
a7cf464933f7
generate HTML version of NEWS, with proper symbol rendering;
wenzelm
parents:
diff
changeset
|
36 |
} |