o added support for byte-compilation

o removed hhg tags in todo
o fixed font-lock for FSF Emacs 20.2
o ensured that goals buffer is updated for longer queues
o fixed a bug in proof-universal-keys-only-mode

2 files changed, 13 insertions, 11 deletions

diff --git a/lego/lego-syntax.el b/lego/lego-syntax.el
index f3a8f767..34608afb 100644
--- a/lego/lego-syntax.el
+++ b/lego/lego-syntax.el
@@ -64,7 +64,7 @@
 
    ; lambda binders
      (list (lego-decl-defn-regexp "[:|?]") 1
-	   'proof-declaration-name-face)
+	   ''proof-declaration-name-face)
 
      ; let binders
      (list lego-definiendum-alternative-regexp 1 'font-lock-function-name-face)
@@ -72,7 +72,7 @@
 
      ; Pi and Sigma binders
      (list (concat "[{<]\\s *\\(" lego-ids "\\)") 1
-	   'proof-declaration-name-face)
+	   ''proof-declaration-name-face)
    
      ;; Kinds
      (cons (concat "\\<Prop\\>\\|\\<Type\\s *\\(("
@@ -82,12 +82,12 @@
 ;; Instead of "[^:]+", it may be better to use "lego-id". Furthermore,
 ;; it might be safer to append "\\s-*:".
 (defconst lego-goal-with-hole-regexp
-  (concat "\\(" (ids-to-regexp lego-keywords-goal) "\\)\\s-+\\([^:]+\\)")
+  (concat "\\(" (proof-ids-to-regexp lego-keywords-goal) "\\)\\s-+\\([^:]+\\)")
   "Regular expression which matches an entry in `lego-keywords-goal'
   and the name of the goal.") 
 
 (defconst lego-save-with-hole-regexp
-  (concat "\\(" (ids-to-regexp lego-keywords-save) "\\)\\s-+\\([^;]+\\)")
+  (concat "\\(" (proof-ids-to-regexp lego-keywords-save) "\\)\\s-+\\([^;]+\\)")
   "Regular expression which matches an entry in
   `lego-keywords-save' and the name of the goal.")
 
@@ -95,8 +95,8 @@
    (append
     lego-font-lock-terms
     (list
-     (cons (ids-to-regexp lego-keywords) 'font-lock-keyword-face)
-     (cons (ids-to-regexp lego-tacticals) 'proof-tacticals-name-face)
+     (cons (proof-ids-to-regexp lego-keywords) 'font-lock-keyword-face)
+     (cons (proof-ids-to-regexp lego-tacticals) ''proof-tacticals-name-face)
      (list lego-goal-with-hole-regexp 2 'font-lock-function-name-face)
      (list lego-save-with-hole-regexp 2 'font-lock-function-name-face))))
      
diff --git a/lego/lego.el b/lego/lego.el
index 3674979d..a1c5b234 100644
--- a/lego/lego.el
+++ b/lego/lego.el
@@ -135,15 +135,15 @@
   "*Regular expression indicating that the proof has been completed.")
 
 (defvar lego-save-command-regexp
-  (concat "^" (ids-to-regexp lego-keywords-save)))
+  (concat "^" (proof-ids-to-regexp lego-keywords-save)))
 (defvar lego-goal-command-regexp
-  (concat "^" (ids-to-regexp lego-keywords-goal)))
+  (concat "^" (proof-ids-to-regexp lego-keywords-goal)))
 
 (defvar lego-kill-goal-command "KillRef;")
 (defvar lego-forget-id-command "Forget ")
 
 (defvar lego-undoable-commands-regexp
-  (ids-to-regexp '("Dnf" "Refine" "Intros" "intros" "Next" "Normal"
+  (proof-ids-to-regexp '("Dnf" "Refine" "Intros" "intros" "Next" "Normal"
   "Qrepl" "Claim" "For" "Repeat" "Succeed" "Fail" "Try" "Assumption"
   "UTac" "Qnify" "qnify" "andE" "andI" "exE" "exI" "orIL" "orIR" "orE" "ImpI"
   "impE" "notI" "notE" "allI" "allE" "Expand" "Induction" "Immed"
@@ -155,7 +155,7 @@
 
 (defvar lego-outline-regexp
   (concat "[[*]\\|"
-	  (ids-to-regexp 
+	  (proof-ids-to-regexp 
 	   '("Discharge" "DischargeKeep" "Freeze" "$?Goal" "Module" "Record" "Inductive"
      "Unfreeze"))))
 
@@ -184,6 +184,7 @@
   (define-derived-mode lego-response-mode proof-response-mode
     "LEGOResp" nil
     (setq font-lock-keywords lego-font-lock-terms)
+    (lego-init-syntax-table)
     (proof-response-config-done)))
   
 (define-derived-mode lego-pbp-mode pbp-mode
@@ -410,7 +411,7 @@
 	proof-save-with-hole-regexp lego-save-with-hole-regexp
 	proof-goal-with-hole-regexp lego-goal-with-hole-regexp
 	proof-kill-goal-command lego-kill-goal-command
-	proof-commands-regexp (ids-to-regexp lego-commands))
+	proof-commands-regexp (proof-ids-to-regexp lego-commands))
 
   (lego-init-syntax-table)
 
@@ -537,6 +538,7 @@ We assume that module identifiers coincide with file names."
   (setq pbp-change-goal "Next %s;"
 	pbp-error-regexp lego-error-regexp)
   (setq font-lock-keywords lego-font-lock-terms)
+  (lego-init-syntax-table)
   (proof-goals-config-done))