File used to test new parsing mechanism.

1 files changed, 37 insertions, 0 deletions

diff --git a/etc/isar/Parsing.thy b/etc/isar/Parsing.thy
new file mode 100644
index 00000000..4bd7e0a3
--- /dev/null
+++ b/etc/isar/Parsing.thy
@@ -0,0 +1,37 @@
+(* Not really a theory of parsing, but a test of Proof General's
+   parsing for Isabelle/Isar.... *)
+
+(* First, start with successive comments before a real command *)
+
+theory Parsing = Main:
+
+(* Then a comment *after* a command.  Also one which mentions
+   the names of commands, such as theory or theorem or proof itself,
+   never mind thus assume end qed. *)
+
+text {* Isar theories can have arbitrary literal text,
+          so the text must be ignored as well; thus. *}
+
+(* Let's do my favourite proof. *)
+
+theorem and_comms: "A & B --> B & A"
+proof
+  assume "A & B"  (* it's "important" that we test "strings" I guess *)
+    thus "B & A"
+    proof
+      assume A B (* blah boo bah *)
+	show ?thesis (* bah boo bah *)
+	..
+    qed
+qed
+
+(* Now the end of file is coming up.  Funny things happen
+   because PG only knows how commands start, not how they end.
+*)
+
+end
+(* That's the final command and it includes any text which follows it.
+   An oddity is that if there is a syntax error - unclosed comment
+   or whatever, after the last end, PG will say that it can't find
+   a complete command! *)
+