src/Pure/ProofGeneral/proof_general_pgip.ML
changeset 24614 a4b2eb0dd673
parent 24244 d7ee11ba1534
child 24712 64ed05609568
equal deleted inserted replaced
24613:bc889c3d55a3 24614:a4b2eb0dd673
   570 fun set_proverflag_quiet b = 
   570 fun set_proverflag_quiet b = 
   571     isarcmd (if b then "disable_pr" else "enable_pr")
   571     isarcmd (if b then "disable_pr" else "enable_pr")
   572 
   572 
   573 fun set_proverflag_pgmlsymbols b =
   573 fun set_proverflag_pgmlsymbols b =
   574     (pgmlsymbols_flag := b;
   574     (pgmlsymbols_flag := b;
   575      change print_mode 
   575       NAMED_CRITICAL "print_mode" (fn () =>
       
   576         change print_mode 
   576             (fn mode =>
   577             (fn mode =>
   577                 remove (op =) Symbol.xsymbolsN mode @ (if b then [Symbol.xsymbolsN] else [])))
   578                 remove (op =) Symbol.xsymbolsN mode @ (if b then [Symbol.xsymbolsN] else []))))
   578 
   579 
   579 fun set_proverflag_thmdeps b =
   580 fun set_proverflag_thmdeps b =
   580     (show_theorem_dependencies := b;
   581     (show_theorem_dependencies := b;
   581      proofs := (if b then 1 else 2))
   582      proofs := (if b then 1 else 2))
   582 
   583