# HG changeset patch
# User wenzelm
# Date 940524245 -7200
# Node ID 10fd5d922c972221ea60c58b65e20e4fec72c22e
# Parent  c21c3d2256ef73f9cbbf86302be2e81942c3101c
added is_indent;

diff -r c21c3d2256ef -r 10fd5d922c97 src/Pure/Isar/outer_lex.ML
--- 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 *)