# HG changeset patch
# User wenzelm
# Date 1571568996 -7200
# Node ID 935c78a90ee021acc20407b2d5fa3e04793f717e
# Parent  3ed399935d7c602dba239e258b23b1ddc5d3dda5
more kinds, notably for Isabelle/MMT;

diff -r 3ed399935d7c -r 935c78a90ee0 src/Pure/Thy/export_theory.scala
--- a/src/Pure/Thy/export_theory.scala	Sat Oct 19 16:16:24 2019 +0200
+++ b/src/Pure/Thy/export_theory.scala	Sun Oct 20 12:56:36 2019 +0200
@@ -184,6 +184,9 @@
     val CLASS = Value("class")
     val LOCALE = Value("locale")
     val LOCALE_DEPENDENCY = Value("locale_dependency")
+    val DOCUMENT_HEADING = Value("document_heading")
+    val DOCUMENT_TEXT = Value("document_text")
+    val PROOF_TEXT = Value("proof_text")
   }
 
   sealed case class Entity(