# HG changeset patch
# User wenzelm
# Date 1230394167 -3600
# Node ID 62513d4d34c2fb203b78a951a13e62af0679721d
# Parent  f27d63717075b5b8dfe528c5191945b4eb3c3b15
tuned;

diff -r f27d63717075 -r 62513d4d34c2 src/Pure/General/yxml.scala
--- a/src/Pure/General/yxml.scala	Sat Dec 27 16:34:26 2008 +0100
+++ b/src/Pure/General/yxml.scala	Sat Dec 27 17:09:27 2008 +0100
@@ -69,7 +69,7 @@
 
     var stack: List[((String, XML.Attributes), List[XML.Tree])] = null
 
-    def add(x: XML.Tree) = stack match {
+    def add(x: XML.Tree) = (stack: @unchecked) match {
       case ((elem, body) :: pending) => stack = (elem, x :: body) :: pending
     }
 
@@ -77,7 +77,7 @@
       if (name == "") err_element()
       else stack = ((name, atts), Nil) :: stack
 
-    def pop() = stack match {
+    def pop() = (stack: @unchecked) match {
       case ((("", _), _) :: _) => err_unbalanced("")
       case (((name, atts), body) :: pending) =>
         stack = pending; add(XML.Elem(name, atts, body.reverse))
diff -r f27d63717075 -r 62513d4d34c2 src/Pure/Tools/isabelle_system.scala
--- a/src/Pure/Tools/isabelle_system.scala	Sat Dec 27 16:34:26 2008 +0100
+++ b/src/Pure/Tools/isabelle_system.scala	Sat Dec 27 17:09:27 2008 +0100
@@ -88,8 +88,10 @@
     for (s <- args) cmdline.add(s)
 
     val proc = new ProcessBuilder(cmdline)
-    val env = proc.environment; env.clear; env.putAll(environment)
-    proc.redirectErrorStream(redirect).start
+    proc.environment.clear
+    proc.environment.putAll(environment)
+    proc.redirectErrorStream(redirect)
+    proc.start
   }