From aede0ea6f6a1d3172081ab3967dea6be8e34ce89 Mon Sep 17 00:00:00 2001
From: David Aspinall
Date: Sun, 16 Feb 2003 01:44:58 +0000
Subject: Add backwards compatibility for old pre-PGIP settings mechanism

---
 isa/isa.el             |   3 +-
 isa/isabelle-system.el | 192 ++++++++++++++++++++++++++++---------------------
 isar/isar.el           |  20 ++++--
 3 files changed, 126 insertions(+), 89 deletions(-)

diff --git a/isa/isa.el b/isa/isa.el
index 3d21f61f..6d0e7d7a 100644
--- a/isa/isa.el
+++ b/isa/isa.el
@@ -196,7 +196,8 @@ and script mode."
 
    ;; Isabelle is learning to talk PGIP...
    proof-shell-match-pgip-cmd		"<pgip"
-   proof-shell-issue-pgip-cmd		'isabelle-process-pgip
+   proof-shell-issue-pgip-cmd		
+	(if isa-supports-pgip 'isabelle-process-pgip nil)
 
    ;; Some messages delimited by eager annotations
    proof-shell-clear-response-regexp    "Proof General, please clear the response buffer."
diff --git a/isa/isabelle-system.el b/isa/isabelle-system.el
index f30b9734..03dbd5a4 100644
--- a/isa/isabelle-system.el
+++ b/isa/isabelle-system.el
@@ -195,6 +195,29 @@ ISABELLE will always override this setting."
 	     "isa-view-doc" nil
 	     (list isa-isatool-command "doc" docname))))
 
+(defvar isabelle-version-string 'unset)
+
+(defun isa-version ()
+  "Try to retrieve a version value for Isabelle."
+  (unless (stringp isabelle-version-string)
+    (setq isabelle-version-string
+	  (if (isa-set-isatool-command)
+	      (isa-shell-command-to-string
+	       ;; This may return the string "Unknown Isabelle tool:
+	       ;; version", but that's fine.
+	       (concat isa-isatool-command " version"))
+	    "Unknown")))
+  isabelle-version-string)
+
+;; We're going to need to know this pretty soon, so let's do it now.
+(defconst isa-supports-pgip 
+  ;; PGIP-aware Isabelle versions are also aware of their own version
+  (not (string-match "^Unknown" (isa-version)))
+  "Whether the currently configured version of Isabelle supports PGIP.")
+
+      
+
+
 (defun isa-tool-list-docs ()
   "Generate a list of documentation files available, with descriptions.
 This function returns a list of lists of the form
@@ -314,7 +337,6 @@ until Proof General is restarted."
 (defconst isabelle-logics-menu (isabelle-logics-menu-calculate)
   "Isabelle logics menu.  Calculated when Proof General is loaded.")
 
-
 ;; Added in PG 3.4: load isar-keywords file.
 ;; This roughly follows the method given in the interface script.
 ;; It could be used to add an elisp command at the bottom of
@@ -342,82 +364,85 @@ until Proof General is restarted."
 ;; NB: use of defpacustom here gives  separate customizable
 ;; options for Isabelle and Isabelle/Isar.
 
-;; In next release of Isabelle, these are set automatically via PGIP
-;; sent from Isabelle.  
-;; FIXME: should we add backward compatibility here?
-
-;(defpacustom show-types  nil
-;  "Whether to show types in Isabelle."
-;  :type 'boolean
-;  :setting "show_types:=%b;")
-
-;(defpacustom show-sorts  nil
-;  "Whether to show sorts in Isabelle."
-;  :type 'boolean
-;  :setting "show_sorts:=%b;")
-
-;(defpacustom show-consts  nil
-;  "Whether to show types of consts in Isabelle goals."
-;  :type 'boolean
-;  :setting "show_consts:=%b;")
-
-;(defpacustom long-names  nil
-;  "Whether to show fully qualified names in Isabelle."
-;  :type 'boolean
-;  :setting "long_names:=%b;")
-
-;(defpacustom eta-contract  t
-;  "Whether to print terms eta-contracted in Isabelle."
-;  :type 'boolean
-;  :setting "Syntax.eta_contract:=%b;")
-
-;(defpacustom trace-simplifier  nil
-;  "Whether to trace the Simplifier in Isabelle."
-;  :type 'boolean
-;  :setting "trace_simp:=%b;")
-
-;(defpacustom trace-rules  nil
-;  "Whether to trace the standard rules in Isabelle."
-;  :type 'boolean
-;  :setting "trace_rules:=%b;")
-
-;(defpacustom quick-and-dirty  t
-;  "Whether to take a few short cuts occasionally."
-;  :type 'boolean
-;  :setting "quick_and_dirty:=%b;")
-
-;(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 Library.None) ();")
-;;FIXME should become "ProofGeneral.full_proofs %b;" next time
-
-;(defpacustom global-timing  nil
-;  "Whether to enable timing in Isabelle."
-;  :type 'boolean
-;  :setting "Library.timing:=%b;")
-
-;(if proof-experimental-features
-;(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
-;  :setting "goals_limit:=%i;")
-
-;(defpacustom prems-limit  10
-;  "Setting for maximum number of premises printed in Isabelle/Isar."
-;  :type 'integer
-;  :setting "ProofContext.prems_limit:=%i;")
-
-;(defpacustom print-depth  10
-;  "Setting for the ML print depth in Isabelle."
-;  :type 'integer
-;  :setting "print_depth %i;")
+;; In latest release of Isabelle, these are set automatically via PGIP
+;; sent from Isabelle.
+
+;; BEGIN backwards compatibility 
+(cond 
+ ((not isa-supports-pgip)
+(defpacustom show-types  nil
+  "Whether to show types in Isabelle."
+  :type 'boolean
+  :setting "show_types:=%b;")
+
+(defpacustom show-sorts  nil
+  "Whether to show sorts in Isabelle."
+  :type 'boolean
+  :setting "show_sorts:=%b;")
+
+(defpacustom show-consts  nil
+  "Whether to show types of consts in Isabelle goals."
+  :type 'boolean
+  :setting "show_consts:=%b;")
+
+(defpacustom long-names  nil
+  "Whether to show fully qualified names in Isabelle."
+  :type 'boolean
+  :setting "long_names:=%b;")
+
+(defpacustom eta-contract  t
+  "Whether to print terms eta-contracted in Isabelle."
+  :type 'boolean
+  :setting "Syntax.eta_contract:=%b;")
+
+(defpacustom trace-simplifier  nil
+  "Whether to trace the Simplifier in Isabelle."
+  :type 'boolean
+  :setting "trace_simp:=%b;")
+
+(defpacustom trace-rules  nil
+  "Whether to trace the standard rules in Isabelle."
+  :type 'boolean
+  :setting "trace_rules:=%b;")
+
+(defpacustom quick-and-dirty  t
+  "Whether to take a few short cuts occasionally."
+  :type 'boolean
+  :setting "quick_and_dirty:=%b;")
+
+(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 Library.None) ();")
+;FIXME should become "ProofGeneral.full_proofs %b;" next time
+
+(defpacustom global-timing  nil
+  "Whether to enable timing in Isabelle."
+  :type 'boolean
+  :setting "Library.timing:=%b;")
+
+(if proof-experimental-features
+(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
+  :setting "goals_limit:=%i;")
+
+(defpacustom prems-limit  10
+  "Setting for maximum number of premises printed in Isabelle/Isar."
+  :type 'integer
+  :setting "ProofContext.prems_limit:=%i;")
+
+(defpacustom print-depth  10
+  "Setting for the ML print depth in Isabelle."
+  :type 'integer
+  :setting "print_depth %i;")))
+;; END backwards compatibility 
 
 
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
@@ -510,11 +535,14 @@ the function `pg-remove-specials' can be used instead)."
 
 (defun isabelle-process-pgip (xmlstring)
   "Return an Isabelle or Isabelle/Isar command to process PGIP in XMLSTRING."
-  (let ((mlcmd (format "ProofGeneral.process_pgip(\"%s\");"
-		       (isabelle-xml-sml-escapes xmlstring))))
-    (if (eq proof-assistant-symbol 'isar)
-	(isar-markup-ml mlcmd)
-      mlcmd)))
+  (if isa-supports-pgip
+      (let ((mlcmd (format "ProofGeneral.process_pgip(\"%s\");"
+			   (isabelle-xml-sml-escapes xmlstring))))
+	(if (eq proof-assistant-symbol 'isar)
+	    (isar-markup-ml mlcmd)
+	  mlcmd))
+    "")) ;; Empty string in case called with non PGIP-aware Isabelle.
+
 
 (provide 'isabelle-system)
 ;; End of isabelle-system.el
diff --git a/isar/isar.el b/isar/isar.el
index 8d39514d..18a1297b 100644
--- a/isar/isar.el
+++ b/isar/isar.el
@@ -2,8 +2,11 @@
 ;; Copyright (C) 1994-1998 LFCS Edinburgh.
 ;; License:   GPL (GNU GENERAL PUBLIC LICENSE)
 ;;
-;; Author:              David Aspinall <da@dcs.ed.ac.uk>
-;; Author / Maintainer: Markus Wenzel <wenzelm@in.tum.de>
+;; Maintainer:    Stefan Berghofer 
+;;
+;; Authors:       David Aspinall <da@dcs.ed.ac.uk>
+;;   	          Markus Wenzel <wenzelm@in.tum.de>
+;;
 ;;
 ;; $Id$
 ;;
@@ -220,7 +223,8 @@ See -k option for Isabelle interface script."
    ;; Would be nice to remove this somehow else, it's only used for 
    ;; Isar.  One way would be to hack the (now obsolete) defpacustom calls.
    ;; 
-   ;; proof-assistant-setting-format       'isar-markup-ml
+   proof-assistant-setting-format       
+   (unless isa-supports-pgip 'isar-markup-ml)
    proof-shell-init-cmd                 '(proof-assistant-settings-cmd)
    proof-shell-restart-cmd              "ProofGeneral.restart"
 
@@ -230,8 +234,10 @@ See -k option for Isabelle interface script."
    ;; see isar-pre-shell-start for proof-shell-trace-output-regexp
 
    ;; Isabelle is learning to talk PGIP...
+   ;; FIXME: we need to be backwards compatible here
    proof-shell-match-pgip-cmd		"<pgip"
-   proof-shell-issue-pgip-cmd		'isabelle-process-pgip
+   proof-shell-issue-pgip-cmd		
+	(if isa-supports-pgip 'isabelle-process-pgip nil)
 
    ;; Some messages delimited by eager annotations
    proof-shell-clear-response-regexp    "Proof General, please clear the response buffer."
@@ -610,8 +616,10 @@ 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\"]))"))
+ (isar-markup-ml 
+  "print_mode := (Library.gen_rems (op =) (! print_mode, [\"xsymbols\", \"symbols\"]))"))
 
 (provide 'isar)
-- 
cgit v1.2.3