src/Tools/VSCode/src/server.scala
changeset 64704 08c2d80428ff
parent 64703 a115391494ed
child 64706 3ebf9f8299df
     1.1 --- a/src/Tools/VSCode/src/server.scala	Thu Dec 29 21:54:04 2016 +0100
     1.2 +++ b/src/Tools/VSCode/src/server.scala	Thu Dec 29 22:10:29 2016 +0100
     1.3 @@ -101,7 +101,7 @@
     1.4    def rendering_offset(node_pos: Line.Node_Position): Option[(VSCode_Rendering, Text.Offset)] =
     1.5      for {
     1.6        model <- resources.get_model(node_pos.name)
     1.7 -      rendering = model.rendering(options)
     1.8 +      rendering = model.rendering()
     1.9        offset <- model.doc.offset(node_pos.pos)
    1.10      } yield (rendering, offset)
    1.11