# HG changeset patch
# User wenzelm
# Date 1606305963 -3600
# Node ID 79a19657c1709c0d1e005dc7d6fdd5e7a7181c26
# Parent  1c42ac589fa0a303652cb33cfed9a82582f09714
clarified names;

diff -r 1c42ac589fa0 -r 79a19657c170 src/Pure/Thy/export.scala
--- a/src/Pure/Thy/export.scala	Wed Nov 25 12:57:45 2020 +0100
+++ b/src/Pure/Thy/export.scala	Wed Nov 25 13:06:03 2020 +0100
@@ -15,8 +15,8 @@
 {
   /* artefact names */
 
-  val MARKUP = "markup.yxml"
-  val MESSAGES = "messages.yxml"
+  val MARKUP = "PIDE/markup"
+  val MESSAGES = "PIDE/messages"
   val DOCUMENT_PREFIX = "document/"
   val THEORY_PREFIX: String = "theory/"
   val PROOFS_PREFIX: String = "proofs/"