# HG changeset patch
# User berghofe
# Date 1106825692 -3600
# Node ID 24132e4965612ed7b53005bc7f1319b49fd82bcb
# Parent  4674102737e9b83c6c1ed5883abb334f4ee8040d
- Proofs are now hidden by default
- Added show_var_qmarks flag

diff -r 4674102737e9 -r 24132e496561 src/Pure/Isar/isar_output.ML
--- a/src/Pure/Isar/isar_output.ML	Thu Jan 27 12:34:09 2005 +0100
+++ b/src/Pure/Isar/isar_output.ML	Thu Jan 27 12:34:52 2005 +0100
@@ -185,7 +185,7 @@
 
 val interest_level = ref 0;
 
-val hide_commands = ref false;
+val hide_commands = ref true;
 val hidden_commands = ref ([] : string list);
 
 fun add_hidden_commands cmds = (hidden_commands := !hidden_commands @ cmds);
@@ -296,6 +296,7 @@
  [("show_types", Library.setmp Syntax.show_types o boolean),
   ("show_sorts", Library.setmp Syntax.show_sorts o boolean),
   ("show_structs", Library.setmp show_structs o boolean),
+  ("show_var_qmarks", Library.setmp show_var_qmarks o boolean),
   ("long_names", Library.setmp NameSpace.long_names o boolean),
   ("eta_contract", Library.setmp Syntax.eta_contract o boolean),
   ("locale", Library.setmp locale),