Allow scanning to recover and reconstruct bad input

--- a/src/Pure/Isar/outer_lex.ML	Fri Oct 01 11:54:15 2004 +0200
+++ b/src/Pure/Isar/outer_lex.ML	Fri Oct 01 11:55:43 2004 +0200
@@ -83,6 +83,7 @@
   | not_sync _ = true;
 
 val malformed = Token (Position.none, (Malformed, ""));
+fun malformed_of xs = Token (Position.none, (Malformed, implode xs));
 
 
 (* eof token *)
@@ -277,7 +278,7 @@
 (* token sources *)
 
 val is_junk = (not o Symbol.is_blank) andf Symbol.not_sync andf Symbol.not_eof;
-fun recover xs = (keep_line (Scan.any is_junk) >> K [malformed]) xs;
+fun recover xs = (keep_line (Scan.any is_junk) >> (fn ts => [malformed_of ts])) xs;
 
 fun source do_recover get_lex pos src =
   Source.source' pos Symbol.stopper (Scan.bulk (fn xs => scan (get_lex ()) xs))

--- a/src/Pure/Isar/outer_syntax.ML	Fri Oct 01 11:54:15 2004 +0200
+++ b/src/Pure/Isar/outer_syntax.ML	Fri Oct 01 11:55:43 2004 +0200
@@ -61,12 +61,12 @@
   val deps_thy: string -> bool -> Path.T -> string list * Path.T list
   val load_thy: string -> bool -> bool -> Path.T -> unit
   val isar: bool -> bool -> unit Toplevel.isar
-  val scan: string -> OuterLex.token list
+  val scan: string -> OuterLex.token list  
   val read: OuterLex.token list -> 
 		(string * OuterLex.token list * Toplevel.transition) list
 end;
 
-structure OuterSyntax: OUTER_SYNTAX =
+structure OuterSyntax : OUTER_SYNTAX  =
 struct
 
 structure T = OuterLex;
@@ -270,7 +270,7 @@
 fun scan str =
  Source.of_string str
  |> Symbol.source false
- |> T.source false get_lexicons Position.none
+ |> T.source true get_lexicons Position.none
  |> Source.exhaust
 
 fun read toks =