--- a/src/Pure/GUI/gui.scala Sat Jan 09 20:56:00 2016 +0100
+++ b/src/Pure/GUI/gui.scala Sat Jan 09 22:00:22 2016 +0100
@@ -166,7 +166,7 @@
def tooltip_lines(text: String): String =
if (text == null || text == "") null
- else "<html>" + HTML.encode(text) + "</html>"
+ else "<html>" + HTML.output(text) + "</html>"
/* icon */
--- a/src/Pure/Thy/html.scala Sat Jan 09 20:56:00 2016 +0100
+++ b/src/Pure/Thy/html.scala Sat Jan 09 22:00:22 2016 +0100
@@ -20,11 +20,11 @@
Symbol.bold -> "b",
Symbol.bold_decoded -> "b")
- def encode(text: String): String =
+ def output(text: String): String =
{
val result = new StringBuilder
- def encode_char(c: Char) =
+ def output_char(c: Char) =
c match {
case '<' => result ++= "<"
case '>' => result ++= ">"
@@ -34,7 +34,7 @@
case '\n' => result ++= "<br/>"
case _ => result += c
}
- def encode_chars(s: String) = s.iterator.foreach(encode_char(_))
+ def output_chars(s: String) = s.iterator.foreach(output_char(_))
var ctrl = ""
for (sym <- Symbol.iterator(text)) {
@@ -43,16 +43,16 @@
control.get(ctrl) match {
case Some(elem) if Symbol.is_controllable(sym) && sym != "\"" =>
result ++= ("<" + elem + ">")
- encode_chars(sym)
+ output_chars(sym)
result ++= ("</" + elem + ">")
case _ =>
- encode_chars(ctrl)
- encode_chars(sym)
+ output_chars(ctrl)
+ output_chars(sym)
}
ctrl = ""
}
}
- encode_chars(ctrl)
+ output_chars(ctrl)
result.toString
}
@@ -60,8 +60,6 @@
/* document */
- val end_document = "\n</div>\n</body>\n</html>\n"
-
def begin_document(title: String): String =
"<?xml version=\"1.0\" encoding=\"utf-8\" ?>\n" +
"<!DOCTYPE html PUBLIC \"-//W3C//DTD XHTML 1.0 Transitional//EN\" " +
@@ -69,13 +67,15 @@
"<html xmlns=\"http://www.w3.org/1999/xhtml\">\n" +
"<head>\n" +
"<meta http-equiv=\"Content-Type\" content=\"text/html; charset=utf-8\"/>\n" +
- "<title>" + encode(title) + "</title>\n" +
+ "<title>" + output(title + " (" + Distribution.version + ")") + "</title>\n" +
"<link media=\"all\" rel=\"stylesheet\" type=\"text/css\" href=\"isabelle.css\"/>\n" +
"</head>\n" +
"\n" +
"<body>\n" +
"<div class=\"head\">" +
- "<h1>" + encode(title) + "</h1>\n"
+ "<h1>" + output(title) + "</h1>\n"
+
+ val end_document = "\n</div>\n</body>\n</html>\n"
/* common markup elements */
--- a/src/Tools/jEdit/src/bibtex_jedit.scala Sat Jan 09 20:56:00 2016 +0100
+++ b/src/Tools/jEdit/src/bibtex_jedit.scala Sat Jan 09 22:00:22 2016 +0100
@@ -254,8 +254,8 @@
if (kind != "") {
val label = kind + (if (name == "") "" else " " + name)
val label_html =
- "<html><b>" + HTML.encode(kind) + "</b>" +
- (if (name == "") "" else " " + HTML.encode(name)) + "</html>"
+ "<html><b>" + HTML.output(kind) + "</b>" +
+ (if (name == "") "" else " " + HTML.output(name)) + "</html>"
val range = Text.Range(offset, offset + source.length)
val asset = new Asset(label, label_html, range, source)
data.root.add(new DefaultMutableTreeNode(asset))
--- a/src/Tools/jEdit/src/completion_popup.scala Sat Jan 09 20:56:00 2016 +0100
+++ b/src/Tools/jEdit/src/completion_popup.scala Sat Jan 09 22:00:22 2016 +0100
@@ -35,8 +35,8 @@
private val html =
item.description match {
case a :: bs =>
- "<html><b>" + HTML.encode(a) + "</b>" +
- HTML.encode(bs.map(" " + _).mkString) + "</html>"
+ "<html><b>" + HTML.output(a) + "</b>" +
+ HTML.output(bs.map(" " + _).mkString) + "</html>"
case Nil => ""
}
override def toString: String = html
--- a/src/Tools/jEdit/src/documentation_dockable.scala Sat Jan 09 20:56:00 2016 +0100
+++ b/src/Tools/jEdit/src/documentation_dockable.scala Sat Jan 09 22:00:22 2016 +0100
@@ -24,7 +24,7 @@
private case class Documentation(name: String, title: String, path: Path)
{
override def toString: String =
- "<html><b>" + HTML.encode(name) + "</b>: " + HTML.encode(title) + "</html>"
+ "<html><b>" + HTML.output(name) + "</b>: " + HTML.output(title) + "</html>"
}
private case class Text_File(name: String, path: Path)
--- a/src/Tools/jEdit/src/isabelle_sidekick.scala Sat Jan 09 20:56:00 2016 +0100
+++ b/src/Tools/jEdit/src/isabelle_sidekick.scala Sat Jan 09 22:00:22 2016 +0100
@@ -44,10 +44,10 @@
val s =
_name.indexOf(keyword) match {
case i if i >= 0 && n > 0 =>
- HTML.encode(_name.substring(0, i)) +
- "<b>" + HTML.encode(keyword) + "</b>" +
- HTML.encode(_name.substring(i + n))
- case _ => HTML.encode(_name)
+ HTML.output(_name.substring(0, i)) +
+ "<b>" + HTML.output(keyword) + "</b>" +
+ HTML.output(_name.substring(i + n))
+ case _ => HTML.output(_name)
}
"<html><span style=\"" + css + "\">" + s + "</span></html>"
}