# HG changeset patch
# User wenzelm
# Date 1313947940 -7200
# Node ID 88bf93c2ae7c1dd06f23eb1b77bf38295b6d8d9f
# Parent  02f286491568f8f09c45a924678b4617f8dfa821
tuned;

diff -r 02f286491568 -r 88bf93c2ae7c src/Pure/Thy/thy_syntax.ML
--- a/src/Pure/Thy/thy_syntax.ML	Sun Aug 21 14:16:44 2011 +0200
+++ b/src/Pure/Thy/thy_syntax.ML	Sun Aug 21 19:32:20 2011 +0200
@@ -115,15 +115,15 @@
 
 local
 
-val is_whitespace = Token.is_kind Token.Space orf Token.is_kind Token.Comment;
+val whitespace = Scan.many (not o Token.is_proper);
+val whitespace1 = Scan.many1 (not o Token.is_proper);
 
-val body =
-  Scan.unless (Scan.many is_whitespace -- Scan.ahead (Parse.command || Parse.eof)) Parse.not_eof;
+val body = Scan.unless (whitespace -- Scan.ahead (Parse.command || Parse.eof)) Parse.not_eof;
 
 val span =
   Scan.ahead Parse.command -- Parse.not_eof -- Scan.repeat body
     >> (fn ((name, c), bs) => Span (Command name, c :: bs)) ||
-  Scan.many1 is_whitespace >> (fn toks => Span (Ignored, toks)) ||
+  whitespace1 >> (fn toks => Span (Ignored, toks)) ||
   Scan.repeat1 body >> (fn toks => Span (Malformed, toks));
 
 in