equal
deleted
inserted
replaced
13 |
13 |
14 object Export |
14 object Export |
15 { |
15 { |
16 /* artefact names */ |
16 /* artefact names */ |
17 |
17 |
18 val MARKUP = "markup.yxml" |
18 val MARKUP = "PIDE/markup" |
19 val MESSAGES = "messages.yxml" |
19 val MESSAGES = "PIDE/messages" |
20 val DOCUMENT_PREFIX = "document/" |
20 val DOCUMENT_PREFIX = "document/" |
21 val THEORY_PREFIX: String = "theory/" |
21 val THEORY_PREFIX: String = "theory/" |
22 val PROOFS_PREFIX: String = "proofs/" |
22 val PROOFS_PREFIX: String = "proofs/" |
23 |
23 |
24 def explode_name(s: String): List[String] = space_explode('/', s) |
24 def explode_name(s: String): List[String] = space_explode('/', s) |