# HG changeset patch
# User wenzelm
# Date 927279537 -7200
# Node ID b7293047b0f49da08c0ce8e86f2327d68eba8fc8
# Parent  0c6c668c685f6770737ad27069bf1229ad731342
local_qed: obtain interactive flag;

diff -r 0c6c668c685f -r b7293047b0f4 src/Pure/Isar/method.ML
--- a/src/Pure/Isar/method.ML	Fri May 21 11:38:23 1999 +0200
+++ b/src/Pure/Isar/method.ML	Fri May 21 11:38:57 1999 +0200
@@ -55,10 +55,10 @@
   val tac: text -> Proof.state -> Proof.state Seq.seq
   val then_tac: text -> Proof.state -> Proof.state Seq.seq
   val proof: text option -> Proof.state -> Proof.state Seq.seq
-  val local_qed: text option -> Proof.state -> Proof.state Seq.seq
-  val local_terminal_proof: text -> Proof.state -> Proof.state Seq.seq
-  val local_immediate_proof: Proof.state -> Proof.state Seq.seq
-  val local_default_proof: Proof.state -> Proof.state Seq.seq
+  val local_qed: text option -> bool -> Proof.state -> Proof.state Seq.seq
+  val local_terminal_proof: text -> bool -> Proof.state -> Proof.state Seq.seq
+  val local_immediate_proof: bool -> Proof.state -> Proof.state Seq.seq
+  val local_default_proof: bool -> Proof.state -> Proof.state Seq.seq
   val global_qed: bstring option -> theory attribute list option -> text option
     -> Proof.state -> theory * {kind: string, name: string, thm: thm}
   val global_terminal_proof: text -> Proof.state -> theory * {kind: string, name: string, thm: thm}
@@ -301,7 +301,7 @@
   |> Seq.map Proof.enter_forward;
 
 fun local_qed opt_text = Proof.local_qed (refine (if_none opt_text finish_text));
-fun local_terminal_proof text = Seq.THEN (proof (Some text), local_qed None);
+fun local_terminal_proof text int = Seq.THEN (proof (Some text), local_qed None int);
 val local_immediate_proof = local_terminal_proof (Basic (K same));
 val local_default_proof = local_terminal_proof default_text;
 
diff -r 0c6c668c685f -r b7293047b0f4 src/Pure/Isar/proof.ML
--- a/src/Pure/Isar/proof.ML	Fri May 21 11:38:23 1999 +0200
+++ b/src/Pure/Isar/proof.ML	Fri May 21 11:38:57 1999 +0200
@@ -58,7 +58,7 @@
   val next_block: state -> state
   val end_block: state -> state
   val at_bottom: state -> bool
-  val local_qed: (state -> state Seq.seq) -> state -> state Seq.seq
+  val local_qed: (state -> state Seq.seq) -> bool -> state -> state Seq.seq
   val global_qed: (state -> state Seq.seq) -> bstring option
     -> theory attribute list option -> state -> theory * {kind: string, name: string, thm: thm}
 end;
@@ -624,7 +624,7 @@
     |> opt_solve
   end;
 
-fun local_qed finalize state =
+fun local_qed finalize int state =	(* FIXME handle int *)
   state
   |> finish_proof false finalize
   |> (Seq.flat o Seq.map finish_local);