src/Tools/VSCode/src/document_model.scala

--- a/src/Tools/VSCode/src/document_model.scala	Tue Dec 20 21:35:56 2016 +0100
+++ b/src/Tools/VSCode/src/document_model.scala	Tue Dec 20 22:24:16 2016 +0100
@@ -52,7 +52,10 @@
   def unchanged: Document_Model = if (changed) copy(changed = false) else this
 
 
-  /* snapshot */
+  /* snapshot and rendering */
 
   def snapshot(): Document.Snapshot = session.snapshot(node_name, text_edits)
+
+  def rendering(options: Options): VSCode_Rendering =
+    new VSCode_Rendering(snapshot(), options, session.resources)
 }