# HG changeset patch # User aspinall # Date 1096624543 -7200 # Node ID 1bd35fd87963cd399efb65bfbc4638ee97c0af67 # Parent e669fb5b0f5aa6578b83897fab92a0eb2e46caab Allow scanning to recover and reconstruct bad input diff -r e669fb5b0f5a -r 1bd35fd87963 src/Pure/Isar/outer_lex.ML --- 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)) diff -r e669fb5b0f5a -r 1bd35fd87963 src/Pure/Isar/outer_syntax.ML --- 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 =