1.1 --- a/src/Pure/ML/ml_lex.ML Mon Jan 10 21:21:23 2011 +0100
1.2 +++ b/src/Pure/ML/ml_lex.ML Mon Jan 10 21:45:44 2011 +0100
1.3 @@ -70,6 +70,14 @@
1.4 fun content_of (Token (_, (_, x))) = x;
1.5 fun token_leq (tok, tok') = content_of tok <= content_of tok';
1.6
1.7 +fun is_regular (Token (_, (Error _, _))) = false
1.8 + | is_regular (Token (_, (EOF, _))) = false
1.9 + | is_regular _ = true;
1.10 +
1.11 +fun is_improper (Token (_, (Space, _))) = true
1.12 + | is_improper (Token (_, (Comment, _))) = true
1.13 + | is_improper _ = false;
1.14 +
1.15 fun warn tok =
1.16 (case tok of
1.17 Token (_, (Keyword, ":>")) =>
1.18 @@ -83,15 +91,13 @@
1.19 Error msg => error msg
1.20 | _ => content_of tok);
1.21
1.22 -val flatten = implode o map (Symbol.escape o check_content_of);
1.23 +fun flatten_content (tok :: (toks as tok' :: _)) =
1.24 + Symbol.escape (check_content_of tok) ::
1.25 + (if is_improper tok orelse is_improper tok' then flatten_content toks
1.26 + else Symbol.space :: flatten_content toks)
1.27 + | flatten_content toks = map (Symbol.escape o check_content_of) toks;
1.28
1.29 -fun is_regular (Token (_, (Error _, _))) = false
1.30 - | is_regular (Token (_, (EOF, _))) = false
1.31 - | is_regular _ = true;
1.32 -
1.33 -fun is_improper (Token (_, (Space, _))) = true
1.34 - | is_improper (Token (_, (Comment, _))) = true
1.35 - | is_improper _ = false;
1.36 +val flatten = implode o flatten_content;
1.37
1.38
1.39 (* markup *)