equal
deleted
inserted
replaced
13 |
13 |
14 object Export |
14 object Export |
15 { |
15 { |
16 /* artefact names */ |
16 /* artefact names */ |
17 |
17 |
|
18 val DOCUMENT_ID = "PIDE/document_id" |
|
19 val FILES = "PIDE/files" |
18 val MARKUP = "PIDE/markup" |
20 val MARKUP = "PIDE/markup" |
19 val FILES = "PIDE/files" |
|
20 val MESSAGES = "PIDE/messages" |
21 val MESSAGES = "PIDE/messages" |
21 val DOCUMENT_PREFIX = "document/" |
22 val DOCUMENT_PREFIX = "document/" |
22 val CITATIONS = DOCUMENT_PREFIX + "citations" |
23 val CITATIONS = DOCUMENT_PREFIX + "citations" |
23 val THEORY_PREFIX: String = "theory/" |
24 val THEORY_PREFIX: String = "theory/" |
24 val PROOFS_PREFIX: String = "proofs/" |
25 val PROOFS_PREFIX: String = "proofs/" |