diff options
| author |  David Aspinall <da@inf.ed.ac.uk> | 2007-05-10 22:46:44 +0000 |
|---|---|---|
| committer | David Aspinall <da@inf.ed.ac.uk> | 2007-05-10 22:46:44 +0000 |
| commit | 72dafc10ea200cb6989e3657aad63d2d50043bd7 (patch) | |
| tree | 6a171aa4d36b4e44204fafbe1c3f9ff3b8cc803e | |
| parent | e78ef6e87a9ff7425d733edc5505ba79c6bf4f97 (diff) | |
Add experimental find theorems form (not working on all Emacs yet)
| -rw-r--r-- | isar/isar.el | 9 |
1 files changed, 6 insertions, 3 deletions
diff --git a/isar/isar.el b/isar/isar.el index 20365bb7..a8b28832 100644 --- a/isar/isar.el +++ b/isar/isar.el @@ -16,6 +16,9 @@ (require 'proof) +;; "Find Theorems" search form +(require 'find-theorems) + ;; System code (require 'isabelle-system) @@ -123,7 +126,9 @@ See -k option for Isabelle interface script." proof-context-command "print_context" proof-info-command "welcome" proof-kill-goal-command "ProofGeneral.kill_proof" - proof-find-theorems-command "find_theorems %s" +; proof-find-theorems-command "find_theorems %s" ;; minibuffer +; proof-find-theorems-command 'proof-find-theorems-minibuffer ;; equivalent + proof-find-theorems-command 'proof-find-theorems-form ;; search form proof-shell-start-silent-cmd "disable_pr" proof-shell-stop-silent-cmd "enable_pr" ;; command hooks @@ -136,7 +141,6 @@ See -k option for Isabelle interface script." ;; span menu proof-script-span-context-menu-extensions 'isabelle-create-span-menu)) - (defun isar-shell-mode-config-set-variables () "Configure generic proof shell mode variables for Isabelle/Isar." (setq @@ -168,7 +172,6 @@ See -k option for Isabelle interface script." proof-shell-error-regexp "\364\\*\\*\\*\\|\^AM\\*\\*\\*" proof-shell-abort-goal-regexp nil ; n.a. - ;; pg-next-error-regexp "\\((line \\([0-9]+\\) of \"[^\"]+\")\\)" pg-next-error-filename-regexp "\\((line [0-9]+ of \"\\([^\"]+\\)\")\\)" |