1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
|
(* 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. *}
(* 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"
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
(* Another thing: nesting with { and } can be tricky. *)
theorem and_comms_again: "A & B --> B & A"
proof
assume "A & B"
thus "B & A"
proof {
assume A B
show ?thesis
..
} 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! *)
|
