From 8fefa9e358e7c41f24b1bf42c0ad48587e8bf1ba Mon Sep 17 00:00:00 2001 From: Makarius Wenzel Date: Thu, 18 May 2000 16:13:50 +0000 Subject: Goals.enable/disable_pr: improved version for Isabelle99-1 (commented out); --- isa/isa.el | 7 +++++++ 1 file changed, 7 insertions(+) diff --git a/isa/isa.el b/isa/isa.el index b2a996eb..81b7f793 100644 --- a/isa/isa.el +++ b/isa/isa.el @@ -115,6 +115,9 @@ and script mode." proof-find-theorems-command "ProofGeneral.thms_containing (space_explode \",\" \"%s\");" proof-shell-start-silent-cmd "proofgeneral_disable_pr();" proof-shell-stop-silent-cmd "proofgeneral_enable_pr();" + ; FIXME improved version for Isabelle99-1: + ; proof-shell-start-silent-cmd "Goals.disable_pr();" + ; proof-shell-stop-silent-cmd "Goals.enable_pr();" ;; command hooks proof-goal-command-p 'isa-goal-command-p proof-count-undos-fn 'isa-count-undos @@ -181,6 +184,10 @@ and script mode." ;; Also for setting default values. proof-shell-init-cmd (concat (isabelle-set-default-cmd) "val pg_saved_gl = ref (!goals_limit); fun proofgeneral_enable_pr () = goals_limit:= !pg_saved_gl; fun proofgeneral_disable_pr() = (pg_saved_gl := (if (!goals_limit)>0 then !goals_limit else !pg_saved_gl); goals_limit := 0); ProofGeneral.init false;") + ; FIXME improved version for Isabelle99-1: + ;proof-shell-init-cmd (concat (isabelle-set-default-cmd) + ; "ProofGeneral.init false;") + proof-shell-restart-cmd "ProofGeneral.isa_restart();" proof-shell-quit-cmd "quit();" -- cgit v1.2.3