- Proofs are now hidden by default
authorberghofe
Thu, 27 Jan 2005 12:34:52 +0100
changeset 15473 24132e496561
parent 15472 4674102737e9
child 15474 6e60be6a6c21
- Proofs are now hidden by default - Added show_var_qmarks flag
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),