block commands: marginal comment;

--- a/src/Pure/Isar/isar_syn.ML	Sat Jun 03 23:58:37 2000 +0200
+++ b/src/Pure/Isar/isar_syn.ML	Sat Jun 03 23:59:37 2000 +0200
@@ -349,15 +349,15 @@
 
 val beginP =
   OuterSyntax.command "{" "begin explicit proof block" K.prf_block
-    (Scan.succeed (Toplevel.print o Toplevel.proof IsarThy.begin_block));
+    (P.marg_comment >> (Toplevel.print oo (Toplevel.proof o IsarThy.begin_block)));
 
 val endP =
   OuterSyntax.command "}" "end explicit proof block" K.prf_block
-    (Scan.succeed (Toplevel.print o Toplevel.proof IsarThy.end_block));
+    (P.marg_comment >> (Toplevel.print oo (Toplevel.proof o IsarThy.end_block)));
 
 val nextP =
   OuterSyntax.command "next" "enter next proof block" K.prf_block
-    (Scan.succeed (Toplevel.print o Toplevel.proof IsarThy.next_block));
+    (P.marg_comment >> (Toplevel.print oo (Toplevel.proof o IsarThy.next_block)));
 
 
 (* end proof *)

--- a/src/Pure/Isar/isar_thy.ML	Sat Jun 03 23:58:37 2000 +0200
+++ b/src/Pure/Isar/isar_thy.ML	Sat Jun 03 23:59:37 2000 +0200
@@ -122,9 +122,9 @@
     * Comment.text -> ProofHistory.T -> ProofHistory.T
   val hence_i: (string * Proof.context attribute list * (term * (term list * term list)))
     * Comment.text -> ProofHistory.T -> ProofHistory.T
-  val begin_block: ProofHistory.T -> ProofHistory.T
-  val next_block: ProofHistory.T -> ProofHistory.T
-  val end_block: ProofHistory.T -> ProofHistory.T
+  val begin_block: Comment.text -> ProofHistory.T -> ProofHistory.T
+  val next_block: Comment.text -> ProofHistory.T -> ProofHistory.T
+  val end_block: Comment.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
@@ -387,9 +387,9 @@
 
 (* blocks *)
 
-val begin_block = ProofHistory.apply Proof.begin_block;
-val next_block = ProofHistory.apply Proof.next_block;
-val end_block = ProofHistory.applys Proof.end_block;
+fun begin_block comment_ignore = ProofHistory.apply Proof.begin_block;
+fun next_block comment_ignore = ProofHistory.apply Proof.next_block;
+fun end_block comment_ignore = ProofHistory.applys Proof.end_block;
 
 
 (* shuffle state *)