# HG changeset patch
# User wenzelm
# Date 1175638282 -7200
# Node ID 18735b5fef26c3e2710f1cd1e371a41dc8b04526
# Parent  4a859d13ef836ff4b6d6b45af0c4b127a32c0354
added print_mode;

diff -r 4a859d13ef83 -r 18735b5fef26 src/Pure/ProofGeneral/pgip_standalone.ML
--- a/src/Pure/ProofGeneral/pgip_standalone.ML	Wed Apr 04 00:11:21 2007 +0200
+++ b/src/Pure/ProofGeneral/pgip_standalone.ML	Wed Apr 04 00:11:22 2007 +0200
@@ -19,6 +19,10 @@
 use "General/path.ML";     (* used directly *)
 use "General/table.ML";
 use "General/alist.ML";
+
+val print_mode = ref ([]: string list);
+fun print_mode_active s = member (op =) (! print_mode) s;
+
 use "General/output.ML";
 use "General/scan.ML";
 use "General/source.ML";