# HG changeset patch # User wenzelm # Date 1368642523 -7200 # Node ID bdb82afdcb922367f16066962f514483700751eb # Parent 0b1183012a3c20c018c5e4ab444e69c96d9d1441 clarified default for Proofterm.proofs, according to etc/options and innermost setmp; diff -r 0b1183012a3c -r bdb82afdcb92 src/Pure/ProofGeneral/proof_general_pure.ML --- a/src/Pure/ProofGeneral/proof_general_pure.ML Wed May 15 20:22:46 2013 +0200 +++ b/src/Pure/ProofGeneral/proof_general_pure.ML Wed May 15 20:28:43 2013 +0200 @@ -133,7 +133,7 @@ "Skip over proofs"; val _ = - Unsynchronized.setmp Proofterm.proofs 0 (fn () => + Unsynchronized.setmp Proofterm.proofs 1 (fn () => ProofGeneral.preference_raw ProofGeneral.category_proof (Markup.print_bool o Proofterm.proofs_enabled) (fn s => Proofterm.proofs := (if Markup.parse_bool s then 2 else 1))