src/Pure/Thy/sessions.scala
changeset 73718 ecb31c3bf980
parent 73701 d83e7e444b43
child 73814 c8b4a4f69068
--- a/src/Pure/Thy/sessions.scala	Mon May 17 15:01:37 2021 +0200
+++ b/src/Pure/Thy/sessions.scala	Mon May 17 16:15:25 2021 +0200
@@ -514,11 +514,11 @@
         case doc => error("Bad document specification " + quote(doc))
       }
 
-    def document_variants: List[Presentation.Document_Variant] =
+    def document_variants: List[Document_Build.Document_Variant] =
     {
       val variants =
         Library.space_explode(':', options.string("document_variants")).
-          map(Presentation.Document_Variant.parse)
+          map(Document_Build.Document_Variant.parse)
 
       val dups = Library.duplicates(variants.map(_.name))
       if (dups.nonEmpty) error("Duplicate document variants: " + commas_quote(dups))
@@ -526,7 +526,7 @@
       variants
     }
 
-    def documents: List[Presentation.Document_Variant] =
+    def documents: List[Document_Build.Document_Variant] =
     {
       val variants = document_variants
       if (!document_enabled || document_files.isEmpty) Nil else variants
@@ -1429,10 +1429,10 @@
         db.using_statement(
           Export.Data.table.delete(Export.Data.session_name.where_equal(name)))(_.execute())
 
-        db.create_table(Presentation.Data.table)
+        db.create_table(Document_Build.Data.table)
         db.using_statement(
-          Presentation.Data.table.delete(
-            Presentation.Data.session_name.where_equal(name)))(_.execute())
+          Document_Build.Data.table.delete(
+            Document_Build.Data.session_name.where_equal(name)))(_.execute())
       }
     }