# HG changeset patch
# User wenzelm
# Date 954094433 -7200
# Node ID 34c4847fd8c11fe775e6993aca71373eec5f19cc
# Parent  3051aa8aa412302f11f511595881ef73d8027316
ignore_stuff;
P.!!!!;

diff -r 3051aa8aa412 -r 34c4847fd8c1 src/Pure/Isar/outer_syntax.ML
--- a/src/Pure/Isar/outer_syntax.ML	Sun Mar 26 20:12:28 2000 +0200
+++ b/src/Pure/Isar/outer_syntax.ML	Sun Mar 26 20:13:53 2000 +0200
@@ -343,24 +343,36 @@
 
 local
 
-val indent_prop = Scan.one T.is_indent -- Scan.one T.is_proper;
-val improp = Scan.unless indent_prop (Scan.one (not o T.is_proper));
-val improper_keep_indent = Scan.repeat improp;
+val is_improper = not o (T.is_proper orf T.is_begin_ignore orf T.is_end_ignore);
+val improper = Scan.any is_improper;
 
-val improper = Scan.any (not o T.is_proper);
+val improper_keep_indent = Scan.repeat
+  (Scan.unless (Scan.one T.is_indent -- Scan.one T.is_proper) (Scan.one is_improper));
 
 val improper_end =
   (improper -- semicolon) |-- improper_keep_indent ||
   improper_keep_indent;
 
+
+val ignore =
+  Scan.depend (fn d => Scan.one T.is_begin_ignore >> pair (d + 1)) ||
+  Scan.depend (fn 0 => Scan.fail | d => Scan.one T.is_end_ignore >> pair (d - 1)) ||
+  Scan.lift (Scan.one (OuterLex.not_eof andf (not o OuterLex.is_end_ignore)));
+
+val ignore_stuff =
+  Scan.one T.is_begin_ignore |--
+    P.!!!! (Scan.pass 0 (Scan.repeat ignore) -- Scan.one T.is_end_ignore);
+
 val markup = Scan.one (T.is_kind T.Command andf is_markup o T.val_of) >> T.val_of;
 val verbatim = Scan.one (T.is_kind T.Command andf is_verbatim o T.val_of);
 
 val present_token =
-  improper |-- markup -- (improper |-- P.text --| improper_end) >> Present.markup_token ||
-  (P.$$$ "--" >> K "cmt") -- (improper |-- P.text) >> Present.markup_token ||
-  (improper -- verbatim -- improper) |-- P.text --| improper_end >> Present.verbatim_token ||
-  Scan.one T.not_eof >> Present.basic_token;
+  ignore_stuff >> K None ||
+  (improper |-- markup -- P.!!!! (improper |-- P.text --| improper_end) >> Present.markup_token ||
+    (P.$$$ "--" >> K "cmt") -- P.!!!! (improper |-- P.text) >> Present.markup_token ||
+    (improper -- verbatim) |-- P.!!!! (improper |-- P.text --| improper_end)
+      >> Present.verbatim_token ||
+    Scan.one T.not_eof >> Present.basic_token) >> Some;
 
 in
 
@@ -368,7 +380,8 @@
 
 fun present_toks text pos () =
   token_source (Source.of_list (Library.untabify text), pos)
-  |> Source.source T.stopper (Scan.bulk present_token) None
+  |> Source.source T.stopper (Scan.bulk (Scan.error present_token)) None
+  |> Source.mapfilter I
   |> Source.exhaust;
 
 fun present_text text () =