# 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 }