# HG changeset patch
# User paulson
# Date 882956547 -3600
# Node ID 9c5a0eef74ff6c379c11e650c5c91b1669bba22c
# Parent  b3e5857d8d99ecaa28fa60e8c50697225e374939
More restrictive patterns to prevent changing comments

diff -r b3e5857d8d99 -r 9c5a0eef74ff lib/scripts/expandshort.pl
--- a/lib/scripts/expandshort.pl	Wed Dec 24 10:02:30 1997 +0100
+++ b/lib/scripts/expandshort.pl	Wed Dec 24 10:42:27 1997 +0100
@@ -3,6 +3,8 @@
 #
 # expandshort.pl - expand shorthand goal commands
 #
+# in "be ... i;" -> "by (etac ... i);" the "..." phrase is not allowed to
+#   contain punctuation.  Otherwise, comments can be affected!
 
 sub expandshort {
     my ($file) = @_;
@@ -18,15 +20,15 @@
     s/ *\(Safe_tac\)/ Safe_tac/sg;
     s/\bby\(/by (/sg;
     s/\bba\b *(\d+);/by (assume_tac \1);/sg;
-    s/\bbr\b *([^;]*) (\d+);/by (rtac \1 \2);/sg;
-    s/\bbrs\b *([^;]*) (\d+);/by (resolve_tac \1 \2);/sg;
-    s/\bbd\b *([^;]*) (\d+);/by (dtac \1 \2);/sg;
-    s/\bbds\b *([^;]*) (\d+);/by (dresolve_tac \1 \2);/sg;
-    s/\bbe\b *([^;]*) (\d+);/by (etac \1 \2);/sg;
-    s/\bbes\b *([^;]*) (\d+);/by (eresolve_tac \1 \2);/sg;
-    s/\bbw\b *([^;]*);/by (rewtac \1);/sg;
-    s/\bbws\b *([^;]*);/by (rewrite_goals_tac \1);/sg;
-    s/\bauto *\(\)/by (Auto_tac())/sg;
+    s/\bbr\b *([^;.*!]*) (\d+);/by (rtac \1 \2);/sg;
+    s/\bbrs\b *([^;.*!]*) (\d+);/by (resolve_tac \1 \2);/sg;
+    s/\bbd\b *([^;.*!]*) (\d+);/by (dtac \1 \2);/sg;
+    s/\bbds\b *([^;.*!]*) (\d+);/by (dresolve_tac \1 \2);/sg;
+    s/\bbe\b *([^;.*!]*) (\d+);/by (etac \1 \2);/sg;
+    s/\bbes\b *([^;.*!]*) (\d+);/by (eresolve_tac \1 \2);/sg;
+    s/\bbw\b *([^;.*!]*);/by (rewtac \1);/sg;
+    s/\bbws\b *([^;.*!]*);/by (rewrite_goals_tac \1);/sg;
+    s/\bauto *\(\)/by Auto_tac/sg;
     s/dresolve_tac *\[(\w+)\] */dtac \1 /sg;
     s/eresolve_tac *\[(\w+)\] */etac \1 /sg;
     s/resolve_tac *\[(\w+)\] */rtac \1 /sg;