src/Tools/VSCode/src/server.scala
changeset 64747 54afac94f52b
parent 64737 9fc965612459
child 64748 155bf8632104
equal deleted inserted replaced
64746:34db87033abe 64747:54afac94f52b
   283         info <- rendering.tooltip(Text.Range(offset, offset + 1))
   283         info <- rendering.tooltip(Text.Range(offset, offset + 1))
   284       } yield {
   284       } yield {
   285         val doc = rendering.model.doc
   285         val doc = rendering.model.doc
   286         val range = doc.range(info.range)
   286         val range = doc.range(info.range)
   287         val s = Pretty.string_of(info.info, margin = rendering.tooltip_margin)
   287         val s = Pretty.string_of(info.info, margin = rendering.tooltip_margin)
   288         (range, List("```\n" + s + "\n```"))  // FIXME proper content format
   288         (range, List(s))
   289       }
   289       }
   290     channel.write(Protocol.Hover.reply(id, result))
   290     channel.write(Protocol.Hover.reply(id, result))
   291   }
   291   }
   292 
   292 
   293 
   293