# HG changeset patch
# User wenzelm
# Date 1469178070 -7200
# Node ID e308f15cc8a7205a381e781f7295263a1ab0ff37
# Parent  f8652d0534fa80ba6204c67bb7cf6b9cb2910d85
more markup for unstructured calculation;

diff -r f8652d0534fa -r e308f15cc8a7 src/Pure/Isar/calculation.ML
--- a/src/Pure/Isar/calculation.ML	Fri Jul 22 11:00:43 2016 +0200
+++ b/src/Pure/Isar/calculation.ML	Fri Jul 22 11:01:10 2016 +0200
@@ -122,7 +122,9 @@
 
 fun maintain_calculation int final calc state =
   let
-    val state' = put_calculation (SOME calc) state;
+    val state' = state
+      |> put_calculation (SOME calc)
+      |> Proof.improper_reset_facts;
     val ctxt' = Proof.context_of state';
     val _ =
       if int then
diff -r f8652d0534fa -r e308f15cc8a7 src/Pure/Isar/proof.ML
--- a/src/Pure/Isar/proof.ML	Fri Jul 22 11:00:43 2016 +0200
+++ b/src/Pure/Isar/proof.ML	Fri Jul 22 11:01:10 2016 +0200
@@ -19,10 +19,12 @@
   val map_context_result : (context -> 'a * context) -> state -> 'a * state
   val map_contexts: (context -> context) -> state -> state
   val propagate_ml_env: state -> state
+  val report_improper: state -> unit
   val the_facts: state -> thm list
   val the_fact: state -> thm
   val set_facts: thm list -> state -> state
   val reset_facts: state -> state
+  val improper_reset_facts: state -> state
   val assert_forward: state -> state
   val assert_chain: state -> state
   val assert_forward_or_chain: state -> state
@@ -163,7 +165,7 @@
 and node =
   Node of
    {context: context,
-    facts: thm list option,
+    facts: (thm list * bool) option,
     mode: mode,
     goal: goal option}
 and goal =
@@ -242,11 +244,14 @@
 
 (* facts *)
 
+fun report_improper state =
+  Context_Position.report (context_of state) (Position.thread_data ()) Markup.improper;
+
 val get_facts = #facts o top;
 
 fun the_facts state =
   (case get_facts state of
-    SOME facts => facts
+    SOME (facts, proper) => (if proper then () else report_improper state; facts)
   | NONE => error "No current facts available");
 
 fun the_fact state =
@@ -256,10 +261,15 @@
 
 fun put_facts index facts =
   map_top (fn (ctxt, _, mode, goal) => (ctxt, facts, mode, goal)) #>
-  map_context (Proof_Context.put_thms index (Auto_Bind.thisN, facts));
+  map_context (Proof_Context.put_thms index (Auto_Bind.thisN, Option.map #1 facts));
+
+fun set_facts thms = put_facts false (SOME (thms, true));
+val reset_facts = put_facts false NONE;
 
-val set_facts = put_facts false o SOME;
-val reset_facts = put_facts false NONE;
+fun improper_reset_facts state =
+  (case get_facts state of
+    SOME (thms, _) => put_facts false (SOME (thms, false)) state
+  | NONE => state);
 
 fun these_factss more_facts (named_factss, state) =
   (named_factss, state |> set_facts (maps snd named_factss @ more_facts));
@@ -267,10 +277,9 @@
 fun export_facts inner outer =
   (case get_facts inner of
     NONE => reset_facts outer
-  | SOME thms =>
-      thms
-      |> Proof_Context.export (context_of inner) (context_of outer)
-      |> (fn ths => put_facts true (SOME ths) outer));
+  | SOME (thms, proper) =>
+      let val thms' = Proof_Context.export (context_of inner) (context_of outer) thms
+      in put_facts true (SOME (thms', proper)) outer end);
 
 
 (* mode *)
@@ -403,8 +412,8 @@
       [Pretty.mark_str (position_markup, "proof"), Pretty.str (" (" ^ mode_name mode ^ ")")]] @
     (if null prt_ctxt then [] else prt_ctxt @ [Pretty.str ""]) @
     (if verbose orelse mode = Forward then
-       pretty_sep (pretty_facts ctxt "" facts) (prt_goal (try find_goal state))
-     else if mode = Chain then pretty_facts ctxt "picking" facts
+       pretty_sep (pretty_facts ctxt "" (Option.map #1 facts)) (prt_goal (try find_goal state))
+     else if mode = Chain then pretty_facts ctxt "picking" (Option.map #1 facts)
      else prt_goal (try find_goal state))
   end;