--- a/src/Pure/Thy/export.scala Wed Aug 16 14:50:17 2023 +0200
+++ b/src/Pure/Thy/export.scala Thu Aug 17 14:43:45 2023 +0200
@@ -14,12 +14,12 @@
object Export {
/* artefact names */
- val DOCUMENT_ID = "PIDE/document_id"
- val FILES = "PIDE/files"
- val MARKUP = "PIDE/markup"
- val MESSAGES = "PIDE/messages"
- val DOCUMENT_PREFIX = "document/"
- val DOCUMENT_LATEX = DOCUMENT_PREFIX + "latex"
+ val DOCUMENT_ID: String = "PIDE/document_id"
+ val FILES: String = "PIDE/files"
+ val MARKUP: String = "PIDE/markup"
+ val MESSAGES: String = "PIDE/messages"
+ val DOCUMENT_PREFIX: String = "document/"
+ val DOCUMENT_LATEX: String = DOCUMENT_PREFIX + "latex"
val THEORY_PREFIX: String = "theory/"
val PROOFS_PREFIX: String = "proofs/"