nested source: explicit interactive flag for recover avoids duplicate errors;

--- a/src/Pure/General/scan.ML	Mon Jul 09 23:12:51 2007 +0200
+++ b/src/Pure/General/scan.ML	Tue Jul 10 00:17:52 2007 +0200
@@ -68,10 +68,11 @@
   val error: ('a -> 'b) -> 'a -> 'b
   val source': string -> (string -> 'a -> 'b list * 'a) -> ('b list * 'a -> 'c) ->
     'b * ('b -> bool) -> ('d * 'b list -> 'e list * ('d * 'b list)) ->
-    (string -> 'd * 'b list -> 'e list * ('d * 'b list)) option -> 'd * 'a -> 'e list * ('d * 'c)
+    (bool * (string -> 'd * 'b list -> 'e list * ('d * 'b list))) option ->
+    'd * 'a -> 'e list * ('d * 'c)
   val source: string -> (string -> 'a -> 'b list * 'a) -> ('b list * 'a -> 'c) ->
     'b * ('b -> bool) -> ('b list -> 'd list * 'b list) ->
-    (string -> 'b list -> 'd list * 'b list) option -> 'a -> 'd list * 'c
+    (bool * (string -> 'b list -> 'd list * 'b list)) option -> 'a -> 'd list * 'c
   val single: ('a -> 'b * 'a) -> 'a -> 'b list * 'a
   val bulk: ('a -> 'b * 'a) -> 'a -> 'b list * 'a
   type lexicon
@@ -252,21 +253,23 @@
 fun source' def_prmpt get unget stopper scanner opt_recover (state, src) =
   let
     val drain_with = drain def_prmpt get stopper;
-
-    fun drain_loop recover inp =
-      drain_with (catch scanner) inp handle FAIL msg =>
-        (drain_with (recover (the_default "Syntax error." msg)) inp);
-
     val ((ys, (state', xs')), src') =
       (case (get def_prmpt src, opt_recover) of
         (([], s), _) => (([], (state, [])), s)
       | ((xs, s), NONE) => drain_with (error scanner) ((state, xs), s)
-      | ((xs, s), SOME r) => drain_loop (unless (lift (one (#2 stopper))) o r) ((state, xs), s));
+      | ((xs, s), SOME (interactive, recover)) =>
+          let val inp = ((state, xs), s) in
+            drain_with (catch scanner) inp handle FAIL msg =>
+              let val err = the_default "Syntax error." msg in
+                if interactive then Output.error_msg err else ();
+                drain_with (unless (lift (one (#2 stopper))) (recover err)) inp
+              end
+          end);
   in (ys, (state', unget (xs', src'))) end;
 
 fun source def_prmpt get unget stopper scan opt_recover =
   unlift (source' def_prmpt get unget stopper (lift scan)
-    (Option.map (fn r => lift o r) opt_recover));
+    (Option.map (fn (int, r) => (int, lift o r)) opt_recover));
 
 fun single scan = scan >> (fn x => [x]);
 fun bulk scan = scan -- repeat (permissive scan) >> (op ::);

--- a/src/Pure/General/source.ML	Mon Jul 09 23:12:51 2007 +0200
+++ b/src/Pure/General/source.ML	Tue Jul 10 00:17:52 2007 +0200
@@ -22,10 +22,10 @@
   val of_stream: TextIO.instream -> TextIO.outstream -> (string, unit) source
   val tty: (string, unit) source
   val source': 'a -> 'b * ('b -> bool) -> ('a * 'b list -> 'c list * ('a * 'b list)) ->
-    (string -> 'a * 'b list -> 'c list * ('a * 'b list)) option ->
+    (bool * (string -> 'a * 'b list -> 'c list * ('a * 'b list))) option ->
     ('b, 'e) source -> ('c, 'a * ('b, 'e) source) source
   val source: 'a * ('a -> bool) -> ('a list -> 'b list * 'a list) ->
-    (string -> 'a list -> 'b list * 'a list) option ->
+    (bool * (string -> 'a list -> 'b list * 'a list)) option ->
     ('a, 'd) source -> ('b, ('a, 'd) source) source
 end;
 

--- a/src/Pure/General/symbol.ML	Mon Jul 09 23:12:51 2007 +0200
+++ b/src/Pure/General/symbol.ML	Tue Jul 10 00:17:52 2007 +0200
@@ -428,7 +428,8 @@
 in
 
 fun source do_recover src =
-  Source.source stopper (Scan.bulk scan) (if do_recover then SOME (K recover) else NONE) src;
+  Source.source stopper (Scan.bulk scan)
+    (if do_recover then SOME (false, K recover) else NONE) src;
 
 end;
 

--- a/src/Pure/Isar/outer_lex.ML	Mon Jul 09 23:12:51 2007 +0200
+++ b/src/Pure/Isar/outer_lex.ML	Tue Jul 10 00:17:52 2007 +0200
@@ -322,16 +322,14 @@
 
 val is_junk = (not o Symbol.is_blank) andf Symbol.not_sync andf Symbol.not_eof;
 
-fun recover interactive msg x =
-  (if interactive then Output.error_msg msg else ();
-    (Scan.state :-- (fn pos => keep_line (Scan.many is_junk)
-      >> (fn xs => [Token (pos, (Malformed msg, implode xs))])) >> #2) x);
+fun recover msg = Scan.state :-- (fn pos =>
+  keep_line (Scan.many is_junk) >> (fn xs => [Token (pos, (Malformed msg, implode xs))])) >> #2;
 
 in
 
 fun source do_recover get_lex pos src =
   Source.source' pos Symbol.stopper (Scan.bulk (fn xs => scan (get_lex ()) xs))
-    (Option.map recover do_recover) src;
+    (Option.map (rpair recover) do_recover) src;
 
 end;
 

--- a/src/Pure/Isar/outer_syntax.ML	Mon Jul 09 23:12:51 2007 +0200
+++ b/src/Pure/Isar/outer_syntax.ML	Tue Jul 10 00:17:52 2007 +0200
@@ -192,18 +192,17 @@
   let
     val no_terminator =
       Scan.unless P.semicolon (Scan.one (T.not_sync andf T.not_eof));
-    fun recover interactive msg x =
-      (if interactive then Output.error_msg msg else ();
-        (Scan.prompt "recover# " (Scan.repeat no_terminator) >> K [NONE]) x);
+    fun recover int =
+      (int, fn _ => Scan.prompt "recover# " (Scan.repeat no_terminator) >> K [NONE]);
   in
     src
     |> T.source_proper
     |> Source.source T.stopper
       (Scan.bulk (P.$$$ "--" -- P.!!! P.text >> K NONE || P.not_eof >> SOME))
-      (Option.map recover do_recover)
+        (Option.map recover do_recover)
     |> Source.map_filter I
     |> Source.source T.stopper (Scan.bulk (fn xs => P.!!! (command term do_trace (cmd ())) xs))
-      (Option.map recover do_recover)
+        (Option.map recover do_recover)
     |> Source.map_filter I
   end;