apply etc.: comments;
authorwenzelm
Fri Apr 07 17:36:25 2000 +0200 (2000-04-07 ago)
changeset 8681957a5fe9b212
parent 8680 898cf487632e
child 8682 82ebf8618e6b
apply etc.: comments;
src/Pure/Isar/isar_syn.ML
src/Pure/Isar/isar_thy.ML
     1.1 --- a/src/Pure/Isar/isar_syn.ML	Thu Apr 06 19:11:30 2000 +0200
     1.2 +++ b/src/Pure/Isar/isar_syn.ML	Fri Apr 07 17:36:25 2000 +0200
     1.3 @@ -387,20 +387,20 @@
     1.4  (* proof steps *)
     1.5  
     1.6  val deferP =
     1.7 -  OuterSyntax.command "defer" "shuffle internal proof state"
     1.8 -    K.prf_script (Scan.option P.nat >> (Toplevel.print oo (Toplevel.proof o IsarThy.defer)));
     1.9 +  OuterSyntax.command "defer" "shuffle internal proof state" K.prf_script
    1.10 +    (Scan.option P.nat -- P.marg_comment >> (Toplevel.print oo (Toplevel.proof o IsarThy.defer)));
    1.11  
    1.12  val preferP =
    1.13 -  OuterSyntax.command "prefer" "shuffle internal proof state"
    1.14 -    K.prf_script (P.nat >> (Toplevel.print oo (Toplevel.proof o IsarThy.prefer)));
    1.15 +  OuterSyntax.command "prefer" "shuffle internal proof state" K.prf_script
    1.16 +    (P.nat -- P.marg_comment >> (Toplevel.print oo (Toplevel.proof o IsarThy.prefer)));
    1.17  
    1.18  val applyP =
    1.19 -  OuterSyntax.command "apply" "initial refinement step (unstructured)"
    1.20 -    K.prf_script (P.method >> (Toplevel.print oo (Toplevel.proof o IsarThy.apply)));
    1.21 +  OuterSyntax.command "apply" "initial refinement step (unstructured)" K.prf_script
    1.22 +    (P.method -- P.marg_comment >> (Toplevel.print oo (Toplevel.proof o IsarThy.apply)));
    1.23  
    1.24  val apply_endP =
    1.25 -  OuterSyntax.command "apply_end" "terminal refinement (unstructured)"
    1.26 -    K.prf_script (P.method >> (Toplevel.print oo (Toplevel.proof o IsarThy.apply_end)));
    1.27 +  OuterSyntax.command "apply_end" "terminal refinement (unstructured)" K.prf_script
    1.28 +    (P.method -- P.marg_comment >> (Toplevel.print oo (Toplevel.proof o IsarThy.apply_end)));
    1.29  
    1.30  val proofP =
    1.31    OuterSyntax.command "proof" "backward proof" K.prf_block
     2.1 --- a/src/Pure/Isar/isar_thy.ML	Thu Apr 06 19:11:30 2000 +0200
     2.2 +++ b/src/Pure/Isar/isar_thy.ML	Fri Apr 07 17:36:25 2000 +0200
     2.3 @@ -120,10 +120,10 @@
     2.4    val begin_block: ProofHistory.T -> ProofHistory.T
     2.5    val next_block: ProofHistory.T -> ProofHistory.T
     2.6    val end_block: ProofHistory.T -> ProofHistory.T
     2.7 -  val defer: int option -> ProofHistory.T -> ProofHistory.T
     2.8 -  val prefer: int -> ProofHistory.T -> ProofHistory.T
     2.9 -  val apply: Method.text -> ProofHistory.T -> ProofHistory.T
    2.10 -  val apply_end: Method.text -> ProofHistory.T -> ProofHistory.T
    2.11 +  val defer: int option * Comment.text -> ProofHistory.T -> ProofHistory.T
    2.12 +  val prefer: int * Comment.text -> ProofHistory.T -> ProofHistory.T
    2.13 +  val apply: Method.text * Comment.text -> ProofHistory.T -> ProofHistory.T
    2.14 +  val apply_end: Method.text * Comment.text -> ProofHistory.T -> ProofHistory.T
    2.15    val proof: (Comment.interest * (Method.text * Comment.interest) option) * Comment.text
    2.16      -> ProofHistory.T -> ProofHistory.T
    2.17    val qed: (Method.text * Comment.interest) option * Comment.text
    2.18 @@ -355,14 +355,15 @@
    2.19  
    2.20  fun shuffle meth i = Method.refine (Method.Basic (K (meth i))) o Proof.assert_no_chain;
    2.21  
    2.22 -fun defer i = ProofHistory.applys (shuffle Method.defer i);
    2.23 -fun prefer i = ProofHistory.applys (shuffle Method.prefer i);
    2.24 +fun defer (i, comment_ignore) = ProofHistory.applys (shuffle Method.defer i);
    2.25 +fun prefer (i, comment_ignore) = ProofHistory.applys (shuffle Method.prefer i);
    2.26  
    2.27  
    2.28  (* backward steps *)
    2.29  
    2.30 -fun apply m = ProofHistory.applys (Method.refine m o Proof.assert_backward);
    2.31 -fun apply_end m = ProofHistory.applys (Method.refine_end m o Proof.assert_forward);
    2.32 +fun apply (m, comment_ignore) = ProofHistory.applys (Method.refine m o Proof.assert_backward);
    2.33 +fun apply_end (m, comment_ignore) =
    2.34 +  ProofHistory.applys (Method.refine_end m o Proof.assert_forward);
    2.35  
    2.36  val proof = ProofHistory.applys o Method.proof o
    2.37    apsome Comment.ignore_interest o Comment.ignore_interest' o Comment.ignore;