src/Tools/VSCode/src/vscode_rendering.scala

 {
   /* diagnostics */
 
   def diagnostics: List[Text.Info[Command.Results]] =
     snapshot.cumulate[Command.Results](
-      model.doc.text_range, Command.Results.empty, VSCode_Rendering.diagnostics_elements, _ =>
+      model.content.text_range, Command.Results.empty, VSCode_Rendering.diagnostics_elements, _ =>
       {
         case (res, Text.Info(_, msg @ XML.Elem(Markup(_, Markup.Serial(i)), body)))
         if body.nonEmpty => Some(res + (i -> msg))
 
         case _ => None

 
   def diagnostics_output(results: List[Text.Info[Command.Results]]): List[Protocol.Diagnostic] =
   {
     (for {
       Text.Info(text_range, res) <- results.iterator
-      range = model.doc.range(text_range)
+      range = model.content.doc.range(text_range)
       (_, XML.Elem(Markup(name, _), body)) <- res.iterator
     } yield {
       val message = Pretty.string_of(body, margin = diagnostics_margin)
       val severity = VSCode_Rendering.message_severity.get(name)
       Protocol.Diagnostic(range, message, severity = severity)