From fecff511bb9fd00267ad9d0d547a64e012480908 Mon Sep 17 00:00:00 2001
From: David Aspinall
Date: Tue, 14 Aug 2007 14:12:40 +0000
Subject: Add support for sending back literal commands reusing PBP markup
 mechanisms.

---
 plastic/plastic.el | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'plastic')

diff --git a/plastic/plastic.el b/plastic/plastic.el
index e6bf14d4..800ac869 100644
--- a/plastic/plastic.el
+++ b/plastic/plastic.el
@@ -377,7 +377,7 @@ Given is the first SPAN which needs to be undone."
   (setq proof-goal-command-p 'plastic-goal-command-p
 	proof-count-undos-fn 'plastic-count-undos
 	proof-find-and-forget-fn 'plastic-find-and-forget
-        pg-topterm-goalhyp-fn 'plastic-goal-hyp
+        pg-topterm-goalhyplit-fn 'plastic-goal-hyp
 	proof-state-preserving-p 'plastic-state-preserving-p)
 
   (setq	proof-save-command-regexp plastic-save-command-regexp
@@ -491,7 +491,7 @@ We assume that module identifiers coincide with file names."
         pg-subterm-start-char ?\372
         pg-subterm-sep-char ?\373
         pg-subterm-end-char ?\374
-        pg-topterm-char ?\375
+        pg-topterm-regexp "\375"
         proof-shell-eager-annotation-start "\376"
 	;; FIXME da: if p-s-e-a-s is implemented, you should set
 	;; proof-shell-eager-annotation-start-length=1 to
-- 
cgit v1.2.3