From e9810344a33d604d78fb487ef3e09a04a85a1bfd Mon Sep 17 00:00:00 2001
From: David Aspinall
Date: Wed, 17 Nov 1999 21:31:58 +0000
Subject: Fix to -with-hole regexps

---
 demoisa/demoisa-easy.el | 4 ++--
 demoisa/demoisa.el      | 4 ++--
 2 files changed, 4 insertions(+), 4 deletions(-)

diff --git a/demoisa/demoisa-easy.el b/demoisa/demoisa-easy.el
index 64710ff1..1ee49526 100644
--- a/demoisa/demoisa-easy.el
+++ b/demoisa/demoisa-easy.el
@@ -25,8 +25,8 @@
  proof-comment-end               "*)"
  proof-goal-command-regexp       "^Goal"
  proof-save-command-regexp       "^qed"
- proof-goal-with-hole-regexp     "^Goal \\(\\(\"%s\"\\)\\)"
- proof-save-with-hole-regexp     "^qed \\(\\(\"%s\"\\)\\)"
+ proof-goal-with-hole-regexp     "qed_goal \"\\(\\(.*\\)\\)\""
+ proof-save-with-hole-regexp     "qed \"\\(\\(.*\\)\\)\"
  proof-non-undoables-regexp      "undo\\|back"
  proof-goal-command              "Goal \"%s\";"
  proof-save-command              "qed \"%s\";"
diff --git a/demoisa/demoisa.el b/demoisa/demoisa.el
index 7f77b5c5..c5ab933f 100644
--- a/demoisa/demoisa.el
+++ b/demoisa/demoisa.el
@@ -114,8 +114,8 @@
    proof-comment-end		"*)"
    proof-goal-command-regexp    "^Goal"
    proof-save-command-regexp    "^qed"
-   proof-goal-with-hole-regexp  "^Goal \\(\\(\"%s\"\\)\\)"
-   proof-save-with-hole-regexp  "^qed \\(\\(\"%s\"\\)\\)"
+   proof-goal-with-hole-regexp  "qed_goal \"\\(\\(.*\\)\\)\""
+   proof-save-with-hole-regexp  "qed \"\\(\\(.*\\)\\)\""
    proof-non-undoables-regexp   "undo\\|back"
    proof-undo-n-times-cmd	"pg_repeat undo %s;"
    proof-showproof-command	"pr()"
-- 
cgit v1.2.3