aboutsummaryrefslogtreecommitdiffhomepage
path: root/etc
diff options
context:
space:
mode:
Diffstat (limited to 'etc')
-rw-r--r--etc/isar/XEmacsSyntacticContextProb.thy20
1 files changed, 20 insertions, 0 deletions
diff --git a/etc/isar/XEmacsSyntacticContextProb.thy b/etc/isar/XEmacsSyntacticContextProb.thy
new file mode 100644
index 00000000..214cc0a3
--- /dev/null
+++ b/etc/isar/XEmacsSyntacticContextProb.thy
@@ -0,0 +1,20 @@
+(* Demonstrates a bug with XEmacs 21.1: after procesing, between
+ two terms, buffer-syntactic-context returns "string".
+ But _before_ processing, it correctly returns "nil".
+ Even when regions are removed, still get "string" returned
+ after processing started.
+
+ Bug doesn't occur in GNU Emacs (using imp of buffer-syntactic context
+ provided in proof-compat.el), nor in XEmacs 21.4
+
+ Workaround added
+*)
+
+theory XEmacsSyntacticContextProb = Main:
+
+term "
+(f x)"
+
+term "(f x)"
+
+end