src/Tools/VSCode/src/server.scala
changeset 64651 ea5620f7b0d8
parent 64649 d67c3094a0c2
child 64655 ea34f36ff6a5
     1.1 --- a/src/Tools/VSCode/src/server.scala	Wed Dec 21 22:37:53 2016 +0100
     1.2 +++ b/src/Tools/VSCode/src/server.scala	Wed Dec 21 22:49:53 2016 +0100
     1.3 @@ -106,11 +106,11 @@
     1.4    def session: Session = state.value.session getOrElse error("Session inactive")
     1.5    def resources: VSCode_Resources = session.resources.asInstanceOf[VSCode_Resources]
     1.6  
     1.7 -  def rendering_offset(pos_node: Line.Position_Node): Option[(VSCode_Rendering, Text.Offset)] =
     1.8 +  def rendering_offset(node_pos: Line.Node_Position): Option[(VSCode_Rendering, Text.Offset)] =
     1.9      for {
    1.10 -      model <- state.value.models.get(pos_node.name)
    1.11 +      model <- state.value.models.get(node_pos.name)
    1.12        rendering = model.rendering(options)
    1.13 -      offset <- model.doc.offset(pos_node.pos, text_length)
    1.14 +      offset <- model.doc.offset(node_pos.pos, text_length)
    1.15      } yield (rendering, offset)
    1.16  
    1.17  
    1.18 @@ -223,11 +223,11 @@
    1.19  
    1.20    /* hover */
    1.21  
    1.22 -  def hover(id: Protocol.Id, pos_node: Line.Position_Node)
    1.23 +  def hover(id: Protocol.Id, node_pos: Line.Node_Position)
    1.24    {
    1.25      val result =
    1.26        for {
    1.27 -        (rendering, offset) <- rendering_offset(pos_node)
    1.28 +        (rendering, offset) <- rendering_offset(node_pos)
    1.29          info <- rendering.tooltip(Text.Range(offset, offset + 1))
    1.30        } yield {
    1.31          val doc = rendering.model.doc
    1.32 @@ -242,10 +242,10 @@
    1.33  
    1.34    /* goto definition */
    1.35  
    1.36 -  def goto_definition(id: Protocol.Id, pos_node: Line.Position_Node)
    1.37 +  def goto_definition(id: Protocol.Id, node_pos: Line.Node_Position)
    1.38    {
    1.39      val result =
    1.40 -      (for ((rendering, offset) <- rendering_offset(pos_node))
    1.41 +      (for ((rendering, offset) <- rendering_offset(node_pos))
    1.42          yield rendering.hyperlinks(Text.Range(offset, offset + 1))) getOrElse Nil
    1.43      channel.write(Protocol.GotoDefinition.reply(id, result))
    1.44    }
    1.45 @@ -270,8 +270,8 @@
    1.46              update_document(uri, text)
    1.47            case Protocol.DidCloseTextDocument(uri) => channel.log("CLOSE " + uri)
    1.48            case Protocol.DidSaveTextDocument(uri) => channel.log("SAVE " + uri)
    1.49 -          case Protocol.Hover(id, pos_node) => hover(id, pos_node)
    1.50 -          case Protocol.GotoDefinition(id, pos_node) => goto_definition(id, pos_node)
    1.51 +          case Protocol.Hover(id, node_pos) => hover(id, node_pos)
    1.52 +          case Protocol.GotoDefinition(id, node_pos) => goto_definition(id, node_pos)
    1.53            case _ => channel.log("### IGNORED")
    1.54          }
    1.55        }