# HG changeset patch
# User wenzelm
# Date 1175638280 -7200
# Node ID 5454b06320fb5774eb7b4ec9bc346f0fe24ff49b
# Parent  d2008c5f8d99e8f12e13afe9ac047d2c5d10980a
renamed Output.has_mode to print_mode_active;

diff -r d2008c5f8d99 -r 5454b06320fb src/Pure/Isar/proof_context.ML
--- a/src/Pure/Isar/proof_context.ML	Wed Apr 04 00:11:18 2007 +0200
+++ b/src/Pure/Isar/proof_context.ML	Wed Apr 04 00:11:20 2007 +0200
@@ -290,7 +290,7 @@
     val thy = theory_of ctxt;
     val syntax = syntax_of ctxt;
     val consts = consts_of ctxt;
-    val do_abbrevs = abbrevs andalso not (Output.has_mode "no_abbrevs");
+    val do_abbrevs = abbrevs andalso not (print_mode_active "no_abbrevs");
     val t' = t
       |> do_abbrevs ? rewrite_term true thy (Consts.abbrevs_of consts (! print_mode @ [""]))
       |> do_abbrevs ? rewrite_term false thy (Consts.abbrevs_of consts [Syntax.internalM])
diff -r d2008c5f8d99 -r 5454b06320fb src/Pure/ProofGeneral/preferences.ML
--- a/src/Pure/ProofGeneral/preferences.ML	Wed Apr 04 00:11:18 2007 +0200
+++ b/src/Pure/ProofGeneral/preferences.ML	Wed Apr 04 00:11:20 2007 +0200
@@ -66,7 +66,7 @@
 
 val thm_deps_pref = 
     let 
-	fun get () = PgipTypes.bool_to_pgstring (Output.has_mode thm_depsN)
+	fun get () = PgipTypes.bool_to_pgstring (print_mode_active thm_depsN)
 	fun set s = if PgipTypes.read_pgipbool s then 
 			change print_mode (insert (op =) thm_depsN)
 		    else