diff --git a/src/emit/selftest.sml b/src/emit/selftest.sml index 6beae77c69..d853928e7c 100644 --- a/src/emit/selftest.sml +++ b/src/emit/selftest.sml @@ -1,9 +1,19 @@ +open HolKernel bossLib testutils local open basis_emitTheory in end val (is_con, thy, name, ty) = ConstMapML.apply ``bool$IN`` -fun die s = (print (s^"\n"); OS.Process.exit OS.Process.failure) - -fun tprint s = print (StringCvt.padRight #" " 65 s) val _ = tprint "Testing ConstMapML information for bool$IN" val _ = if thy <> "set" then die "FAILED!" else print "OK\n" + +fun gh157() = let + val gh157a_def = Define`gh157a = T` + val gh157b_def = Define`gh157b = ~gh157a`; + val _ = tprint "Emit should fail on missing def'n" +in + (with_flag (Feedback.emit_WARNING, false) (EmitML.eSML "bug") [EmitML.DEFN gh157b_def]; + die "FAILED!") + handle HOL_ERR _ => print "OK\n" +end + +val _ = trace ("Define.storage_message", 0) gh157 ()