# HG changeset patch
# User wenzelm
# Date 1412098654 -7200
# Node ID ea22f23808714e6f3cdead4546318c45a845d177
# Parent  d37c712cc01bd5f996f69909d3cf032c60bfba3e
tuned;

diff -r d37c712cc01b -r ea22f2380871 src/Pure/Isar/outer_syntax.scala
--- a/src/Pure/Isar/outer_syntax.scala	Tue Sep 30 18:44:01 2014 +0200
+++ b/src/Pure/Isar/outer_syntax.scala	Tue Sep 30 19:37:34 2014 +0200
@@ -126,7 +126,7 @@
 
   def scan(input: CharSequence): List[Token] =
   {
-    var in: Reader[Char] = new CharSequenceReader(input)
+    val in: Reader[Char] = new CharSequenceReader(input)
     Token.Parsers.parseAll(
         Token.Parsers.rep(Token.Parsers.token(lexicon, is_command)), in) match {
       case Token.Parsers.Success(tokens, _) => tokens