From b937e7485be9d69c5b32e9837f90708935791271 Mon Sep 17 00:00:00 2001 From: David Aspinall Date: Thu, 11 May 2000 14:33:55 +0000 Subject: Moved generic settings to isabelle-system.el. isa-set-default-cmd->isabelle-set.. --- isa/isa.el | 29 +---------------------------- 1 file changed, 1 insertion(+), 28 deletions(-) diff --git a/isa/isa.el b/isa/isa.el index d6adba79..19de70da 100644 --- a/isa/isa.el +++ b/isa/isa.el @@ -51,33 +51,6 @@ no regular or easily discernable structure." :type 'number :group 'isabelle) -(defcustom isabelle-web-page - "http://www.cl.cam.ac.uk/Research/HVG/Isabelle/" - ;; "http://www.dcs.ed.ac.uk/home/isabelle" - "URL of web page for Isabelle." - :type 'string - :group 'isabelle) - -;; FIXME: deftoggle should only define toggler, not setter? -(proof-deftoggle isabelle-show-sorts) -(proof-deftoggle isabelle-show-types) - -(defcustom isabelle-menu-entries - (append - '(["Switch to theory" thy-find-other-file t]) - (list "----") - '(["Show types" isabelle-show-types-toggle - :active t :style toggle - :selected isabelle-show-types] - ["Show sorts" isabelle-show-sorts-toggle - :active t :style toggle - :selected isabelle-show-sorts]) - (list "----") - (list isa-docs-menu)) - "Entries for Isabelle menu.") - - - ;;; ;;; ======== Configuration of generic modes ======== @@ -205,7 +178,7 @@ and script mode." ;; initial command configures Isabelle by hacking print functions. ;; FIXME: temporary hack for almost enabling/disabling printing. ;; Also for setting default values. - proof-shell-init-cmd (concat (isa-set-default-cmd) + 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;") proof-shell-restart-cmd "ProofGeneral.isa_restart();" proof-shell-quit-cmd "quit();" -- cgit v1.2.3