author | wenzelm |
Tue, 14 May 2013 19:30:21 +0200 | |
changeset 51987 | 7d8e0e3c553b |
parent 51416 | e2505a192a7c |
child 60077 | 55cb9462e602 |
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 |
|
51402 | 10 |
import scala.collection.immutable.SortedMap |
11 |
||
12 |
||
50707
5b2bf7611662
maintain session index on Scala side, for more determistic results;
wenzelm
parents:
diff
changeset
|
13 |
object Present |
5b2bf7611662
maintain session index on Scala side, for more determistic results;
wenzelm
parents:
diff
changeset
|
14 |
{ |
51399
6ac3c29a300e
discontinued "isabelle usedir" option -r (reset session path);
wenzelm
parents:
50707
diff
changeset
|
15 |
/* maintain chapter index -- NOT thread-safe */ |
50707
5b2bf7611662
maintain session index on Scala side, for more determistic results;
wenzelm
parents:
diff
changeset
|
16 |
|
5b2bf7611662
maintain session index on Scala side, for more determistic results;
wenzelm
parents:
diff
changeset
|
17 |
private val index_path = Path.basic("index.html") |
51399
6ac3c29a300e
discontinued "isabelle usedir" option -r (reset session path);
wenzelm
parents:
50707
diff
changeset
|
18 |
private val sessions_path = Path.basic(".sessions") |
50707
5b2bf7611662
maintain session index on Scala side, for more determistic results;
wenzelm
parents:
diff
changeset
|
19 |
|
51402 | 20 |
private def read_sessions(dir: Path): List[(String, String)] = |
21 |
{ |
|
51416 | 22 |
val path = dir + sessions_path |
23 |
if (path.is_file) { |
|
24 |
import XML.Decode._ |
|
25 |
list(pair(string, string))(YXML.parse_body(File.read(path))) |
|
26 |
} |
|
27 |
else Nil |
|
51402 | 28 |
} |
50707
5b2bf7611662
maintain session index on Scala side, for more determistic results;
wenzelm
parents:
diff
changeset
|
29 |
|
51402 | 30 |
private def write_sessions(dir: Path, sessions: List[(String, String)]) |
31 |
{ |
|
32 |
import XML.Encode._ |
|
33 |
File.write(dir + sessions_path, YXML.string_of_body(list(pair(string, string))(sessions))) |
|
34 |
} |
|
50707
5b2bf7611662
maintain session index on Scala side, for more determistic results;
wenzelm
parents:
diff
changeset
|
35 |
|
51402 | 36 |
def update_chapter_index(info_path: Path, chapter: String, new_sessions: List[(String, String)]) |
51399
6ac3c29a300e
discontinued "isabelle usedir" option -r (reset session path);
wenzelm
parents:
50707
diff
changeset
|
37 |
{ |
6ac3c29a300e
discontinued "isabelle usedir" option -r (reset session path);
wenzelm
parents:
50707
diff
changeset
|
38 |
val dir = info_path + Path.basic(chapter) |
6ac3c29a300e
discontinued "isabelle usedir" option -r (reset session path);
wenzelm
parents:
50707
diff
changeset
|
39 |
Isabelle_System.mkdirs(dir) |
50707
5b2bf7611662
maintain session index on Scala side, for more determistic results;
wenzelm
parents:
diff
changeset
|
40 |
|
51399
6ac3c29a300e
discontinued "isabelle usedir" option -r (reset session path);
wenzelm
parents:
50707
diff
changeset
|
41 |
val sessions0 = |
51406
950b897f95bb
proper path -- I/O was hidden due to permissiveness;
wenzelm
parents:
51402
diff
changeset
|
42 |
try { read_sessions(dir) } |
51987 | 43 |
catch { case _: XML.Error => Nil } |
51399
6ac3c29a300e
discontinued "isabelle usedir" option -r (reset session path);
wenzelm
parents:
50707
diff
changeset
|
44 |
|
51402 | 45 |
val sessions = (SortedMap.empty[String, String] ++ sessions0 ++ new_sessions).toList |
46 |
||
51399
6ac3c29a300e
discontinued "isabelle usedir" option -r (reset session path);
wenzelm
parents:
50707
diff
changeset
|
47 |
write_sessions(dir, sessions) |
6ac3c29a300e
discontinued "isabelle usedir" option -r (reset session path);
wenzelm
parents:
50707
diff
changeset
|
48 |
File.write(dir + index_path, HTML.chapter_index(chapter, sessions)) |
6ac3c29a300e
discontinued "isabelle usedir" option -r (reset session path);
wenzelm
parents:
50707
diff
changeset
|
49 |
} |
50707
5b2bf7611662
maintain session index on Scala side, for more determistic results;
wenzelm
parents:
diff
changeset
|
50 |
} |
5b2bf7611662
maintain session index on Scala side, for more determistic results;
wenzelm
parents:
diff
changeset
|
51 |