From e0f49c585004b33476039f0ab2734dba95155e2f Mon Sep 17 00:00:00 2001
From: David Aspinall
Date: Fri, 7 Apr 2000 14:03:52 +0000
Subject: Tweak to disable_pr function to allow for it being called twice
 (why?).

---
 isa/isa.el | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/isa/isa.el b/isa/isa.el
index 18c91948..843950d0 100644
--- a/isa/isa.el
+++ b/isa/isa.el
@@ -194,7 +194,7 @@ and script mode."
 
    ;; initial command configures Isabelle by hacking print functions.
    ;; FIXME: temporary hack for almost enabling/disabling printing.
-   proof-shell-init-cmd                 "val pg_saved_gl = ref (!goals_limit); fun proofgeneral_enable_pr () = goals_limit:= !pg_saved_gl; fun proofgeneral_disable_pr() = (pg_saved_gl := !goals_limit; goals_limit := 0); ProofGeneral.init false;"
+   proof-shell-init-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;"
    proof-shell-restart-cmd		"ProofGeneral.isa_restart();"
    proof-shell-quit-cmd			"quit();"
    
-- 
cgit v1.2.3