# HG changeset patch # User blanchet # Date 1344693258 -7200 # Node ID 553ad5f999688fb6319c80fcb790c02fc5798763 # Parent fb1ed5230abcbf4ec87b52e122e91021065cfbd1 fixed "double rev" bug that arose in situations where a % comment arose on the last line of a file without \n at the end diff -r fb1ed5230abc -r 553ad5f99968 src/HOL/Tools/ATP/atp_util.ML --- a/src/HOL/Tools/ATP/atp_util.ML Sat Aug 11 11:31:05 2012 +0200 +++ b/src/HOL/Tools/ATP/atp_util.ML Sat Aug 11 15:54:18 2012 +0200 @@ -82,7 +82,7 @@ | strip_c_style_comment (#"*" :: #"/" :: cs) accum = strip_spaces_in_list true cs accum | strip_c_style_comment (_ :: cs) accum = strip_c_style_comment cs accum - and strip_spaces_in_list _ [] accum = rev accum + and strip_spaces_in_list _ [] accum = accum | strip_spaces_in_list true (#"%" :: cs) accum = strip_spaces_in_list true (cs |> chop_while (not_equal #"\n") |> snd) accum