src/Pure/Isar/outer_lex.ML

 
 signature OUTER_LEX =
 sig
   datatype token_kind =
     Command | Keyword | Ident | LongIdent | SymIdent | Var | TypeIdent | TypeVar |
-    Nat | String | Verbatim | Space | Comment | Sync | EOF
+    Nat | String | Verbatim | Space | Comment | Sync | Malformed | EOF
   type token
   val str_of_kind: token_kind -> string
   val stopper: token * (token -> bool)
   val not_sync: token -> bool
   val not_eof: token -> bool

 
 (* datatype token *)
 
 datatype token_kind =
   Command | Keyword | Ident | LongIdent | SymIdent | Var | TypeIdent | TypeVar |
-  Nat | String | Verbatim | Space | Comment | Sync | EOF;
+  Nat | String | Verbatim | Space | Comment | Sync | Malformed | EOF;
 
 datatype token = Token of Position.T * (token_kind * string);
 
 val str_of_kind =
  fn Command => "command"

   | String => "string"
   | Verbatim => "verbatim text"
   | Space => "white space"
   | Comment => "comment text"
   | Sync => "sync marker"
+  | Malformed => "bad input"
   | EOF => "end-of-file";
 
 
-(* sync token *)
+(* control tokens *)
 
 fun not_sync (Token (_, (Sync, _))) = false
   | not_sync _ = true;
+
+val malformed = Token (Position.none, (Malformed, ""));
 
 
 (* eof token *)
 
 val eof = Token (Position.none, (EOF, ""));

 
 
 (* name and value of token *)
 
 fun name_of (tok as Token (_, (k, x))) =
-  if is_semicolon tok then "terminator" else str_of_kind k ^ " " ^ quote x;
+  if is_semicolon tok then "terminator"
+  else if x = "" then str_of_kind k
+  else str_of_kind k ^ " " ^ quote x;
 
 fun val_of (Token (_, (_, x))) = x;
 
 fun token_leq (Token (_, (_, x)), Token (_, (_, x'))) = x <= x';
 

 
 
 (* 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) xs;
+fun recover xs = (keep_line (Scan.any is_junk) >> K [malformed]) xs;
 
 fun source do_recover get_lex pos src =
   Source.source' pos Symbol.stopper (Scan.bulk (fn xs => scan (get_lex ()) xs))
     (if do_recover then Some recover else None) src;