# HG changeset patch
# User wenzelm
# Date 1418230531 -3600
# Node ID ff0703716c516e344537a46353001f80890d414c
# Parent  ee19c92ae8b4d5931415d945450d0969be2d34c0
more markup for improper situations;

diff -r ee19c92ae8b4 -r ff0703716c51 src/Pure/Isar/calculation.ML
--- a/src/Pure/Isar/calculation.ML	Wed Dec 10 13:45:44 2014 +0100
+++ b/src/Pure/Isar/calculation.ML	Wed Dec 10 17:55:31 2014 +0100
@@ -111,7 +111,13 @@
 (** proof commands **)
 
 fun assert_sane final =
-  if final then Proof.assert_forward else Proof.assert_forward_or_chain;
+  if final then Proof.assert_forward
+  else
+    Proof.assert_forward_or_chain #>
+    tap (fn state =>
+      if can Proof.assert_chain state then
+        Context_Position.report (Proof.context_of state) (Position.thread_data ()) Markup.improper
+      else ());
 
 fun maintain_calculation int final calc state =
   let