author | wenzelm |
Sun, 09 Mar 2014 17:40:02 +0100 | |
changeset 56007 | 1b61dfbcf9a4 |
parent 55618 | 995162143ef4 |
child 56745 | 5e3db9209bcf |
permissions | -rw-r--r-- |
33984 | 1 |
/* Title: Pure/Thy/html.scala |
54379 | 2 |
Module: PIDE-GUI |
33984 | 3 |
Author: Makarius |
4 |
||
50707
5b2bf7611662
maintain session index on Scala side, for more determistic results;
wenzelm
parents:
50201
diff
changeset
|
5 |
HTML presentation elements. |
33984 | 6 |
*/ |
7 |
||
8 |
package isabelle |
|
9 |
||
55618 | 10 |
|
34000
1fecda948697
more robust treatment of line breaks -- Java "split" has off semantics;
wenzelm
parents:
33984
diff
changeset
|
11 |
import scala.collection.mutable.ListBuffer |
1fecda948697
more robust treatment of line breaks -- Java "split" has off semantics;
wenzelm
parents:
33984
diff
changeset
|
12 |
|
1fecda948697
more robust treatment of line breaks -- Java "split" has off semantics;
wenzelm
parents:
33984
diff
changeset
|
13 |
|
33984 | 14 |
object HTML |
15 |
{ |
|
51399
6ac3c29a300e
discontinued "isabelle usedir" option -r (reset session path);
wenzelm
parents:
50707
diff
changeset
|
16 |
/* encode text */ |
37200
0f3edc64356a
added HTML.encode (in Scala), similar to HTML.output in ML;
wenzelm
parents:
36016
diff
changeset
|
17 |
|
0f3edc64356a
added HTML.encode (in Scala), similar to HTML.output in ML;
wenzelm
parents:
36016
diff
changeset
|
18 |
def encode(text: String): String = |
0f3edc64356a
added HTML.encode (in Scala), similar to HTML.output in ML;
wenzelm
parents:
36016
diff
changeset
|
19 |
{ |
0f3edc64356a
added HTML.encode (in Scala), similar to HTML.output in ML;
wenzelm
parents:
36016
diff
changeset
|
20 |
val s = new StringBuilder |
0f3edc64356a
added HTML.encode (in Scala), similar to HTML.output in ML;
wenzelm
parents:
36016
diff
changeset
|
21 |
for (c <- text.iterator) c match { |
0f3edc64356a
added HTML.encode (in Scala), similar to HTML.output in ML;
wenzelm
parents:
36016
diff
changeset
|
22 |
case '<' => s ++= "<" |
0f3edc64356a
added HTML.encode (in Scala), similar to HTML.output in ML;
wenzelm
parents:
36016
diff
changeset
|
23 |
case '>' => s ++= ">" |
0f3edc64356a
added HTML.encode (in Scala), similar to HTML.output in ML;
wenzelm
parents:
36016
diff
changeset
|
24 |
case '&' => s ++= "&" |
0f3edc64356a
added HTML.encode (in Scala), similar to HTML.output in ML;
wenzelm
parents:
36016
diff
changeset
|
25 |
case '"' => s ++= """ |
0f3edc64356a
added HTML.encode (in Scala), similar to HTML.output in ML;
wenzelm
parents:
36016
diff
changeset
|
26 |
case '\'' => s ++= "'" |
0f3edc64356a
added HTML.encode (in Scala), similar to HTML.output in ML;
wenzelm
parents:
36016
diff
changeset
|
27 |
case '\n' => s ++= "<br/>" |
0f3edc64356a
added HTML.encode (in Scala), similar to HTML.output in ML;
wenzelm
parents:
36016
diff
changeset
|
28 |
case _ => s += c |
0f3edc64356a
added HTML.encode (in Scala), similar to HTML.output in ML;
wenzelm
parents:
36016
diff
changeset
|
29 |
} |
0f3edc64356a
added HTML.encode (in Scala), similar to HTML.output in ML;
wenzelm
parents:
36016
diff
changeset
|
30 |
s.toString |
0f3edc64356a
added HTML.encode (in Scala), similar to HTML.output in ML;
wenzelm
parents:
36016
diff
changeset
|
31 |
} |
0f3edc64356a
added HTML.encode (in Scala), similar to HTML.output in ML;
wenzelm
parents:
36016
diff
changeset
|
32 |
|
0f3edc64356a
added HTML.encode (in Scala), similar to HTML.output in ML;
wenzelm
parents:
36016
diff
changeset
|
33 |
|
51399
6ac3c29a300e
discontinued "isabelle usedir" option -r (reset session path);
wenzelm
parents:
50707
diff
changeset
|
34 |
/* document */ |
6ac3c29a300e
discontinued "isabelle usedir" option -r (reset session path);
wenzelm
parents:
50707
diff
changeset
|
35 |
|
6ac3c29a300e
discontinued "isabelle usedir" option -r (reset session path);
wenzelm
parents:
50707
diff
changeset
|
36 |
val end_document = "\n</div>\n</body>\n</html>\n" |
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 |
def begin_document(title: String): String = |
6ac3c29a300e
discontinued "isabelle usedir" option -r (reset session path);
wenzelm
parents:
50707
diff
changeset
|
39 |
"<?xml version=\"1.0\" encoding=\"utf-8\" ?>\n" + |
6ac3c29a300e
discontinued "isabelle usedir" option -r (reset session path);
wenzelm
parents:
50707
diff
changeset
|
40 |
"<!DOCTYPE html PUBLIC \"-//W3C//DTD XHTML 1.0 Transitional//EN\" " + |
6ac3c29a300e
discontinued "isabelle usedir" option -r (reset session path);
wenzelm
parents:
50707
diff
changeset
|
41 |
"\"http://www.w3.org/TR/xhtml1/DTD/xhtml1-transitional.dtd\">\n" + |
6ac3c29a300e
discontinued "isabelle usedir" option -r (reset session path);
wenzelm
parents:
50707
diff
changeset
|
42 |
"<html xmlns=\"http://www.w3.org/1999/xhtml\">\n" + |
6ac3c29a300e
discontinued "isabelle usedir" option -r (reset session path);
wenzelm
parents:
50707
diff
changeset
|
43 |
"<head>\n" + |
6ac3c29a300e
discontinued "isabelle usedir" option -r (reset session path);
wenzelm
parents:
50707
diff
changeset
|
44 |
"<meta http-equiv=\"Content-Type\" content=\"text/html; charset=utf-8\"/>\n" + |
6ac3c29a300e
discontinued "isabelle usedir" option -r (reset session path);
wenzelm
parents:
50707
diff
changeset
|
45 |
"<title>" + encode(title) + "</title>\n" + |
6ac3c29a300e
discontinued "isabelle usedir" option -r (reset session path);
wenzelm
parents:
50707
diff
changeset
|
46 |
"<link media=\"all\" rel=\"stylesheet\" type=\"text/css\" href=\"isabelle.css\"/>\n" + |
6ac3c29a300e
discontinued "isabelle usedir" option -r (reset session path);
wenzelm
parents:
50707
diff
changeset
|
47 |
"</head>\n" + |
6ac3c29a300e
discontinued "isabelle usedir" option -r (reset session path);
wenzelm
parents:
50707
diff
changeset
|
48 |
"\n" + |
6ac3c29a300e
discontinued "isabelle usedir" option -r (reset session path);
wenzelm
parents:
50707
diff
changeset
|
49 |
"<body>\n" + |
6ac3c29a300e
discontinued "isabelle usedir" option -r (reset session path);
wenzelm
parents:
50707
diff
changeset
|
50 |
"<div class=\"head\">" + |
6ac3c29a300e
discontinued "isabelle usedir" option -r (reset session path);
wenzelm
parents:
50707
diff
changeset
|
51 |
"<h1>" + encode(title) + "</h1>\n" |
6ac3c29a300e
discontinued "isabelle usedir" option -r (reset session path);
wenzelm
parents:
50707
diff
changeset
|
52 |
|
6ac3c29a300e
discontinued "isabelle usedir" option -r (reset session path);
wenzelm
parents:
50707
diff
changeset
|
53 |
|
6ac3c29a300e
discontinued "isabelle usedir" option -r (reset session path);
wenzelm
parents:
50707
diff
changeset
|
54 |
/* common markup elements */ |
33984 | 55 |
|
51402 | 56 |
private def session_entry(entry: (String, String)): String = |
57 |
{ |
|
58 |
val (name, description) = entry |
|
59 |
val descr = |
|
60 |
if (description == "") Nil |
|
61 |
else List(XML.elem("br"), XML.elem("pre", List(XML.Text(description)))) |
|
50707
5b2bf7611662
maintain session index on Scala side, for more determistic results;
wenzelm
parents:
50201
diff
changeset
|
62 |
XML.string_of_tree( |
5b2bf7611662
maintain session index on Scala side, for more determistic results;
wenzelm
parents:
50201
diff
changeset
|
63 |
XML.elem("li", |
5b2bf7611662
maintain session index on Scala side, for more determistic results;
wenzelm
parents:
50201
diff
changeset
|
64 |
List(XML.Elem(Markup("a", List(("href", name + "/index.html"))), |
51402 | 65 |
List(XML.Text(name)))) ::: descr)) + "\n" |
66 |
} |
|
34002 | 67 |
|
51402 | 68 |
def chapter_index(chapter: String, sessions: List[(String, String)]): String = |
51399
6ac3c29a300e
discontinued "isabelle usedir" option -r (reset session path);
wenzelm
parents:
50707
diff
changeset
|
69 |
{ |
6ac3c29a300e
discontinued "isabelle usedir" option -r (reset session path);
wenzelm
parents:
50707
diff
changeset
|
70 |
begin_document("Isabelle/" + chapter + " sessions") + |
6ac3c29a300e
discontinued "isabelle usedir" option -r (reset session path);
wenzelm
parents:
50707
diff
changeset
|
71 |
(if (sessions.isEmpty) "" |
6ac3c29a300e
discontinued "isabelle usedir" option -r (reset session path);
wenzelm
parents:
50707
diff
changeset
|
72 |
else "<div class=\"sessions\"><ul>\n" + sessions.map(session_entry(_)).mkString + "</ul>") + |
6ac3c29a300e
discontinued "isabelle usedir" option -r (reset session path);
wenzelm
parents:
50707
diff
changeset
|
73 |
end_document |
6ac3c29a300e
discontinued "isabelle usedir" option -r (reset session path);
wenzelm
parents:
50707
diff
changeset
|
74 |
} |
33984 | 75 |
} |