Refactor several variable names; clean up, doc subterm markup and output display.

2 files changed, 10 insertions, 10 deletions

diff --git a/lego/lego-syntax.el b/lego/lego-syntax.el
index e1ff82a4..bdb30a72 100644
--- a/lego/lego-syntax.el
+++ b/lego/lego-syntax.el
@@ -82,7 +82,7 @@
      ;; Special hacks!!
      (cons "Discharge.." 'font-lock-keyword-face)
      (cons "\\*\\*\\* QED \\*\\*\\*" 'font-lock-keyword-face))
-  "*Font-lock table for LEGO terms.")
+  "*Font-lock table for LEGO terms (displayed in output buffers).")
 
 ;; Instead of "[^:]+", it may be better to use "lego-id". Furthermore,
 ;; it might be safer to append "\\s-*:".
diff --git a/lego/lego.el b/lego/lego.el
index 18d5e728..f170c5a2 100644
--- a/lego/lego.el
+++ b/lego/lego.el
@@ -318,7 +318,7 @@ Checks the width in the `proof-goals-buffer'"
 	proof-completed-proof-behaviour 'closeany ; new in 3.0
 	proof-count-undos-fn 'lego-count-undos
 	proof-find-and-forget-fn 'lego-find-and-forget
-        proof-goal-hyp-fn 'lego-goal-hyp
+        pg-topterm-goalhyp-fn 'lego-goal-hyp
 	proof-state-preserving-p 'lego-state-preserving-p)
 
   (setq	proof-save-command-regexp lego-save-command-regexp
@@ -397,12 +397,12 @@ We assume that module identifiers coincide with file names."
         proof-shell-error-regexp lego-error-regexp
 	proof-shell-interrupt-regexp lego-interrupt-regexp
         proof-shell-assumption-regexp lego-id
-        proof-shell-first-special-char ?\360
+        pg-subterm-first-special-char ?\360
         proof-shell-wakeup-char ?\371
-        proof-shell-start-char ?\372
-        proof-shell-end-char ?\373
-        proof-shell-field-char ?\374
-        proof-shell-goal-char ?\375
+        pg-subterm-start-char ?\372
+        pg-subterm-sep-char ?\373
+        pg-subterm-end-char ?\374
+        pg-topterm-char ?\375
 	proof-shell-eager-annotation-start "\376"
 	proof-shell-eager-annotation-start-length 1
 	proof-shell-eager-annotation-end "\377"
@@ -414,7 +414,7 @@ We assume that module identifiers coincide with file names."
 	proof-shell-pre-sync-init-cmd "Configure AnnotateOn;"
         proof-shell-init-cmd lego-process-config
 	proof-shell-restart-cmd lego-process-config
-	proof-analyse-using-stack nil
+	pg-subterm-anns-use-stack nil
 	proof-shell-process-output-system-specific lego-shell-process-output
         lego-shell-current-line-width nil
 
@@ -436,8 +436,8 @@ We assume that module identifiers coincide with file names."
   (proof-shell-config-done))
 
 (defun lego-goals-mode-config ()
-  (setq pbp-change-goal "Next %s;"
-	pbp-error-regexp lego-error-regexp)
+  (setq pg-goals-change-goal "Next %s;"
+	pg-goals-error-regexp lego-error-regexp)
   (setq font-lock-keywords lego-font-lock-terms)
   (lego-init-syntax-table)
   (proof-goals-config-done))