Added clear_response_buffer regexp, use_thy_and_update now in ProofGeneral

2 files changed, 10 insertions, 16 deletions

diff --git a/isa/isa-syntax.el b/isa/isa-syntax.el
index c00918dc..1bf2775f 100644
--- a/isa/isa-syntax.el
+++ b/isa/isa-syntax.el
@@ -104,26 +104,17 @@
 
 (defconst isa-id proof-id)
 
-(defconst isa-ids (proof-ids isa-id))
+(defconst isa-ids (proof-ids isa-id "[ \t]*")
+  "Matches a sequence of identifiers separated by whitespace.")
 
-;; FIXME: rubbish syntax here.
-(defun isa-abstr-regexp (paren char)
-    (concat paren "\\s-*\\(" isa-ids "\\)\\s-*" char))
+(defun isa-binder-regexp (binder dot)
+    (concat binder "\\s-*\\(" isa-ids "\\)\\s-*" dot))
 
-;; FIXME: rubbish syntax here.
 (defvar isa-font-lock-terms
   (list
    ;; lambda binders
-   (list (concat "\%\\s-*\\(" isa-ids "\\)\\.") 1
-	 'proof-declaration-name-face)
-
-   ;; Pi binders
-   (list (isa-abstr-regexp "(" ":") 1 'proof-declaration-name-face)
-   
-   ;; Kinds
-   (cons (concat "\\<Prop\\>\\|\\<Set\\>\\|\\<Type\\s-*\\(("
-		   isa-id ")\\)?") 'font-lock-type-face))
-  "*Font-lock table for Isa terms.")
+   (list (isa-binder-regexp "\%" "\\.") 1 'proof-declaration-name-face))
+  "*Font-lock table for Isabelle terms.")
 
 (defconst isa-save-command-regexp
   (concat "^" (proof-ids-to-regexp isa-keywords-save)))
diff --git a/isa/isa.el b/isa/isa.el
index 28e1c1a9..534124ee 100644
--- a/isa/isa.el
+++ b/isa/isa.el
@@ -183,6 +183,9 @@ no regular or easily discernable structure."
    proof-shell-eager-annotation-start   "\360\\|\362\\|\364"
    proof-shell-eager-annotation-end     "\361\\|\363\\|\365"
 
+   ;; Some messages delineated by eager annotations
+   proof-shell-clear-response-regexp    "Proof General, please clear the response buffer."
+
    ;; Tested values of proof-shell-eager-annotation-start: 
    ;; "^\\[opening \\|^###\\|^Reading\\|^Proof General\\|^Not reading"
    ;; "^---\\|^\\[opening "
@@ -224,7 +227,7 @@ no regular or easily discernable structure."
 ;;; So we rely on some hacked versions.
 ;;;
 
-(defcustom isa-usethy-notopml-command "use_thy_and_update \"%s\";"
+(defcustom isa-usethy-notopml-command "ProofGeneral.use_thy_and_update \"%s\";"
   "Sent to Isabelle to process theory for this ML file, and all ancestors."
   :type 'string
   :group 'isabelle-config)