diff --git a/src_ext/l4v/src/tools/c-parser/Feedback.ML b/src_ext/l4v/src/tools/c-parser/Feedback.ML
index 553e37b685a2beb1040a11151e9ea1efc3beae5c..23cf17818d8f16fd77a461f4a07232da83b02de3 100644
--- a/src_ext/l4v/src/tools/c-parser/Feedback.ML
+++ b/src_ext/l4v/src/tools/c-parser/Feedback.ML
@@ -13,6 +13,9 @@ signature FEEDBACK =
 sig
 
   exception WantToExit of string
+
+  val msg_c99 : string
+
   val numErrors : int Unsynchronized.ref
   val errorThreshold : int option Unsynchronized.ref
   val errorStr : Region.t * string -> unit
@@ -35,6 +38,9 @@ structure Feedback :> FEEDBACK =
 struct
 open Unsynchronized
 exception WantToExit of string
+
+val msg_c99 = "C99 parser"
+
 val isSome = Option.isSome
 
 val numErrors = ref 0
diff --git a/src_ext/l4v/src/tools/c-parser/StrictCParser.ML b/src_ext/l4v/src/tools/c-parser/StrictCParser.ML
index b8dafec53a9660c023847d7edf6af5d2613e8ecc..dd9c81f494801288358d0efd5eccd995cc4a4f62 100644
--- a/src_ext/l4v/src/tools/c-parser/StrictCParser.ML
+++ b/src_ext/l4v/src/tools/c-parser/StrictCParser.ML
@@ -63,7 +63,7 @@ fun parse maybe_c11 docpp0 error_lookahead (includes : string list) (input : inp
        | (_, Source src) =>
           f (drain [Input.source_content src |> #1]) (C_Env.encode_positions [Input.pos_of src])
 
-    fun parse_without_c11 thy = 
+    fun parse_without_c11 exit_err thy = 
       docpp
         (open_close (fn istream => fn fname =>
           let
@@ -71,8 +71,14 @@ fun parse maybe_c11 docpp0 error_lookahead (includes : string list) (input : inp
             val lexarg = StrictCLex.UserDeclarations.new_state fname
             val lexer = StrictCParser.makeLexer istream lexarg
             val pos = #source lexarg
+            fun err e =
+              tap (fn _ => 
+                    (writeln (Markup.markup (Markup.bad ()) (Feedback.msg_c99 ^ ": " ^ "returning a default empty parsed value"));
+                     exit_err (Feedback.msg_c99 ^ ": " ^ @{make_string} e ^ Position.here \<^here>)))
+                  ([], !Feedback.numErrors)
           in (invoke error_lookahead pos lexer
-                handle StrictCParser.ParseError => ([], !Feedback.numErrors))
+                handle e as StrictCParser.ParseError => err e
+                     | e as Feedback.WantToExit _ => err e)
              |>> pair fname
           end))
       |>> (fn (fname, v) => Synchronized.change_result last_parsed (K (v, (fname, v))))
@@ -119,7 +125,7 @@ fun parse maybe_c11 docpp0 error_lookahead (includes : string list) (input : inp
     case maybe_c11 of
       SOME true => 
         let val ((res2, err2), thy) = parse_with_c11 thy
-            val ((res1, err1), thy) = parse_without_c11 thy
+            val ((res1, err1), thy) = parse_without_c11 warning thy
             val rm = StmtDecl.rm_region_ext_decl_list
             val r1 = rm res1
             val r2 = rm res2
@@ -134,7 +140,7 @@ fun parse maybe_c11 docpp0 error_lookahead (includes : string list) (input : inp
                         r1 r2 (0, true))
            then ((res1, err1 + err2), thy)
            else error "Parsed values are not similar." end
-    | SOME false => parse_without_c11 thy
+    | SOME false => parse_without_c11 error thy
     | _ => parse_with_c11 thy
   end
 
diff --git a/src_ext/l4v/src/tools/c-parser/isar_install.ML b/src_ext/l4v/src/tools/c-parser/isar_install.ML
index 8200f1bd99ffd8b0b632b47426a25c8e40b3201e..3c4be8ced25f15039d541e72d881836d52f39b98 100644
--- a/src_ext/l4v/src/tools/c-parser/isar_install.ML
+++ b/src_ext/l4v/src/tools/c-parser/isar_install.ML
@@ -55,7 +55,7 @@ fun setup_feedback extra_output_filename = let
         NONE => (fn _ => fn f => f)
       | SOME _ => (fn pfx => fn f => fn s => (trace_extra (pfx ^ s); f s))
   in
-    Feedback.errorf := add_extra "ERROR: " (writeln o Markup.markup (Markup.bad ()));
+    Feedback.errorf := add_extra "ERROR: " (writeln o Markup.markup (Markup.bad ()) o (fn s => Feedback.msg_c99 ^ ": " ^ s));
     Feedback.warnf := add_extra "" warning;
     Feedback.informf := add_extra "" (Output.tracing o Feedback.timestamp)
   end