apply etc.: comments;

--- a/src/Pure/Isar/isar_syn.ML	Thu Apr 06 19:11:30 2000 +0200
+++ b/src/Pure/Isar/isar_syn.ML	Fri Apr 07 17:36:25 2000 +0200
@@ -387,20 +387,20 @@
 (* proof steps *)
 
 val deferP =
-  OuterSyntax.command "defer" "shuffle internal proof state"
-    K.prf_script (Scan.option P.nat >> (Toplevel.print oo (Toplevel.proof o IsarThy.defer)));
+  OuterSyntax.command "defer" "shuffle internal proof state" K.prf_script
+    (Scan.option P.nat -- P.marg_comment >> (Toplevel.print oo (Toplevel.proof o IsarThy.defer)));
 
 val preferP =
-  OuterSyntax.command "prefer" "shuffle internal proof state"
-    K.prf_script (P.nat >> (Toplevel.print oo (Toplevel.proof o IsarThy.prefer)));
+  OuterSyntax.command "prefer" "shuffle internal proof state" K.prf_script
+    (P.nat -- P.marg_comment >> (Toplevel.print oo (Toplevel.proof o IsarThy.prefer)));
 
 val applyP =
-  OuterSyntax.command "apply" "initial refinement step (unstructured)"
-    K.prf_script (P.method >> (Toplevel.print oo (Toplevel.proof o IsarThy.apply)));
+  OuterSyntax.command "apply" "initial refinement step (unstructured)" K.prf_script
+    (P.method -- P.marg_comment >> (Toplevel.print oo (Toplevel.proof o IsarThy.apply)));
 
 val apply_endP =
-  OuterSyntax.command "apply_end" "terminal refinement (unstructured)"
-    K.prf_script (P.method >> (Toplevel.print oo (Toplevel.proof o IsarThy.apply_end)));
+  OuterSyntax.command "apply_end" "terminal refinement (unstructured)" K.prf_script
+    (P.method -- P.marg_comment >> (Toplevel.print oo (Toplevel.proof o IsarThy.apply_end)));
 
 val proofP =
   OuterSyntax.command "proof" "backward proof" K.prf_block

--- a/src/Pure/Isar/isar_thy.ML	Thu Apr 06 19:11:30 2000 +0200
+++ b/src/Pure/Isar/isar_thy.ML	Fri Apr 07 17:36:25 2000 +0200
@@ -120,10 +120,10 @@
   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 apply: Method.text -> ProofHistory.T -> ProofHistory.T
-  val apply_end: Method.text -> ProofHistory.T -> ProofHistory.T
+  val defer: int option * Comment.text -> ProofHistory.T -> ProofHistory.T
+  val prefer: int * Comment.text -> ProofHistory.T -> ProofHistory.T
+  val apply: Method.text * Comment.text -> ProofHistory.T -> ProofHistory.T
+  val apply_end: Method.text * Comment.text -> ProofHistory.T -> ProofHistory.T
   val proof: (Comment.interest * (Method.text * Comment.interest) option) * Comment.text
     -> ProofHistory.T -> ProofHistory.T
   val qed: (Method.text * Comment.interest) option * Comment.text
@@ -355,14 +355,15 @@
 
 fun shuffle meth i = Method.refine (Method.Basic (K (meth i))) o Proof.assert_no_chain;
 
-fun defer i = ProofHistory.applys (shuffle Method.defer i);
-fun prefer i = ProofHistory.applys (shuffle Method.prefer i);
+fun defer (i, comment_ignore) = ProofHistory.applys (shuffle Method.defer i);
+fun prefer (i, comment_ignore) = ProofHistory.applys (shuffle Method.prefer i);
 
 
 (* backward steps *)
 
-fun apply m = ProofHistory.applys (Method.refine m o Proof.assert_backward);
-fun apply_end m = ProofHistory.applys (Method.refine_end m o Proof.assert_forward);
+fun apply (m, comment_ignore) = ProofHistory.applys (Method.refine m o Proof.assert_backward);
+fun apply_end (m, comment_ignore) =
+  ProofHistory.applys (Method.refine_end m o Proof.assert_forward);
 
 val proof = ProofHistory.applys o Method.proof o
   apsome Comment.ignore_interest o Comment.ignore_interest' o Comment.ignore;