author | wenzelm |
Thu, 06 Apr 2017 14:32:56 +0200 | |
changeset 65404 | 2b819faf45e9 |
parent 65391 | b5740579cad6 |
child 65988 | 8040d2563593 |
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 |
|
5b2bf7611662
maintain session index on Scala side, for more determistic results;
wenzelm
parents:
diff
changeset
|
19 |
private val index_path = Path.basic("index.html") |
51399
6ac3c29a300e
discontinued "isabelle usedir" option -r (reset session path);
wenzelm
parents:
50707
diff
changeset
|
20 |
private val sessions_path = Path.basic(".sessions") |
50707
5b2bf7611662
maintain session index on Scala side, for more determistic results;
wenzelm
parents:
diff
changeset
|
21 |
|
51402 | 22 |
private def read_sessions(dir: Path): List[(String, String)] = |
23 |
{ |
|
51416 | 24 |
val path = dir + sessions_path |
25 |
if (path.is_file) { |
|
26 |
import XML.Decode._ |
|
65344
b99283eed13c
clarified YXML vs. symbol encoding: operate on whole message;
wenzelm
parents:
65089
diff
changeset
|
27 |
list(pair(string, string))(Symbol.decode_yxml(File.read(path))) |
51416 | 28 |
} |
29 |
else Nil |
|
51402 | 30 |
} |
50707
5b2bf7611662
maintain session index on Scala side, for more determistic results;
wenzelm
parents:
diff
changeset
|
31 |
|
51402 | 32 |
private def write_sessions(dir: Path, sessions: List[(String, String)]) |
33 |
{ |
|
34 |
import XML.Encode._ |
|
35 |
File.write(dir + sessions_path, YXML.string_of_body(list(pair(string, string))(sessions))) |
|
36 |
} |
|
50707
5b2bf7611662
maintain session index on Scala side, for more determistic results;
wenzelm
parents:
diff
changeset
|
37 |
|
61372 | 38 |
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
|
39 |
{ |
61372 | 40 |
val dir = browser_info + Path.basic(chapter) |
51399
6ac3c29a300e
discontinued "isabelle usedir" option -r (reset session path);
wenzelm
parents:
50707
diff
changeset
|
41 |
Isabelle_System.mkdirs(dir) |
50707
5b2bf7611662
maintain session index on Scala side, for more determistic results;
wenzelm
parents:
diff
changeset
|
42 |
|
51399
6ac3c29a300e
discontinued "isabelle usedir" option -r (reset session path);
wenzelm
parents:
50707
diff
changeset
|
43 |
val sessions0 = |
51406
950b897f95bb
proper path -- I/O was hidden due to permissiveness;
wenzelm
parents:
51402
diff
changeset
|
44 |
try { read_sessions(dir) } |
51987 | 45 |
catch { case _: XML.Error => Nil } |
51399
6ac3c29a300e
discontinued "isabelle usedir" option -r (reset session path);
wenzelm
parents:
50707
diff
changeset
|
46 |
|
51402 | 47 |
val sessions = (SortedMap.empty[String, String] ++ sessions0 ++ new_sessions).toList |
48 |
||
51399
6ac3c29a300e
discontinued "isabelle usedir" option -r (reset session path);
wenzelm
parents:
50707
diff
changeset
|
49 |
write_sessions(dir, sessions) |
6ac3c29a300e
discontinued "isabelle usedir" option -r (reset session path);
wenzelm
parents:
50707
diff
changeset
|
50 |
File.write(dir + index_path, HTML.chapter_index(chapter, sessions)) |
6ac3c29a300e
discontinued "isabelle usedir" option -r (reset session path);
wenzelm
parents:
50707
diff
changeset
|
51 |
} |
61372 | 52 |
|
53 |
def make_global_index(browser_info: Path) |
|
54 |
{ |
|
55 |
if (!(browser_info + Path.explode("index.html")).is_file) { |
|
56 |
Isabelle_System.mkdirs(browser_info) |
|
57 |
File.copy(Path.explode("~~/lib/logo/isabelle.gif"), |
|
58 |
browser_info + Path.explode("isabelle.gif")) |
|
59 |
File.write(browser_info + Path.explode("index.html"), |
|
60 |
File.read(Path.explode("~~/lib/html/library_index_header.template")) + |
|
61 |
File.read(Path.explode("~~/lib/html/library_index_content.template")) + |
|
62 |
File.read(Path.explode("~~/lib/html/library_index_footer.template"))) |
|
63 |
} |
|
64 |
} |
|
65 |
||
66 |
||
67 |
/* finish session */ |
|
68 |
||
69 |
def finish( |
|
70 |
progress: Progress, |
|
71 |
browser_info: Path, |
|
72 |
graph_file: JFile, |
|
62631 | 73 |
info: Sessions.Info, |
61372 | 74 |
name: String) |
75 |
{ |
|
76 |
val session_prefix = browser_info + Path.basic(info.chapter) + Path.basic(name) |
|
65089 | 77 |
val session_fonts = session_prefix + Path.explode("fonts") |
61372 | 78 |
|
79 |
if (info.options.bool("browser_info")) { |
|
65089 | 80 |
Isabelle_System.mkdirs(session_fonts) |
62971
087e36ce0593
back to exact copy of non-text file (amending dcc8e1d34b18);
wenzelm
parents:
62631
diff
changeset
|
81 |
|
087e36ce0593
back to exact copy of non-text file (amending dcc8e1d34b18);
wenzelm
parents:
62631
diff
changeset
|
82 |
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
|
83 |
File.copy(graph_file, session_graph.file) |
087e36ce0593
back to exact copy of non-text file (amending dcc8e1d34b18);
wenzelm
parents:
62631
diff
changeset
|
84 |
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
|
85 |
|
61372 | 86 |
File.copy(Path.explode("~~/etc/isabelle.css"), session_prefix) |
61500 | 87 |
|
65083 | 88 |
for (font <- Isabelle_System.fonts(html = true)) |
65089 | 89 |
File.copy(font, session_fonts) |
61372 | 90 |
} |
91 |
} |
|
50707
5b2bf7611662
maintain session index on Scala side, for more determistic results;
wenzelm
parents:
diff
changeset
|
92 |
} |