equal
deleted
inserted
replaced
18 val FILES = "PIDE/files" |
18 val FILES = "PIDE/files" |
19 val MARKUP = "PIDE/markup" |
19 val MARKUP = "PIDE/markup" |
20 val MESSAGES = "PIDE/messages" |
20 val MESSAGES = "PIDE/messages" |
21 val DOCUMENT_PREFIX = "document/" |
21 val DOCUMENT_PREFIX = "document/" |
22 val DOCUMENT_LATEX = DOCUMENT_PREFIX + "latex" |
22 val DOCUMENT_LATEX = DOCUMENT_PREFIX + "latex" |
23 val DOCUMENT_CITATIONS = DOCUMENT_PREFIX + "citations" |
|
24 val THEORY_PREFIX: String = "theory/" |
23 val THEORY_PREFIX: String = "theory/" |
25 val PROOFS_PREFIX: String = "proofs/" |
24 val PROOFS_PREFIX: String = "proofs/" |
26 |
25 |
27 def explode_name(s: String): List[String] = space_explode('/', s) |
26 def explode_name(s: String): List[String] = space_explode('/', s) |
28 def implode_name(elems: Iterable[String]): String = elems.mkString("/") |
27 def implode_name(elems: Iterable[String]): String = elems.mkString("/") |