src/Tools/VSCode/src/protocol.scala
changeset 66090 5e1c1b366ac3
parent 66062 175772371cd0
child 66096 6187612e83c1
equal deleted inserted replaced
66086:3f7067ba5df3 66090:5e1c1b366ac3
   460 
   460 
   461   /* dynamic output */
   461   /* dynamic output */
   462 
   462 
   463   object Dynamic_Output
   463   object Dynamic_Output
   464   {
   464   {
   465     def apply(body: String): JSON.T =
   465     def apply(content: String): JSON.T =
   466       Notification("PIDE/dynamic_output", Map("content" -> body))
   466       Notification("PIDE/dynamic_output", Map("content" -> content))
   467   }
   467   }
   468 
   468 
   469 
   469 
   470   /* preview */
   470   /* preview */
   471 
   471