added is_begin/end_ignore;

--- a/src/Pure/Isar/outer_lex.ML	Sun Mar 26 20:08:03 2000 +0200
+++ b/src/Pure/Isar/outer_lex.ML	Sun Mar 26 20:10:31 2000 +0200
@@ -21,6 +21,8 @@
   val keyword_with: (string -> bool) -> token -> bool
   val name_of: token -> string
   val is_proper: token -> bool
+  val is_begin_ignore: token -> bool
+  val is_end_ignore: token -> bool
   val is_indent: token -> bool
   val val_of: token -> string
   val is_sid: string -> bool
@@ -99,6 +101,12 @@
   | is_proper (Token (_, (Comment, _))) = false
   | is_proper _ = true;
 
+fun is_begin_ignore (Token (_, (Comment, "<"))) = true
+  | is_begin_ignore _ = false;
+
+fun is_end_ignore (Token (_, (Comment, ">"))) = true
+  | is_end_ignore _ = false;
+
 (*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