src/Tools/VSCode/src/server.scala
changeset 64667 cdb0d559a24b
parent 64655 ea34f36ff6a5
child 64673 b5965890e54d
     1.1 --- a/src/Tools/VSCode/src/server.scala	Fri Dec 23 19:07:54 2016 +0100
     1.2 +++ b/src/Tools/VSCode/src/server.scala	Fri Dec 23 19:19:59 2016 +0100
     1.3 @@ -109,7 +109,7 @@
     1.4    def rendering_offset(node_pos: Line.Node_Position): Option[(VSCode_Rendering, Text.Offset)] =
     1.5      for {
     1.6        model <- state.value.models.get(node_pos.name)
     1.7 -      rendering = model.rendering(options)
     1.8 +      rendering = model.rendering(options, text_length)
     1.9        offset <- model.doc.offset(node_pos.pos, text_length)
    1.10      } yield (rendering, offset)
    1.11