diff -r d637e60427db -r ec761aa6cc64 src/Pure/Thy/export.scala
--- 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/"