src/Tools/VSCode/src/server.scala

       rendering = model.rendering()
       offset <- model.content.doc.offset(node_pos.pos)
     } yield (rendering, offset)
 
   private val dynamic_output = Dynamic_Output(this)
-  private val dynamic_preview = Dynamic_Preview(this)
 
 
   /* input from client or file-system */
 
   private val delay_input: Standard_Thread.Delay =

   private def update_caret(caret: Option[(JFile, Line.Position)])
   {
     resources.update_caret(caret)
     delay_caret_update.invoke()
     delay_input.invoke()
+  }
+
+
+  /* preview */
+
+  private lazy val preview = new Preview(resources)
+
+  private lazy val delay_preview: Standard_Thread.Delay =
+    Standard_Thread.delay_last(options.seconds("vscode_output_delay"), channel.Error_Logger)
+    {
+      if (preview.flush(channel)) delay_preview.invoke()
+    }
+
+  private def request_preview(file: JFile, column: Int)
+  {
+    preview.request(file, column)
+    delay_preview.invoke()
   }
 
 
   /* output to client */
 

 
       session.commands_changed += prover_output
       session.all_messages += syslog
 
       dynamic_output.init()
-      dynamic_preview.init()
 
       var session_phase: Session.Consumer[Session.Phase] = null
       session_phase =
         Session.Consumer(getClass.getName) {
           case Session.Ready =>

       case Some(session) =>
         session.commands_changed -= prover_output
         session.all_messages -= syslog
 
         dynamic_output.exit()
-        dynamic_preview.exit()
 
         delay_load.revoke()
         file_watcher.shutdown()
         delay_input.revoke()
         delay_output.revoke()
         delay_caret_update.revoke()
+        delay_preview.revoke()
 
         val rc = session.stop()
         if (rc == 0) reply("") else reply("Prover shutdown failed: return code " + rc)
         None
       case None =>

           case Protocol.Completion(id, node_pos) => completion(id, node_pos)
           case Protocol.Hover(id, node_pos) => hover(id, node_pos)
           case Protocol.GotoDefinition(id, node_pos) => goto_definition(id, node_pos)
           case Protocol.DocumentHighlights(id, node_pos) => document_highlights(id, node_pos)
           case Protocol.Caret_Update(caret) => update_caret(caret)
+          case Protocol.Preview_Request(file, column) => request_preview(file, column)
           case _ => log("### IGNORED")
         }
       }
       catch { case exn: Throwable => channel.log_error_message(Exn.message(exn)) }
     }