Allow scanning to recover and reconstruct bad input
authoraspinall
Fri Oct 01 11:55:43 2004 +0200 (2004-10-01)
changeset 152241bd35fd87963
parent 15223 e669fb5b0f5a
child 15225 68ab0f4eb457
Allow scanning to recover and reconstruct bad input
src/Pure/Isar/outer_lex.ML
src/Pure/Isar/outer_syntax.ML
     1.1 --- a/src/Pure/Isar/outer_lex.ML	Fri Oct 01 11:54:15 2004 +0200
     1.2 +++ b/src/Pure/Isar/outer_lex.ML	Fri Oct 01 11:55:43 2004 +0200
     1.3 @@ -83,6 +83,7 @@
     1.4    | not_sync _ = true;
     1.5  
     1.6  val malformed = Token (Position.none, (Malformed, ""));
     1.7 +fun malformed_of xs = Token (Position.none, (Malformed, implode xs));
     1.8  
     1.9  
    1.10  (* eof token *)
    1.11 @@ -277,7 +278,7 @@
    1.12  (* token sources *)
    1.13  
    1.14  val is_junk = (not o Symbol.is_blank) andf Symbol.not_sync andf Symbol.not_eof;
    1.15 -fun recover xs = (keep_line (Scan.any is_junk) >> K [malformed]) xs;
    1.16 +fun recover xs = (keep_line (Scan.any is_junk) >> (fn ts => [malformed_of ts])) xs;
    1.17  
    1.18  fun source do_recover get_lex pos src =
    1.19    Source.source' pos Symbol.stopper (Scan.bulk (fn xs => scan (get_lex ()) xs))
     2.1 --- a/src/Pure/Isar/outer_syntax.ML	Fri Oct 01 11:54:15 2004 +0200
     2.2 +++ b/src/Pure/Isar/outer_syntax.ML	Fri Oct 01 11:55:43 2004 +0200
     2.3 @@ -61,12 +61,12 @@
     2.4    val deps_thy: string -> bool -> Path.T -> string list * Path.T list
     2.5    val load_thy: string -> bool -> bool -> Path.T -> unit
     2.6    val isar: bool -> bool -> unit Toplevel.isar
     2.7 -  val scan: string -> OuterLex.token list
     2.8 +  val scan: string -> OuterLex.token list  
     2.9    val read: OuterLex.token list -> 
    2.10  		(string * OuterLex.token list * Toplevel.transition) list
    2.11  end;
    2.12  
    2.13 -structure OuterSyntax: OUTER_SYNTAX =
    2.14 +structure OuterSyntax : OUTER_SYNTAX  =
    2.15  struct
    2.16  
    2.17  structure T = OuterLex;
    2.18 @@ -270,7 +270,7 @@
    2.19  fun scan str =
    2.20   Source.of_string str
    2.21   |> Symbol.source false
    2.22 - |> T.source false get_lexicons Position.none
    2.23 + |> T.source true get_lexicons Position.none
    2.24   |> Source.exhaust
    2.25  
    2.26  fun read toks =