Turned off C-c C-l; fixed syntax for old result form; proof-showproof-command.

2 files changed, 16 insertions, 6 deletions

diff --git a/isa/isa-syntax.el b/isa/isa-syntax.el
index 4645b4cf..342ba447 100644
--- a/isa/isa-syntax.el
+++ b/isa/isa-syntax.el
@@ -111,7 +111,7 @@
   :type '(repeat string))
 
 (defcustom isa-keywords-save
-  '("qed" "qed_spec_mp" "no_qed" "result()" "result ()")
+  '("qed" "qed_spec_mp" "no_qed" "result")
   ;; Related commands, but having different types, so PG
   ;; won't bother support them:
   ;; "uresult" "bind_thm" "store_thm"
@@ -155,8 +155,18 @@
 
 (defconst isa-string "\"\\(\\([^\\\"]\\|\\\\\"\\)*\\)\"")
 
-(defconst isa-save-command-regexp
-  (proof-anchor-regexp (proof-ids-to-regexp isa-keywords-save)))
+(defcustom isa-save-command-regexp
+  (proof-regexp-alt
+   (proof-anchor-regexp (proof-ids-to-regexp isa-keywords-save))
+   ;; match val ... = result blah
+   (proof-anchor-regexp
+    (concat
+     (proof-ids-to-regexp '("val")) ".+=\\s-*"
+     "\\(" (proof-ids-to-regexp isa-keywords-save) "\\)")))
+  "Regular expression used to match a qed/result."
+  :type 'regexp
+  :group 'isabelle-config)
+
 
 ;; CHECKED
 (defconst isa-save-with-hole-regexp
diff --git a/isa/isa.el b/isa/isa.el
index ae80f4c9..7440ac06 100644
--- a/isa/isa.el
+++ b/isa/isa.el
@@ -128,7 +128,7 @@ no regular or easily discernable structure."
    proof-indent-commands-regexp	(proof-ids-to-regexp isa-keywords)
    
    ;; proof engine commands
-   proof-proof-command		"pr()"
+   proof-showproof-command	"pr()"
    proof-goal-command		"Goal \"%s\";"
    proof-save-command		"qed \"%s\";"
    proof-context-command		"ProofGeneral.show_context()"
@@ -309,8 +309,8 @@ proof-shell-retract-files-regexp."
     "Isabelle script" nil
     (isa-mode-config)))
 
-(define-key isa-proofscript-mode-map
-  [(control c) (control l)] 'proof-prf)	; keybinding like Isamode
+; (define-key isa-proofscript-mode-map
+;  [(control c) (control l)] 'proof-prf)	; keybinding like Isamode