author | wenzelm |
Thu, 08 Jun 2017 13:01:50 +0200 | |
changeset 66038 | 36bf57d6c011 |
parent 66000 | 58aa6749ff36 |
child 66040 | f826ba18fe08 |
permissions | -rw-r--r-- |
50707
5b2bf7611662
maintain session index on Scala side, for more determistic results;
wenzelm
parents:
diff
changeset
|
1 |
/* Title: Pure/Thy/present.scala |
5b2bf7611662
maintain session index on Scala side, for more determistic results;
wenzelm
parents:
diff
changeset
|
2 |
Author: Makarius |
5b2bf7611662
maintain session index on Scala side, for more determistic results;
wenzelm
parents:
diff
changeset
|
3 |
|
5b2bf7611662
maintain session index on Scala side, for more determistic results;
wenzelm
parents:
diff
changeset
|
4 |
Theory presentation: HTML. |
5b2bf7611662
maintain session index on Scala side, for more determistic results;
wenzelm
parents:
diff
changeset
|
5 |
*/ |
5b2bf7611662
maintain session index on Scala side, for more determistic results;
wenzelm
parents:
diff
changeset
|
6 |
|
5b2bf7611662
maintain session index on Scala side, for more determistic results;
wenzelm
parents:
diff
changeset
|
7 |
package isabelle |
5b2bf7611662
maintain session index on Scala side, for more determistic results;
wenzelm
parents:
diff
changeset
|
8 |
|
5b2bf7611662
maintain session index on Scala side, for more determistic results;
wenzelm
parents:
diff
changeset
|
9 |
|
61372 | 10 |
import java.io.{File => JFile} |
11 |
||
51402 | 12 |
import scala.collection.immutable.SortedMap |
13 |
||
14 |
||
50707
5b2bf7611662
maintain session index on Scala side, for more determistic results;
wenzelm
parents:
diff
changeset
|
15 |
object Present |
5b2bf7611662
maintain session index on Scala side, for more determistic results;
wenzelm
parents:
diff
changeset
|
16 |
{ |
51399
6ac3c29a300e
discontinued "isabelle usedir" option -r (reset session path);
wenzelm
parents:
50707
diff
changeset
|
17 |
/* maintain chapter index -- NOT thread-safe */ |
50707
5b2bf7611662
maintain session index on Scala side, for more determistic results;
wenzelm
parents:
diff
changeset
|
18 |
|
51399
6ac3c29a300e
discontinued "isabelle usedir" option -r (reset session path);
wenzelm
parents:
50707
diff
changeset
|
19 |
private val sessions_path = Path.basic(".sessions") |
50707
5b2bf7611662
maintain session index on Scala side, for more determistic results;
wenzelm
parents:
diff
changeset
|
20 |
|
51402 | 21 |
private def read_sessions(dir: Path): List[(String, String)] = |
22 |
{ |
|
51416 | 23 |
val path = dir + sessions_path |
24 |
if (path.is_file) { |
|
25 |
import XML.Decode._ |
|
65344
b99283eed13c
clarified YXML vs. symbol encoding: operate on whole message;
wenzelm
parents:
65089
diff
changeset
|
26 |
list(pair(string, string))(Symbol.decode_yxml(File.read(path))) |
51416 | 27 |
} |
28 |
else Nil |
|
51402 | 29 |
} |
50707
5b2bf7611662
maintain session index on Scala side, for more determistic results;
wenzelm
parents:
diff
changeset
|
30 |
|
51402 | 31 |
private def write_sessions(dir: Path, sessions: List[(String, String)]) |
32 |
{ |
|
33 |
import XML.Encode._ |
|
34 |
File.write(dir + sessions_path, YXML.string_of_body(list(pair(string, string))(sessions))) |
|
35 |
} |
|
50707
5b2bf7611662
maintain session index on Scala side, for more determistic results;
wenzelm
parents:
diff
changeset
|
36 |
|
61372 | 37 |
def update_chapter_index(browser_info: Path, chapter: String, new_sessions: List[(String, String)]) |
51399
6ac3c29a300e
discontinued "isabelle usedir" option -r (reset session path);
wenzelm
parents:
50707
diff
changeset
|
38 |
{ |
61372 | 39 |
val dir = browser_info + Path.basic(chapter) |
51399
6ac3c29a300e
discontinued "isabelle usedir" option -r (reset session path);
wenzelm
parents:
50707
diff
changeset
|
40 |
Isabelle_System.mkdirs(dir) |
50707
5b2bf7611662
maintain session index on Scala side, for more determistic results;
wenzelm
parents:
diff
changeset
|
41 |
|
51399
6ac3c29a300e
discontinued "isabelle usedir" option -r (reset session path);
wenzelm
parents:
50707
diff
changeset
|
42 |
val sessions0 = |
51406
950b897f95bb
proper path -- I/O was hidden due to permissiveness;
wenzelm
parents:
51402
diff
changeset
|
43 |
try { read_sessions(dir) } |
51987 | 44 |
catch { case _: XML.Error => Nil } |
51399
6ac3c29a300e
discontinued "isabelle usedir" option -r (reset session path);
wenzelm
parents:
50707
diff
changeset
|
45 |
|
51402 | 46 |
val sessions = (SortedMap.empty[String, String] ++ sessions0 ++ new_sessions).toList |
65988 | 47 |
write_sessions(dir, sessions) |
51402 | 48 |
|
65988 | 49 |
val title = "Isabelle/" + chapter + " sessions" |
50 |
HTML.write_document(dir, "index.html", |
|
51 |
List(HTML.title(title + " (" + Distribution.version + ")")), |
|
52 |
HTML.chapter(title) :: |
|
53 |
(if (sessions.isEmpty) Nil |
|
54 |
else |
|
65992 | 55 |
List(HTML.div("sessions", |
56 |
List(HTML.description( |
|
65988 | 57 |
sessions.map({ case (name, description) => |
65989 | 58 |
(List(HTML.link(name + "/index.html", HTML.text(name))), |
59 |
if (description == "") Nil |
|
66038 | 60 |
else HTML.break ::: List(HTML.pre(HTML.text(description)))) }))))))) |
51399
6ac3c29a300e
discontinued "isabelle usedir" option -r (reset session path);
wenzelm
parents:
50707
diff
changeset
|
61 |
} |
61372 | 62 |
|
63 |
def make_global_index(browser_info: Path) |
|
64 |
{ |
|
65 |
if (!(browser_info + Path.explode("index.html")).is_file) { |
|
66 |
Isabelle_System.mkdirs(browser_info) |
|
67 |
File.copy(Path.explode("~~/lib/logo/isabelle.gif"), |
|
68 |
browser_info + Path.explode("isabelle.gif")) |
|
69 |
File.write(browser_info + Path.explode("index.html"), |
|
70 |
File.read(Path.explode("~~/lib/html/library_index_header.template")) + |
|
71 |
File.read(Path.explode("~~/lib/html/library_index_content.template")) + |
|
72 |
File.read(Path.explode("~~/lib/html/library_index_footer.template"))) |
|
73 |
} |
|
74 |
} |
|
75 |
||
76 |
||
77 |
/* finish session */ |
|
78 |
||
79 |
def finish( |
|
80 |
progress: Progress, |
|
81 |
browser_info: Path, |
|
82 |
graph_file: JFile, |
|
62631 | 83 |
info: Sessions.Info, |
61372 | 84 |
name: String) |
85 |
{ |
|
86 |
val session_prefix = browser_info + Path.basic(info.chapter) + Path.basic(name) |
|
65089 | 87 |
val session_fonts = session_prefix + Path.explode("fonts") |
61372 | 88 |
|
89 |
if (info.options.bool("browser_info")) { |
|
65089 | 90 |
Isabelle_System.mkdirs(session_fonts) |
62971
087e36ce0593
back to exact copy of non-text file (amending dcc8e1d34b18);
wenzelm
parents:
62631
diff
changeset
|
91 |
|
087e36ce0593
back to exact copy of non-text file (amending dcc8e1d34b18);
wenzelm
parents:
62631
diff
changeset
|
92 |
val session_graph = session_prefix + Path.basic("session_graph.pdf") |
087e36ce0593
back to exact copy of non-text file (amending dcc8e1d34b18);
wenzelm
parents:
62631
diff
changeset
|
93 |
File.copy(graph_file, session_graph.file) |
087e36ce0593
back to exact copy of non-text file (amending dcc8e1d34b18);
wenzelm
parents:
62631
diff
changeset
|
94 |
Isabelle_System.bash("chmod a+r " + File.bash_path(session_graph)) |
087e36ce0593
back to exact copy of non-text file (amending dcc8e1d34b18);
wenzelm
parents:
62631
diff
changeset
|
95 |
|
66000 | 96 |
HTML.write_isabelle_css(session_prefix) |
61500 | 97 |
|
65083 | 98 |
for (font <- Isabelle_System.fonts(html = true)) |
65089 | 99 |
File.copy(font, session_fonts) |
61372 | 100 |
} |
101 |
} |
|
50707
5b2bf7611662
maintain session index on Scala side, for more determistic results;
wenzelm
parents:
diff
changeset
|
102 |
} |