src/Pure/Tools/build_job.scala

--- a/src/Pure/Tools/build_job.scala	Wed Dec 09 14:29:30 2020 +0100
+++ b/src/Pure/Tools/build_job.scala	Wed Dec 09 15:14:24 2020 +0100
@@ -118,10 +118,6 @@
             }
           }
         }
-      def make_rendering(snapshot: Document.Snapshot): Rendering =
-        new Rendering(snapshot, options, session) {
-          override def model: Document.Model = ???
-        }
 
       object Build_Session_Errors
       {
@@ -231,7 +227,7 @@
       session.finished_theories += Session.Consumer[Document.Snapshot]("finished_theories")
         {
           case snapshot =>
-            val rendering = make_rendering(snapshot)
+            val rendering = new Rendering(snapshot, options, session)
 
             def export(name: String, xml: XML.Body, compress: Boolean = true)
             {