# HG changeset patch
# User wenzelm
# Date 954094231 -7200
# Node ID e79ee31d3936e38331665188f3abb2dadd55886b
# Parent  81ef0fc80822a8203ca072cc5beb8d3590da5695
added is_begin/end_ignore;

diff -r 81ef0fc80822 -r e79ee31d3936 src/Pure/Isar/outer_lex.ML
--- 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