--- a/src/Pure/Isar/outer_lex.ML Thu Oct 21 18:43:21 1999 +0200
+++ b/src/Pure/Isar/outer_lex.ML Thu Oct 21 18:44:05 1999 +0200
@@ -21,6 +21,7 @@
val keyword_with: (string -> bool) -> token -> bool
val name_of: token -> string
val is_proper: token -> bool
+ val is_indent: token -> bool
val val_of: token -> string
val is_sid: string -> bool
val scan: (Scan.lexicon * Scan.lexicon) ->
@@ -98,6 +99,11 @@
| is_proper (Token (_, (Comment, _))) = false
| is_proper _ = true;
+(*indentations; note that space tokens obey lines*)
+fun is_indent (Token (_, (Space, s))) =
+ let val n = size s in n > 0 andalso String.substring (s, n - 1, 1) <> "\n" end
+ | is_indent _ = false;
+
(* value of token *)