# HG changeset patch
# User wenzelm
# Date 1260181124 -3600
# Node ID f215f52b7ff17509294ac012a864ecd53c4235a6
# Parent 5426ada71790723e0a5e879e39a396440d471ea1# Parent bbd146caa6b2545c05498e3975c7d87d36d7b171
merged
diff -r 5426ada71790 -r f215f52b7ff1 src/Pure/General/symbol.scala
--- a/src/Pure/General/symbol.scala Mon Dec 07 09:35:18 2009 +0100
+++ b/src/Pure/General/symbol.scala Mon Dec 07 11:18:44 2009 +0100
@@ -13,8 +13,7 @@
object Symbol
{
-
- /** Symbol regexps **/
+ /* Symbol regexps */
private val plain = new Regex("""(?xs)
[^\\ \ud800-\udfff] | [\ud800-\udbff][\udc00-\udfff] """)
@@ -31,35 +30,57 @@
val regex = new Regex(plain + "|" + symbol + "|" + bad_symbol + "| .")
// prefix of another symbol
- def is_open(s: String): Boolean =
+ def is_open(s: CharSequence): Boolean =
{
val len = s.length
- len == 1 && Character.isLowSurrogate(s(0)) ||
+ len == 1 && Character.isHighSurrogate(s.charAt(0)) ||
s == "\\" ||
s == "\\<" ||
- len > 2 && s(len - 1) != '>'
+ len > 2 && s.charAt(len - 1) != '>'
}
- /** Decoding offsets **/
+ /* elements */
+
+ private def could_open(c: Char): Boolean =
+ c == '\\' || Character.isHighSurrogate(c)
- class Index(text: String)
+ def elements(text: CharSequence) = new Iterator[String] {
+ private val matcher = regex.pattern.matcher(text)
+ private var i = 0
+ def hasNext = i < text.length
+ def next = {
+ val len =
+ if (could_open(text.charAt(i))) {
+ matcher.region(i, text.length).lookingAt
+ matcher.group.length
+ }
+ else 1
+ val s = text.subSequence(i, i + len)
+ i += len
+ s.toString
+ }
+ }
+
+
+ /* decoding offsets */
+
+ class Index(text: CharSequence)
{
case class Entry(chr: Int, sym: Int)
val index: Array[Entry] =
{
- val length = text.length
val matcher = regex.pattern.matcher(text)
val buf = new mutable.ArrayBuffer[Entry]
var chr = 0
var sym = 0
- while (chr < length) {
- val c = text(chr)
+ while (chr < text.length) {
val len =
- if (c == '\\' || Character.isHighSurrogate(c)) {
- matcher.region(chr, length).lookingAt
+ if (could_open(text.charAt(chr))) {
+ matcher.region(chr, text.length).lookingAt
matcher.group.length
- } else 1
+ }
+ else 1
chr += len
sym += 1
if (len > 1) buf += Entry(chr, sym)
@@ -86,7 +107,7 @@
}
- /** Recoding text **/
+ /* recoding text */
private class Recoder(list: List[(String, String)])
{
@@ -195,6 +216,5 @@
def decode(text: String) = decoder.recode(text)
def encode(text: String) = encoder.recode(text)
-
}
}
diff -r 5426ada71790 -r f215f52b7ff1 src/Pure/General/xml.scala
--- a/src/Pure/General/xml.scala Mon Dec 07 09:35:18 2009 +0100
+++ b/src/Pure/General/xml.scala Mon Dec 07 11:18:44 2009 +0100
@@ -26,35 +26,41 @@
case class Elem(name: String, attributes: Attributes, body: List[Tree]) extends Tree
case class Text(content: String) extends Tree
+ def elem(name: String, body: List[Tree]) = Elem(name, Nil, body)
+ def elem(name: String) = Elem(name, Nil, Nil)
+
/* string representation */
private def append_text(text: String, s: StringBuilder) {
- for (c <- text.elements) c match {
- case '<' => s.append("<")
- case '>' => s.append(">")
- case '&' => s.append("&")
- case '"' => s.append(""")
- case '\'' => s.append("'")
- case _ => s.append(c)
+ if (text == null) s ++ text
+ else {
+ for (c <- text.elements) c match {
+ case '<' => s ++ "<"
+ case '>' => s ++ ">"
+ case '&' => s ++ "&"
+ case '"' => s ++ """
+ case '\'' => s ++ "'"
+ case _ => s + c
+ }
}
}
private def append_elem(name: String, atts: Attributes, s: StringBuilder) {
- s.append(name)
+ s ++ name
for ((a, x) <- atts) {
- s.append(" "); s.append(a); s.append("=\""); append_text(x, s); s.append("\"")
+ s ++ " "; s ++ a; s ++ "=\""; append_text(x, s); s ++ "\""
}
}
private def append_tree(tree: Tree, s: StringBuilder) {
tree match {
case Elem(name, atts, Nil) =>
- s.append("<"); append_elem(name, atts, s); s.append("/>")
+ s ++ "<"; append_elem(name, atts, s); s ++ "/>"
case Elem(name, atts, ts) =>
- s.append("<"); append_elem(name, atts, s); s.append(">")
+ s ++ "<"; append_elem(name, atts, s); s ++ ">"
for (t <- ts) append_tree(t, s)
- s.append("")
+ s ++ ""
case Text(text) => append_text(text, s)
}
}
diff -r 5426ada71790 -r f215f52b7ff1 src/Pure/Thy/html.ML
--- a/src/Pure/Thy/html.ML Mon Dec 07 09:35:18 2009 +0100
+++ b/src/Pure/Thy/html.ML Mon Dec 07 11:18:44 2009 +0100
@@ -58,7 +58,8 @@
val hidden = XML.text #> (span Markup.hiddenN |-> enclose);
val html_syms = Symtab.make
- [("\n", (0, "
")),
+ [("", (0, "")),
+ ("\n", (0, "
")),
("'", (1, "'")),
("\\", (2, " ")),
("\\", (1, "¡")),
@@ -221,13 +222,14 @@
val output_bold = output_markup (span "bold");
val output_loc = output_markup (span "loc");
- fun output_syms (s1 :: s2 :: ss) =
- if s1 = "\\<^sub>" orelse s1 = "\\<^isub>" then output_sub s1 s2 :: output_syms ss
- else if s1 = "\\<^sup>" orelse s1 = "\\<^isup>" then output_sup s1 s2 :: output_syms ss
- else if s1 = "\\<^bold>" then output_bold s1 s2 :: output_syms ss
- else if s1 = "\\<^loc>" then output_loc s1 s2 :: output_syms ss
- else output_sym s1 :: output_syms (s2 :: ss)
- | output_syms (s :: ss) = output_sym s :: output_syms ss
+ fun output_syms (s1 :: rest) =
+ let val (s2, ss) = (case rest of [] => ("", []) | s2 :: ss => (s2, ss)) in
+ if s1 = "\\<^sub>" orelse s1 = "\\<^isub>" then output_sub s1 s2 :: output_syms ss
+ else if s1 = "\\<^sup>" orelse s1 = "\\<^isup>" then output_sup s1 s2 :: output_syms ss
+ else if s1 = "\\<^bold>" then output_bold s1 s2 :: output_syms ss
+ else if s1 = "\\<^loc>" then output_loc s1 s2 :: output_syms ss
+ else output_sym s1 :: output_syms rest
+ end
| output_syms [] = [];
in
diff -r 5426ada71790 -r f215f52b7ff1 src/Pure/Thy/html.scala
--- a/src/Pure/Thy/html.scala Mon Dec 07 09:35:18 2009 +0100
+++ b/src/Pure/Thy/html.scala Mon Dec 07 11:18:44 2009 +0100
@@ -6,6 +6,9 @@
package isabelle
+import scala.collection.mutable.ListBuffer
+
+
object HTML
{
// common elements and attributes
@@ -14,28 +17,55 @@
val DIV = "div"
val SPAN = "span"
val BR = "br"
+ val PRE = "pre"
val CLASS = "class"
// document markup
- def body(trees: List[XML.Tree]): XML.Tree =
- XML.Elem(BODY, Nil, trees)
+ def span(cls: String, body: List[XML.Tree]): XML.Elem =
+ XML.Elem(SPAN, List((CLASS, cls)), body)
- def div(trees: List[XML.Tree]): XML.Tree =
- XML.Elem(DIV, Nil, trees)
+ def hidden(txt: String): XML.Elem =
+ span(Markup.HIDDEN, List(XML.Text(txt)))
- val br: XML.Tree = XML.Elem(BR, Nil, Nil)
+ def sub(txt: String): XML.Elem = XML.elem("sub", List(XML.Text(txt)))
+ def sup(txt: String): XML.Elem = XML.elem("sup", List(XML.Text(txt)))
def spans(tree: XML.Tree): List[XML.Tree] =
tree match {
- case XML.Elem(name, _, ts) =>
- List(XML.Elem(SPAN, List((CLASS, name)), ts.flatMap(spans)))
- case text @ XML.Text(txt) =>
- txt.split("\n").toList match {
- case line :: lines if !lines.isEmpty =>
- XML.Text(line) :: lines.flatMap(l => List(br, XML.Text(l)))
- case _ => List(text)
+ case XML.Elem(name, _, ts) => List(span(name, ts.flatMap(spans)))
+ case XML.Text(txt) =>
+ val ts = new ListBuffer[XML.Tree]
+ val t = new StringBuilder
+ def flush() {
+ if (!t.isEmpty) {
+ ts + XML.Text(t.toString)
+ t.clear
+ }
+ }
+ def add(elem: XML.Tree) {
+ flush()
+ ts + elem
}
+ val syms = Symbol.elements(txt)
+ while (syms.hasNext) {
+ val s1 = syms.next
+ def s2() = if (syms.hasNext) syms.next else ""
+ s1 match {
+ case "\n" => add(XML.elem(BR))
+ case "\\<^bsub>" => t ++ s1 // FIXME
+ case "\\<^esub>" => t ++ s1 // FIXME
+ case "\\<^bsup>" => t ++ s1 // FIXME
+ case "\\<^esup>" => t ++ s1 // FIXME
+ case "\\<^sub>" | "\\<^isub>" => add(hidden(s1)); add(sub(s2()))
+ case "\\<^sup>" | "\\<^isup>" => add(hidden(s1)); add(sup(s2()))
+ case "\\<^bold>" => add(hidden(s1)); add(span("bold", List(XML.Text(s2()))))
+ case "\\<^loc>" => add(hidden(s1)); add(span("loc", List(XML.Text(s2()))))
+ case _ => t ++ s1
+ }
+ }
+ flush()
+ ts.toList
}
}