src/Tools/VSCode/src/vscode_rendering.scala
changeset 64706 3ebf9f8299df
parent 64704 08c2d80428ff
child 64730 76996d915894
equal deleted inserted replaced
64704:08c2d80428ff 64706:3ebf9f8299df
    86         catch { case ERROR(_) => None }
    86         catch { case ERROR(_) => None }
    87       Line.Node_Range(File.platform_url(name),
    87       Line.Node_Range(File.platform_url(name),
    88         opt_text match {
    88         opt_text match {
    89           case Some(text) if range.start > 0 =>
    89           case Some(text) if range.start > 0 =>
    90             val chunk = Symbol.Text_Chunk(text)
    90             val chunk = Symbol.Text_Chunk(text)
    91             val doc = Line.Document(text, model.doc.text_length)
    91             val doc = Line.Document(text, resources.text_length)
    92             doc.range(chunk.decode(range))
    92             doc.range(chunk.decode(range))
    93           case _ =>
    93           case _ =>
    94             Line.Range(Line.Position((line1 - 1) max 0))
    94             Line.Range(Line.Position((line1 - 1) max 0))
    95         })
    95         })
    96     }
    96     }