Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
more markup for improper situations;
authorwenzelm
Wed, 10 Dec 2014 17:55:31 +0100
changeset 59126 ff0703716c51
parent 59125 ee19c92ae8b4
child 59127 723b11f8ffbf
more markup for improper situations;
src/Pure/Isar/calculation.ML file | annotate | diff | comparison | revisions 
--- 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
isabelle