Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
tuned;
authorwenzelm
Sun, 21 Aug 2011 19:32:20 +0200
changeset 44354 88bf93c2ae7c
parent 44353 02f286491568
child 44355 9c38bdc6d755
tuned;
src/Pure/Thy/thy_syntax.ML file | annotate | diff | comparison | revisions 
--- 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
isabelle