| author | wenzelm | 
| Sat, 09 Jan 2016 22:22:17 +0100 | |
| changeset 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  | 
}  |