tuned;
authorwenzelm
Sun Aug 21 19:32:20 2011 +0200 (2011-08-21)
changeset 4435488bf93c2ae7c
parent 44353 02f286491568
child 44355 9c38bdc6d755
tuned;
src/Pure/Thy/thy_syntax.ML
     1.1 --- a/src/Pure/Thy/thy_syntax.ML	Sun Aug 21 14:16:44 2011 +0200
     1.2 +++ b/src/Pure/Thy/thy_syntax.ML	Sun Aug 21 19:32:20 2011 +0200
     1.3 @@ -115,15 +115,15 @@
     1.4  
     1.5  local
     1.6  
     1.7 -val is_whitespace = Token.is_kind Token.Space orf Token.is_kind Token.Comment;
     1.8 +val whitespace = Scan.many (not o Token.is_proper);
     1.9 +val whitespace1 = Scan.many1 (not o Token.is_proper);
    1.10  
    1.11 -val body =
    1.12 -  Scan.unless (Scan.many is_whitespace -- Scan.ahead (Parse.command || Parse.eof)) Parse.not_eof;
    1.13 +val body = Scan.unless (whitespace -- Scan.ahead (Parse.command || Parse.eof)) Parse.not_eof;
    1.14  
    1.15  val span =
    1.16    Scan.ahead Parse.command -- Parse.not_eof -- Scan.repeat body
    1.17      >> (fn ((name, c), bs) => Span (Command name, c :: bs)) ||
    1.18 -  Scan.many1 is_whitespace >> (fn toks => Span (Ignored, toks)) ||
    1.19 +  whitespace1 >> (fn toks => Span (Ignored, toks)) ||
    1.20    Scan.repeat1 body >> (fn toks => Span (Malformed, toks));
    1.21  
    1.22  in