proper setup for theorem dependencies;

3 files changed, 16 insertions, 74 deletions

diff --git a/isa/isa.el b/isa/isa.el
index bec0003d..387a3ce0 100644
--- a/isa/isa.el
+++ b/isa/isa.el
@@ -1,4 +1,4 @@
-;; isa-mode.el	 Emacs support for Isabelle proof assistant
+; isa-mode.el	 Emacs support for Isabelle proof assistant
 ;; Copyright (C) 1993-2000 LFCS Edinburgh, David Aspinall.
 ;; License:   GPL (GNU GENERAL PUBLIC LICENSE)
 ;; Author:    David Aspinall <da@dcs.ed.ac.uk>
@@ -189,9 +189,7 @@ and script mode."
    ;; restoring settings saved by Proof General, etc.
 
    proof-shell-pre-sync-init-cmd	"ProofGeneral.init false;"
-   proof-shell-init-cmd		        (concat
-					 (isa-load-isabelle-patch)
-					 (proof-assistant-settings-cmd))
+   proof-shell-init-cmd		        (proof-assistant-settings-cmd)
 
    proof-shell-restart-cmd		"ProofGeneral.isa_restart();"
    proof-shell-quit-cmd			"quit();"
@@ -206,7 +204,7 @@ and script mode."
    proof-shell-clear-response-regexp    "Proof General, please clear the response buffer."
    proof-shell-clear-goals-regexp       "Proof General, please clear the goals buffer."
    proof-shell-set-elisp-variable-regexp "Proof General, please set the variable \\([^ ]+\\) to: #\\([^#]+\\)#\\."
-   proof-shell-theorem-dependency-list-regexp    "Proof General, the theorem dependencies are: \"\\([^\"]*\\)\"" 
+   proof-shell-theorem-dependency-list-regexp    "Proof General, theorem dependencies are: \\(.*\\)"
    proof-shell-show-dependency-cmd	"thm \"%s\";" 
    
    ;; Dirty hack to allow font-locking for output based on hidden
@@ -621,9 +619,9 @@ you will be asked to retract the file or process the remainder of it."
 
 (setq proof-xsym-extra-modes '(thy-mode)
       proof-xsym-activate-command
-      "print_mode := ([\"xsymbols\",\"symbols\"] @ ! print_mode);"
+      "print_mode := ([\"xsymbols\", \"symbols\"] @ ! print_mode);"
       proof-xsym-deactivate-command
-      "print_mode := (! print_mode \\\\ [\"xsymbols\",\"symbols\"]);")
+      "print_mode := (! print_mode \\\\ [\"xsymbols\", \"symbols\"]);")
 
 
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
@@ -729,31 +727,4 @@ you will be asked to retract the file or process the remainder of it."
     ;; that's it for now!
     ))
 
-
-;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
-;;
-;; Theorem dependencies  (experimental, uses Isabelle "patch")
-;;
-
-(defun isa-load-isabelle-patch ()
-  "Return string to load patch to Isabelle or a dummy version of it."
-  (if proof-experimental-features
-      (isa-load-dependsml-file-cmd)
-    "structure PGThmDeps = struct fun enable()=() fun disable() = () end;"))
-
-(defpacustom theorem-dependencies nil
-  "Whether to track theorem dependencies within Proof General."
-  :type 'boolean
-  ;; when this is built-in  (or with a ":=%b" setting).
-  ;; :setting ("depends_enable()" . "depends_disable()")
-  :setting ("PGThmDeps.enable();" . "PGThmDeps.disable();"))
-
-(defun isa-load-dependsml-file-cmd ()
-  (proof-format-filename
-   "use \"%r\";"
-   (concat (file-name-directory 
-	    (locate-library "isa"))
-	   "depends.ML")))
-
-
 (provide 'isa)
diff --git a/isa/isabelle-system.el b/isa/isabelle-system.el
index 1262e786..7e2f3c68 100644
--- a/isa/isabelle-system.el
+++ b/isa/isabelle-system.el
@@ -346,7 +346,7 @@ until Proof General is restarted."
 (defpacustom full-proofs  nil
   "Whether to record full proof objects internally."
   :type 'boolean
-  :setting "Library.error_fn := (fn _ => ()); Library.try (fn () => Context.use_mltext \"ProofGeneral.full_proofs %b;\" false None) ();")
+  :setting "Library.error_fn := (fn _ => ()); Library.try (fn () => Context.use_mltext \"ProofGeneral.full_proofs %b;\" false Library.None) ();")
 ;FIXME should become "ProofGeneral.full_proofs %b;" next time
 
 (defpacustom global-timing  nil
@@ -354,6 +354,12 @@ until Proof General is restarted."
   :type 'boolean
   :setting "Library.timing:=%b;")
 
+(defpacustom theorem-dependencies nil
+  "Whether to track theorem dependencies within Proof General."
+  :type 'boolean
+  :setting ("print_mode := ([\"thm_deps\"] @ ! print_mode);" .
+	    "print_mode := (Library.gen_rems (op =) (! print_mode, [\"thm_deps\"]))"))
+
 (defpacustom goals-limit  10
   "Setting for maximum number of goals printed in Isabelle."
   :type 'integer
diff --git a/isar/isar.el b/isar/isar.el
index d0b8c6ec..5bd8bcef 100644
--- a/isar/isar.el
+++ b/isar/isar.el
@@ -219,9 +219,7 @@ See -k option for Isabelle interface script."
    pg-topterm-char			?\370
 
    proof-assistant-setting-format       'isar-markup-ml
-   proof-shell-init-cmd                 (concat
-					 (isar-load-isabelle-patch)
-					 (proof-assistant-settings-cmd))
+   proof-shell-init-cmd                 (proof-assistant-settings-cmd)
    proof-shell-restart-cmd              "ProofGeneral.restart"
 
    proof-shell-eager-annotation-start-length 1
@@ -232,7 +230,7 @@ See -k option for Isabelle interface script."
    ;; Some messages delimited by eager annotations
    proof-shell-clear-response-regexp    "Proof General, please clear the response buffer."
    proof-shell-clear-goals-regexp       "Proof General, please clear the goals buffer."
-   proof-shell-theorem-dependency-list-regexp "Proof General, the theorem dependencies are: \"\\([^\"]*\\)\"" 
+   proof-shell-theorem-dependency-list-regexp "Proof General, theorem dependencies are: \\(.*\\)"
 
    ;; Allow font-locking for output based on hidden annotations, see
    ;; isar-output-font-lock-keywords-1
@@ -598,41 +596,8 @@ proof-shell-retract-files-regexp."
 
 (setq
  proof-xsym-activate-command
- (isar-markup-ml "print_mode := ([\"xsymbols\",\"symbols\"] @ ! print_mode)")
+ (isar-markup-ml "print_mode := ([\"xsymbols\", \"symbols\"] @ ! print_mode)")
  proof-xsym-deactivate-command
- (isar-markup-ml "print_mode := (Library.gen_rems (op =) (! print_mode, [\"xsymbols\",\"symbols\"]))"))
-
-
-;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
-;;
-;; Theorem dependencies  (experimental, uses Isabelle "patch")
-;;
-
-(defun isar-load-isabelle-patch ()
-  "Return string to load patch to Isabelle or a dummy version of it."
-  (if proof-experimental-features
-       (isar-load-dependsml-file-cmd)
-    (isar-markup-ml
-     "structure PGThmDeps = struct fun enable()=() fun disable() = () end; fun PG_thm_deps x = ();")))
-
-;; NB: notice backquote here to evaluate isar-markup-ml
-`(defpacustom theorem-dependencies nil
-  "Whether to track theorem dependencies within Proof General."
-  :type 'boolean
-  ;; when this is built-in  (or with a ":=%b" setting).
-  ;; :setting ("depends_enable()" . "depends_disable()")
-  :setting ,(cons
-	     (isar-markup-ml "PGThmDeps.enable();") 
-	     (isar-markup-ml "PGThmDeps.disable();")))
-
-(defun isar-load-dependsml-file-cmd ()
-  (isar-markup-ml
-   (proof-format-filename
-    "use \"%r\";"
-    (concat (file-name-directory 
-	     (locate-library "isa"))
-	    "depends.ML"))))
-
-
+ (isar-markup-ml "print_mode := (Library.gen_rems (op =) (! print_mode, [\"xsymbols\", \"symbols\"]))"))
 
 (provide 'isar)