src/Pure/General/symbol.ML
changeset 25644 d30391cdd9d9
parent 25641 615aecd485ad
child 26524 63953bec4c98
equal deleted inserted replaced
25643:2fdb26d45184 25644:d30391cdd9d9
   424     !! (fn (cs, _) => malformed_msg (beginning 10 ("\\" :: "<" :: cs)))
   424     !! (fn (cs, _) => malformed_msg (beginning 10 ("\\" :: "<" :: cs)))
   425       (($$ "^" ^^ (scan_raw || scan_id) || scan_id) ^^ $$ ">")) ||
   425       (($$ "^" ^^ (scan_raw || scan_id) || scan_id) ^^ $$ ">")) ||
   426   Scan.one not_eof;
   426   Scan.one not_eof;
   427 
   427 
   428 val recover =
   428 val recover =
   429   Scan.many (fn s => not (is_blank s) andalso s <> "\"" andalso not_eof s)
   429   Scan.many (fn s => not (is_blank s) andalso s <> "\"" andalso s <> "`" andalso not_eof s)
   430     >> (fn ss => malformed :: ss @ [end_malformed]);
   430     >> (fn ss => malformed :: ss @ [end_malformed]);
   431 
   431 
   432 in
   432 in
   433 
   433 
   434 fun source do_recover src =
   434 fun source do_recover src =