Self-test illustrating bug from github issue #157

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 ()