--- a/src/Pure/Thy/sessions.scala Wed Nov 18 15:47:53 2020 +0100
+++ b/src/Pure/Thy/sessions.scala Wed Nov 18 15:52:12 2020 +0100
@@ -492,11 +492,11 @@
case doc => error("Bad document specification " + quote(doc))
}
- def documents_variants: List[Present.Document_Variant] =
+ def documents_variants: List[Presentation.Document_Variant] =
{
val variants =
Library.space_explode(':', options.string("document_variants")).
- map(Present.Document_Variant.parse)
+ map(Presentation.Document_Variant.parse)
val dups = Library.duplicates(variants.map(_.name))
if (dups.nonEmpty) error("Duplicate document variants: " + commas_quote(dups))
@@ -504,7 +504,7 @@
variants
}
- def documents: List[Present.Document_Variant] =
+ def documents: List[Presentation.Document_Variant] =
{
val variants = documents_variants
if (!document_enabled || document_files.isEmpty) Nil else variants