author | wenzelm |
Tue, 04 Apr 2017 21:33:51 +0200 | |
changeset 65376 | 4ad983094226 |
parent 65344 | b99283eed13c |
child 65377 | 6e47a27e3d43 |
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 |
{ |
60077 | 17 |
/* session graph */ |
18 |
||
19 |
def session_graph( |
|
20 |
parent_session: String, |
|
21 |
parent_loaded: String => Boolean, |
|
22 |
deps: List[Thy_Info.Dep]): Graph_Display.Graph = |
|
23 |
{ |
|
24 |
val parent_session_node = |
|
25 |
Graph_Display.Node("[" + parent_session + "]", "session." + parent_session) |
|
26 |
||
27 |
def node(name: Document.Node.Name): Graph_Display.Node = |
|
28 |
if (parent_loaded(name.theory)) parent_session_node |
|
65376 | 29 |
else Graph_Display.Node(Long_Name.base_name(name.theory), "theory." + name.theory) |
60077 | 30 |
|
31 |
(Graph_Display.empty_graph /: deps) { |
|
32 |
case (g, dep) => |
|
33 |
if (parent_loaded(dep.name.theory)) g |
|
34 |
else { |
|
35 |
val a = node(dep.name) |
|
36 |
val bs = dep.header.imports.map({ case (name, _) => node(name) }) |
|
37 |
((g /: (a :: bs))(_.default_node(_, Nil)) /: bs)(_.add_edge(_, a)) |
|
38 |
} |
|
39 |
} |
|
40 |
} |
|
41 |
||
42 |
||
51399
6ac3c29a300e
discontinued "isabelle usedir" option -r (reset session path);
wenzelm
parents:
50707
diff
changeset
|
43 |
/* maintain chapter index -- NOT thread-safe */ |
50707
5b2bf7611662
maintain session index on Scala side, for more determistic results;
wenzelm
parents:
diff
changeset
|
44 |
|
5b2bf7611662
maintain session index on Scala side, for more determistic results;
wenzelm
parents:
diff
changeset
|
45 |
private val index_path = Path.basic("index.html") |
51399
6ac3c29a300e
discontinued "isabelle usedir" option -r (reset session path);
wenzelm
parents:
50707
diff
changeset
|
46 |
private val sessions_path = Path.basic(".sessions") |
50707
5b2bf7611662
maintain session index on Scala side, for more determistic results;
wenzelm
parents:
diff
changeset
|
47 |
|
51402 | 48 |
private def read_sessions(dir: Path): List[(String, String)] = |
49 |
{ |
|
51416 | 50 |
val path = dir + sessions_path |
51 |
if (path.is_file) { |
|
52 |
import XML.Decode._ |
|
65344
b99283eed13c
clarified YXML vs. symbol encoding: operate on whole message;
wenzelm
parents:
65089
diff
changeset
|
53 |
list(pair(string, string))(Symbol.decode_yxml(File.read(path))) |
51416 | 54 |
} |
55 |
else Nil |
|
51402 | 56 |
} |
50707
5b2bf7611662
maintain session index on Scala side, for more determistic results;
wenzelm
parents:
diff
changeset
|
57 |
|
51402 | 58 |
private def write_sessions(dir: Path, sessions: List[(String, String)]) |
59 |
{ |
|
60 |
import XML.Encode._ |
|
61 |
File.write(dir + sessions_path, YXML.string_of_body(list(pair(string, string))(sessions))) |
|
62 |
} |
|
50707
5b2bf7611662
maintain session index on Scala side, for more determistic results;
wenzelm
parents:
diff
changeset
|
63 |
|
61372 | 64 |
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
|
65 |
{ |
61372 | 66 |
val dir = browser_info + Path.basic(chapter) |
51399
6ac3c29a300e
discontinued "isabelle usedir" option -r (reset session path);
wenzelm
parents:
50707
diff
changeset
|
67 |
Isabelle_System.mkdirs(dir) |
50707
5b2bf7611662
maintain session index on Scala side, for more determistic results;
wenzelm
parents:
diff
changeset
|
68 |
|
51399
6ac3c29a300e
discontinued "isabelle usedir" option -r (reset session path);
wenzelm
parents:
50707
diff
changeset
|
69 |
val sessions0 = |
51406
950b897f95bb
proper path -- I/O was hidden due to permissiveness;
wenzelm
parents:
51402
diff
changeset
|
70 |
try { read_sessions(dir) } |
51987 | 71 |
catch { case _: XML.Error => Nil } |
51399
6ac3c29a300e
discontinued "isabelle usedir" option -r (reset session path);
wenzelm
parents:
50707
diff
changeset
|
72 |
|
51402 | 73 |
val sessions = (SortedMap.empty[String, String] ++ sessions0 ++ new_sessions).toList |
74 |
||
51399
6ac3c29a300e
discontinued "isabelle usedir" option -r (reset session path);
wenzelm
parents:
50707
diff
changeset
|
75 |
write_sessions(dir, sessions) |
6ac3c29a300e
discontinued "isabelle usedir" option -r (reset session path);
wenzelm
parents:
50707
diff
changeset
|
76 |
File.write(dir + index_path, HTML.chapter_index(chapter, sessions)) |
6ac3c29a300e
discontinued "isabelle usedir" option -r (reset session path);
wenzelm
parents:
50707
diff
changeset
|
77 |
} |
61372 | 78 |
|
79 |
def make_global_index(browser_info: Path) |
|
80 |
{ |
|
81 |
if (!(browser_info + Path.explode("index.html")).is_file) { |
|
82 |
Isabelle_System.mkdirs(browser_info) |
|
83 |
File.copy(Path.explode("~~/lib/logo/isabelle.gif"), |
|
84 |
browser_info + Path.explode("isabelle.gif")) |
|
85 |
File.write(browser_info + Path.explode("index.html"), |
|
86 |
File.read(Path.explode("~~/lib/html/library_index_header.template")) + |
|
87 |
File.read(Path.explode("~~/lib/html/library_index_content.template")) + |
|
88 |
File.read(Path.explode("~~/lib/html/library_index_footer.template"))) |
|
89 |
} |
|
90 |
} |
|
91 |
||
92 |
||
93 |
/* finish session */ |
|
94 |
||
95 |
def finish( |
|
96 |
progress: Progress, |
|
97 |
browser_info: Path, |
|
98 |
graph_file: JFile, |
|
62631 | 99 |
info: Sessions.Info, |
61372 | 100 |
name: String) |
101 |
{ |
|
102 |
val session_prefix = browser_info + Path.basic(info.chapter) + Path.basic(name) |
|
65089 | 103 |
val session_fonts = session_prefix + Path.explode("fonts") |
61372 | 104 |
|
105 |
if (info.options.bool("browser_info")) { |
|
65089 | 106 |
Isabelle_System.mkdirs(session_fonts) |
62971
087e36ce0593
back to exact copy of non-text file (amending dcc8e1d34b18);
wenzelm
parents:
62631
diff
changeset
|
107 |
|
087e36ce0593
back to exact copy of non-text file (amending dcc8e1d34b18);
wenzelm
parents:
62631
diff
changeset
|
108 |
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
|
109 |
File.copy(graph_file, session_graph.file) |
087e36ce0593
back to exact copy of non-text file (amending dcc8e1d34b18);
wenzelm
parents:
62631
diff
changeset
|
110 |
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
|
111 |
|
61372 | 112 |
File.copy(Path.explode("~~/etc/isabelle.css"), session_prefix) |
61500 | 113 |
|
65083 | 114 |
for (font <- Isabelle_System.fonts(html = true)) |
65089 | 115 |
File.copy(font, session_fonts) |
61372 | 116 |
} |
117 |
} |
|
50707
5b2bf7611662
maintain session index on Scala side, for more determistic results;
wenzelm
parents:
diff
changeset
|
118 |
} |