equal
deleted
inserted
replaced
|
1 (* Title: Pure/ProofGeneral/pgip_markup.ML |
|
2 ID: $Id$ |
|
3 Author: David Aspinall |
|
4 |
|
5 PGIP abstraction: document markup for proof scripts (in progress). |
|
6 *) |
|
7 |
|
8 signature PGIPMARKUP = |
|
9 sig |
|
10 val markup_elements : string list |
|
11 end |
|
12 |
|
13 structure PgipMarkup : PGIPMARKUP = |
|
14 struct |
|
15 (* Names of all PGIP document markup elements *) |
|
16 val markup_elements = |
|
17 [ |
|
18 "opengoal", |
|
19 "proofstep", |
|
20 "closegoal", |
|
21 "comment", |
|
22 "doccomment", |
|
23 "whitespace", |
|
24 "litcomment", |
|
25 "spuriouscmd", |
|
26 "badcmd", |
|
27 "opentheory", |
|
28 "theoryitem", |
|
29 "closetheory", |
|
30 "metainfo" (* non-document text *) |
|
31 ] |
|
32 |
|
33 end |