src/Tools/VSCode/src/server.scala
changeset 64704 08c2d80428ff
parent 64703 a115391494ed
child 64706 3ebf9f8299df
equal deleted inserted replaced
64703:a115391494ed 64704:08c2d80428ff
    99   def resources: VSCode_Resources = session.resources.asInstanceOf[VSCode_Resources]
    99   def resources: VSCode_Resources = session.resources.asInstanceOf[VSCode_Resources]
   100 
   100 
   101   def rendering_offset(node_pos: Line.Node_Position): Option[(VSCode_Rendering, Text.Offset)] =
   101   def rendering_offset(node_pos: Line.Node_Position): Option[(VSCode_Rendering, Text.Offset)] =
   102     for {
   102     for {
   103       model <- resources.get_model(node_pos.name)
   103       model <- resources.get_model(node_pos.name)
   104       rendering = model.rendering(options)
   104       rendering = model.rendering()
   105       offset <- model.doc.offset(node_pos.pos)
   105       offset <- model.doc.offset(node_pos.pos)
   106     } yield (rendering, offset)
   106     } yield (rendering, offset)
   107 
   107 
   108 
   108 
   109   /* input from client */
   109   /* input from client */