diff options
| author |  Makarius Wenzel <makarius@sketis.net> | 2007-10-24 15:12:03 +0000 |
|---|---|---|
| committer | Makarius Wenzel <makarius@sketis.net> | 2007-10-24 15:12:03 +0000 |
| commit | add527a641fea25726d4671387471d015d49d46a (patch) | |
| tree | 6aa56f8d04bdc64a2e74c9849a82b6534dca1621 /isar | |
| parent | c9624e4cc84e9485a3beb3a78615b77e19b5dca3 (diff) | |
proof-shell-issue-pgip-cmd is always isabelle-process-pgip;
Diffstat (limited to 'isar')
| -rw-r--r-- | isar/isar.el | 10 |
1 files changed, 1 insertions, 9 deletions
diff --git a/isar/isar.el b/isar/isar.el index 9d0e741b..16384979 100644 --- a/isar/isar.el +++ b/isar/isar.el @@ -183,13 +183,6 @@ See -k option for Isabelle interface script." proof-shell-start-goals-regexp "\366\n\\|\^AO\n" proof-shell-end-goals-regexp "\367\\|\^AP" - ;; FIXME: next one is needed for backward compatibility. - ;; Would be nice to remove this somehow else, it's only used for - ;; Isar and pre-PGIP. One way would be to hack the - ;; (now obsolete) defpacustom calls. - proof-assistant-setting-format - (unless isa-supports-pgip 'isar-markup-ml) - proof-shell-init-cmd nil proof-shell-restart-cmd "ProofGeneral.restart" @@ -200,8 +193,7 @@ See -k option for Isabelle interface script." ;; Isabelle is learning to talk PGIP... proof-shell-match-pgip-cmd "<pgip" - proof-shell-issue-pgip-cmd - (if isa-supports-pgip 'isabelle-process-pgip nil) + proof-shell-issue-pgip-cmd 'isabelle-process-pgip ;; Some messages delimited by eager annotations proof-shell-clear-response-regexp "Proof General, please clear the response buffer." |