src/Pure/Tools/build_job.scala
changeset 73718 ecb31c3bf980
parent 73700 908351c8c0b1
child 73719 d4c7b88f56a0
--- a/src/Pure/Tools/build_job.scala	Mon May 17 15:01:37 2021 +0200
+++ b/src/Pure/Tools/build_job.scala	Mon May 17 16:15:25 2021 +0200
@@ -447,7 +447,7 @@
             using(store.open_database_context())(db_context =>
               {
                 val documents =
-                  Presentation.build_documents(session_name, deps, db_context,
+                  Document_Build.build_documents(session_name, deps, db_context,
                     output_sources = info.document_output,
                     output_pdf = info.document_output,
                     progress = progress,
@@ -460,7 +460,7 @@
           else (Nil, Nil)
         }
         catch {
-          case exn: Presentation.Build_Error => (exn.log_lines, List(exn.message))
+          case exn: Document_Build.Build_Error => (exn.log_lines, List(exn.message))
           case Exn.Interrupt.ERROR(msg) => (Nil, List(msg))
         }