# HG changeset patch
# User wenzelm
# Date 1261146824 -3600
# Node ID 7492eca87ab4308aa67e7f7f073b9e6cb4de298b
# Parent  8650a073dd9b5d9d55af31321be12d43c9fc6e67# Parent  5e4396105332690a37aecc125703e41f60f4cdc0
merged

diff -r 8650a073dd9b -r 7492eca87ab4 lib/html/isabelle.css
--- a/lib/html/isabelle.css	Fri Dec 18 14:02:58 2009 +0100
+++ b/lib/html/isabelle.css	Fri Dec 18 15:33:44 2009 +0100
@@ -23,19 +23,19 @@
 .hidden, hidden { font-size: 0.1pt; visibility: hidden; }
 
 .tclass, tclass               { color: red; }
-.tfree, tfree                 { color: purple; }
-.tvar, tvar                   { color: purple; }
+.tfree, tfree                 { color: #A020F0; }
+.tvar, tvar                   { color: #A020F0; }
 .free, free                   { color: blue; }
-.skolem, skolem               { color: brown; }
+.skolem, skolem               { color: #D2691E; font-weight: bold; }
 .bound, bound                 { color: green; }
-.var, var                     { color: blue; }
+.var, var                     { color: #00009B; }
 .numeral, numeral             { }
 .literal, literal             { font-weight: bold; }
-.inner_string, inner_string   { color: brown; }
+.inner_string, inner_string   { color: #D2691E; }
 .inner_comment, inner_comment { color: #8B0000; }
 
 .bold, bold  { font-weight: bold; }
-.loc, loc  { color: brown; }
+.loc, loc  { color: #D2691E; }
 
 .keyword, keyword      { font-weight: bold; }
 .command, command      { font-weight: bold; }
diff -r 8650a073dd9b -r 7492eca87ab4 src/Pure/General/markup.scala
--- a/src/Pure/General/markup.scala	Fri Dec 18 14:02:58 2009 +0100
+++ b/src/Pure/General/markup.scala	Fri Dec 18 15:33:44 2009 +0100
@@ -182,9 +182,7 @@
   val READY = "ready"
 
 
-  /* content */
+  /* system data */
 
-  val ROOT = "root"
-  val BAD = "bad"
   val DATA = "data"
 }
diff -r 8650a073dd9b -r 7492eca87ab4 src/Pure/General/xml.scala
--- a/src/Pure/General/xml.scala	Fri Dec 18 14:02:58 2009 +0100
+++ b/src/Pure/General/xml.scala	Fri Dec 18 15:33:44 2009 +0100
@@ -127,20 +127,20 @@
         case Some(y) => y
         case None => store(x.map(p => (cache_string(p._1), cache_string(p._2))))
       }
-    def apply(x: XML.Tree): XML.Tree =
+    def cache_tree(x: XML.Tree): XML.Tree =
       lookup(x) match {
         case Some(y) => y
         case None =>
           x match {
             case XML.Elem(name, props, body) =>
-              store(XML.Elem(cache_string(name), cache_props(props), apply(body)))
+              store(XML.Elem(cache_string(name), cache_props(props), cache_trees(body)))
             case XML.Text(text) => XML.Text(cache_string(text))
           }
       }
-    def apply(x: List[XML.Tree]): List[XML.Tree] =
+    def cache_trees(x: List[XML.Tree]): List[XML.Tree] =
       lookup(x) match {
         case Some(y) => y
-        case None => x.map(apply(_))
+        case None => x.map(cache_tree(_))
       }
   }
 
@@ -171,21 +171,4 @@
     }
     DOM(tree)
   }
-
-  def document(tree: Tree, styles: String*): Document =
-  {
-    val doc = DocumentBuilderFactory.newInstance.newDocumentBuilder.newDocument
-    doc.appendChild(doc.createProcessingInstruction("xml", "version=\"1.0\""))
-
-    for (style <- styles) {
-      doc.appendChild(doc.createProcessingInstruction("xml-stylesheet",
-        "href=\"" + style + "\" type=\"text/css\""))
-    }
-    val root_elem = tree match {
-      case Elem(_, _, _) => document_node(doc, tree)
-      case Text(_) => document_node(doc, (Elem(Markup.ROOT, Nil, List(tree))))
-    }
-    doc.appendChild(root_elem)
-    doc
-  }
 }
diff -r 8650a073dd9b -r 7492eca87ab4 src/Pure/General/yxml.scala
--- a/src/Pure/General/yxml.scala	Fri Dec 18 14:02:58 2009 +0100
+++ b/src/Pure/General/yxml.scala	Fri Dec 18 15:33:44 2009 +0100
@@ -60,7 +60,8 @@
       def flush()
       {
         if (code != -1) {
-          if (rest == 0) buf.appendCodePoint(code)
+          if (rest == 0 && Character.isValidCodePoint(code))
+            buf.appendCodePoint(code)
           else buf.append('\uFFFD')
           code = -1
           rest = 0
@@ -170,7 +171,7 @@
   /* failsafe parsing */
 
   private def markup_failsafe(source: CharSequence) =
-    XML.Elem (Markup.BAD, Nil,
+    XML.Elem (Markup.MALFORMED, Nil,
       List(XML.Text(source.toString.replace(X_string, "\\<^X>").replace(Y_string, "\\<^Y>"))))
 
   def parse_body_failsafe(source: CharSequence): List[XML.Tree] =
diff -r 8650a073dd9b -r 7492eca87ab4 src/Pure/System/isabelle_process.scala
--- a/src/Pure/System/isabelle_process.scala	Fri Dec 18 14:02:58 2009 +0100
+++ b/src/Pure/System/isabelle_process.scala	Fri Dec 18 15:33:44 2009 +0100
@@ -101,8 +101,8 @@
     def is_control = Kind.is_control(kind)
     def is_system = Kind.is_system(kind)
 
-    def cache(table: XML.Cache): Result =
-      new Result(kind, table.cache_props(props), table(body))
+    def cache(c: XML.Cache): Result =
+      new Result(kind, c.cache_props(props), c.cache_trees(body))
   }
 }