--- a/src/Pure/Isar/outer_lex.ML Sat Apr 01 20:12:15 2000 +0200
+++ b/src/Pure/Isar/outer_lex.ML Sat Apr 01 20:12:52 2000 +0200
@@ -23,6 +23,7 @@
val is_proper: token -> bool
val is_begin_ignore: token -> bool
val is_end_ignore: token -> bool
+ val is_newline: token -> bool
val is_indent: token -> bool
val val_of: token -> string
val is_sid: string -> bool
@@ -107,7 +108,12 @@
fun is_end_ignore (Token (_, (Comment, ">"))) = true
| is_end_ignore _ = false;
-(*indentations; note that space tokens obey lines*)
+
+(* newline and indentations (note that space tokens obey lines) *)
+
+fun is_newline (Token (_, (Space, "\n"))) = true
+ | is_newline _ = false;
+
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;