From dc236b0cdbcec9ceae637fdb90f5aef46eecdb22 Mon Sep 17 00:00:00 2001
From: David Aspinall
Date: Fri, 12 Jul 2002 08:13:19 +0000
Subject: Add some nesting examples

---
 etc/isar/Parsing.thy | 15 +++++++++++++++
 1 file changed, 15 insertions(+)

diff --git a/etc/isar/Parsing.thy b/etc/isar/Parsing.thy
index 4bd7e0a3..2252d96c 100644
--- a/etc/isar/Parsing.thy
+++ b/etc/isar/Parsing.thy
@@ -12,6 +12,21 @@ theory Parsing = Main:
 text {* Isar theories can have arbitrary literal text,
           so the text must be ignored as well; thus. *}
 
+(* Those pieces of literal text are treated as another kind
+   of comment. What gets slight risky is when they're
+   text {* nested one inside the other. *}.
+   If Emacs confuses the two kinds of sequence, then
+   this can go wrong.
+*)
+
+text {* nesting (* may be the other way around *) *}
+
+(* The main type of comment (* may be nested *)
+   just like in SML. GNU Emacs supports this now, nicely,
+   but XEmacs doesn't, so colouration goes wrong.  
+   If there are any command names inside this comment
+   (e.g. theorem), it breaks the parser in XEmacs. *)
+
 (* Let's do my favourite proof. *)
 
 theorem and_comms: "A & B --> B & A"
-- 
cgit v1.2.3