| author | wenzelm |
| Fri, 07 Oct 2016 11:10:17 +0200 | |
| changeset 64079 | ff26032b7f2a |
| parent 62114 | a7cf464933f7 |
| permissions | -rw-r--r-- |
|
62114
a7cf464933f7
generate HTML version of NEWS, with proper symbol rendering;
wenzelm
parents:
diff
changeset
|
1 |
/* Title: Pure/Tools/news.scala |
|
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 |
|
|
a7cf464933f7
generate HTML version of NEWS, with proper symbol rendering;
wenzelm
parents:
diff
changeset
|
32 |
/* command line entry point */ |
|
a7cf464933f7
generate HTML version of NEWS, with proper symbol rendering;
wenzelm
parents:
diff
changeset
|
33 |
|
|
a7cf464933f7
generate HTML version of NEWS, with proper symbol rendering;
wenzelm
parents:
diff
changeset
|
34 |
def main(args: Array[String]) |
|
a7cf464933f7
generate HTML version of NEWS, with proper symbol rendering;
wenzelm
parents:
diff
changeset
|
35 |
{
|
|
a7cf464933f7
generate HTML version of NEWS, with proper symbol rendering;
wenzelm
parents:
diff
changeset
|
36 |
Command_Line.tool0 { generate_html() }
|
|
a7cf464933f7
generate HTML version of NEWS, with proper symbol rendering;
wenzelm
parents:
diff
changeset
|
37 |
} |
|
a7cf464933f7
generate HTML version of NEWS, with proper symbol rendering;
wenzelm
parents:
diff
changeset
|
38 |
} |