# HG changeset patch
# User wenzelm
# Date 931950328 -7200
# Node ID 01a4e15ee253218ae89010a5ab1964e858abcad4
# Parent  8121e11ed765b6fbe27969e1964f6151d421b0f5
more marg_comments;

diff -r 8121e11ed765 -r 01a4e15ee253 src/Pure/Isar/isar_syn.ML
--- a/src/Pure/Isar/isar_syn.ML	Wed Jul 14 12:28:12 1999 +0200
+++ b/src/Pure/Isar/isar_syn.ML	Wed Jul 14 13:05:28 1999 +0200
@@ -343,23 +343,24 @@
 
 val qedP =
   OuterSyntax.command "qed" "conclude (sub-)proof" K.qed_block
-    (Scan.option (P.method -- P.interest) >> IsarThy.qed);
+    (Scan.option (P.method -- P.interest) -- P.marg_comment >> IsarThy.qed);
 
 val terminal_proofP =
   OuterSyntax.command "by" "terminal backward proof" K.qed
-    (P.method -- P.interest -- Scan.option (P.method -- P.interest) >> IsarThy.terminal_proof);
+    (P.method -- P.interest -- Scan.option (P.method -- P.interest)
+      -- P.marg_comment >> IsarThy.terminal_proof);
 
 val immediate_proofP =
   OuterSyntax.command "." "immediate proof" K.qed
-    (Scan.succeed IsarThy.immediate_proof);
+    (P.marg_comment >> IsarThy.immediate_proof);
 
 val default_proofP =
   OuterSyntax.command ".." "default proof" K.qed
-    (Scan.succeed IsarThy.default_proof);
+    (P.marg_comment >> IsarThy.default_proof);
 
 val skip_proofP =
   OuterSyntax.command "sorry" "skip proof (quick-and-dirty mode only!)" K.qed
-    (Scan.succeed IsarThy.skip_proof);
+    (P.marg_comment >> IsarThy.skip_proof);
 
 
 (* proof steps *)
@@ -374,7 +375,7 @@
 
 val proofP =
   OuterSyntax.command "proof" "backward proof" K.prf_block
-    (P.interest -- Scan.option (P.method -- P.interest)
+    (P.interest -- Scan.option (P.method -- P.interest) -- P.marg_comment
       >> (Toplevel.print oo (Toplevel.proof o IsarThy.proof)));
 
 
diff -r 8121e11ed765 -r 01a4e15ee253 src/Pure/Isar/isar_thy.ML
--- a/src/Pure/Isar/isar_thy.ML	Wed Jul 14 12:28:12 1999 +0200
+++ b/src/Pure/Isar/isar_thy.ML	Wed Jul 14 13:05:28 1999 +0200
@@ -113,15 +113,16 @@
   val end_block: 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
+  val proof: (Comment.interest * (Method.text * Comment.interest) option) * Comment.text
     -> ProofHistory.T -> ProofHistory.T
   val kill_proof: ProofHistory.T -> theory
-  val qed: (Method.text * Comment.interest) option -> Toplevel.transition -> Toplevel.transition
-  val terminal_proof: (Method.text * Comment.interest) * (Method.text * Comment.interest) option
+  val qed: (Method.text * Comment.interest) option * Comment.text
     -> Toplevel.transition -> Toplevel.transition
-  val immediate_proof: Toplevel.transition -> Toplevel.transition
-  val default_proof: Toplevel.transition -> Toplevel.transition
-  val skip_proof: Toplevel.transition -> Toplevel.transition
+  val terminal_proof: ((Method.text * Comment.interest) * (Method.text * Comment.interest) option)
+    * Comment.text -> Toplevel.transition -> Toplevel.transition
+  val immediate_proof: Comment.text -> Toplevel.transition -> Toplevel.transition
+  val default_proof: Comment.text -> Toplevel.transition -> Toplevel.transition
+  val skip_proof: Comment.text -> Toplevel.transition -> Toplevel.transition
   val also: ((string * Args.src list) list * Comment.interest) option * Comment.text
     -> Toplevel.transition -> Toplevel.transition
   val also_i: (thm list * Comment.interest) option * Comment.text
@@ -309,8 +310,8 @@
 val tac = ProofHistory.applys o Method.tac;
 val then_tac = ProofHistory.applys o Method.then_tac;
 
-val proof =
-  ProofHistory.applys o Method.proof o apsome Comment.ignore_interest o Comment.ignore_interest';
+val proof = ProofHistory.applys o Method.proof o
+  apsome Comment.ignore_interest o Comment.ignore_interest' o Comment.ignore;
 
 
 (* print result *)
@@ -365,11 +366,11 @@
 
 (* common endings *)
 
-fun qed meth = local_qed meth o global_qed meth;
-fun terminal_proof meths = local_terminal_proof meths o global_terminal_proof meths;
-val immediate_proof = local_immediate_proof o global_immediate_proof;
-val default_proof = local_default_proof o global_default_proof;
-val skip_proof = local_skip_proof o global_skip_proof;
+fun qed (meth, comment) = local_qed meth o global_qed meth;
+fun terminal_proof (meths, comment) = local_terminal_proof meths o global_terminal_proof meths;
+fun immediate_proof comment = local_immediate_proof o global_immediate_proof;
+fun default_proof comment = local_default_proof o global_default_proof;
+fun skip_proof comment = local_skip_proof o global_skip_proof;
 
 
 (* calculational proof commands *)