# HG changeset patch
# User wenzelm
# Date 949092962 -3600
# Node ID 651b006d7eb8897e24402e76d27f2e006e457a6d
# Parent  27f14e47e2d5f8d66920198b5b6c19dd2072dbc1
added defer, prefer;

diff -r 27f14e47e2d5 -r 651b006d7eb8 src/Pure/Isar/isar_syn.ML
--- a/src/Pure/Isar/isar_syn.ML	Fri Jan 28 21:55:43 2000 +0100
+++ b/src/Pure/Isar/isar_syn.ML	Fri Jan 28 21:56:02 2000 +0100
@@ -381,6 +381,14 @@
 
 (* proof steps *)
 
+val deferP =
+  OuterSyntax.improper_command "defer" "shuffle internal proof state"
+    K.prf_script (Scan.option P.nat >> (Toplevel.print oo (Toplevel.proof o IsarThy.defer)));
+
+val preferP =
+  OuterSyntax.improper_command "prefer" "shuffle internal proof state"
+    K.prf_script (P.nat >> (Toplevel.print oo (Toplevel.proof o IsarThy.prefer)));
+
 val applyP =
   OuterSyntax.improper_command "apply" "unstructured backward proof step, ignoring facts"
     K.prf_script (P.method >> (Toplevel.print oo (Toplevel.proof o IsarThy.tac)));
@@ -616,8 +624,9 @@
   theoremP, lemmaP, showP, haveP, thusP, henceP, assumeP, presumeP,
   defP, fixP, letP, thenP, thenceP, fromP, withP, noteP, beginP, endP,
   nextP, qedP, terminal_proofP, immediate_proofP, default_proofP,
-  skip_proofP, applyP, then_applyP, proofP, alsoP, finallyP, backP,
-  cannot_undoP, clear_undosP, redoP, undos_proofP, kill_proofP, undoP,
+  skip_proofP, deferP, preferP, applyP, then_applyP, proofP, alsoP,
+  finallyP, backP, cannot_undoP, clear_undosP, redoP, undos_proofP,
+  kill_proofP, undoP,
   (*diagnostic commands*)
   pretty_setmarginP, print_commandsP, print_contextP, print_theoryP,
   print_syntaxP, print_theoremsP, print_attributesP, print_methodsP,
diff -r 27f14e47e2d5 -r 651b006d7eb8 src/Pure/Isar/isar_thy.ML
--- a/src/Pure/Isar/isar_thy.ML	Fri Jan 28 21:55:43 2000 +0100
+++ b/src/Pure/Isar/isar_thy.ML	Fri Jan 28 21:56:02 2000 +0100
@@ -116,6 +116,8 @@
   val begin_block: ProofHistory.T -> ProofHistory.T
   val next_block: ProofHistory.T -> ProofHistory.T
   val end_block: ProofHistory.T -> ProofHistory.T
+  val defer: int option -> ProofHistory.T -> ProofHistory.T
+  val prefer: int -> ProofHistory.T -> ProofHistory.T
   val tac: Method.text -> ProofHistory.T -> ProofHistory.T
   val then_tac: Method.text -> ProofHistory.T -> ProofHistory.T
   val proof: (Comment.interest * (Method.text * Comment.interest) option) * Comment.text
@@ -342,6 +344,12 @@
 val end_block = ProofHistory.applys Proof.end_block;
 
 
+(* shuffle state *)
+
+fun defer i = ProofHistory.applys (Method.refine (Method.Basic (K (Method.defer i))));
+fun prefer i = ProofHistory.applys (Method.refine (Method.Basic (K (Method.prefer i))));
+
+
 (* backward steps *)
 
 val tac = ProofHistory.applys o Method.refine_no_facts;