# HG changeset patch
# User wenzelm
# Date 954612772 -7200
# Node ID f095f3b8181a60c055e2bd5c10d7851555b9c39f
# Parent  b7542463e93671109f4585eaa94833e6c4428bc9
added is_newline;

diff -r b7542463e936 -r f095f3b8181a src/Pure/Isar/outer_lex.ML
--- 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;