# HG changeset patch
# User wenzelm
# Date 1014744025 -3600
# Node ID 7d5bd53555d818529a9212998411def3d7cc00fc
# Parent  2d61562329942ef5ec05f5b392d3e49cc682613a
markup commands: proper theory/proof transactions!

diff -r 2d6156232994 -r 7d5bd53555d8 src/Pure/Isar/isar_cmd.ML
--- a/src/Pure/Isar/isar_cmd.ML	Tue Feb 26 18:20:01 2002 +0100
+++ b/src/Pure/Isar/isar_cmd.ML	Tue Feb 26 18:20:25 2002 +0100
@@ -308,21 +308,31 @@
   (if Toplevel.is_toplevel state then () else raise Toplevel.UNDEF;
     OuterSyntax.check_text s int state));
 
+local
+
 fun present_text assert_proof present (s, pos) = Toplevel.keep' (fn int => fn state =>
   (if can Toplevel.proof_of state = assert_proof then () else raise Toplevel.UNDEF;
+    Context.setmp (Some (Toplevel.theory_of state)) present s;
     OuterSyntax.check_text (s, pos) int state;
-    Context.setmp (Some (Toplevel.theory_of state)) present s));
+    raise Toplevel.UNDEF));
+
+fun theory f x = Toplevel.theory I o present_text false f x;
+fun proof f x = Toplevel.print o Toplevel.proof (ProofHistory.apply I) o present_text true f x;
 
-val add_chapter = present_text false Present.section;
-val add_section = present_text false Present.section;
-val add_subsection = present_text false Present.subsection;
-val add_subsubsection = present_text false Present.subsubsection;
-val add_text = present_text false (K ());
+in
+
+val add_chapter = theory Present.section;
+val add_section = theory Present.section;
+val add_subsection = theory Present.subsection;
+val add_subsubsection = theory Present.subsubsection;
+val add_text = theory (K ());
 val add_text_raw = add_text;
-val add_txt = present_text true (K ());
+val add_txt = proof (K ());
 val add_txt_raw = add_txt;
 val add_sect = add_txt;
 val add_subsect = add_txt;
 val add_subsubsect = add_txt;
 
 end;
+
+end;