1/* Title: Tools/VSCode/src/server.scala 2 Author: Makarius 3 4Server for VS Code Language Server Protocol 2.0/3.0, see also 5https://github.com/Microsoft/language-server-protocol 6https://github.com/Microsoft/language-server-protocol/blob/master/protocol.md 7 8PIDE protocol extensions depend on system option "vscode_pide_extensions". 9*/ 10 11package isabelle.vscode 12 13 14import isabelle._ 15 16import java.io.{PrintStream, OutputStream, File => JFile} 17 18import scala.annotation.tailrec 19import scala.collection.mutable 20 21 22object Server 23{ 24 type Editor = isabelle.Editor[Unit] 25 26 27 /* Isabelle tool wrapper */ 28 29 private lazy val default_logic = Isabelle_System.getenv("ISABELLE_LOGIC") 30 31 val isabelle_tool = Isabelle_Tool("vscode_server", "VSCode Language Server for PIDE", args => 32 { 33 try { 34 var logic_ancestor: Option[String] = None 35 var log_file: Option[Path] = None 36 var logic_requirements = false 37 var logic_focus = false 38 var dirs: List[Path] = Nil 39 var include_sessions: List[String] = Nil 40 var logic = default_logic 41 var modes: List[String] = Nil 42 var options = Options.init() 43 var system_mode = false 44 var verbose = false 45 46 val getopts = Getopts(""" 47Usage: isabelle vscode_server [OPTIONS] 48 49 Options are: 50 -A NAME ancestor session for options -R and -S (default: parent) 51 -L FILE logging on FILE 52 -R NAME build image with requirements from other sessions 53 -S NAME like option -R, with focus on selected session 54 -d DIR include session directory 55 -i NAME include session in name-space of theories 56 -l NAME logic session name (default ISABELLE_LOGIC=""" + quote(default_logic) + """) 57 -m MODE add print mode for output 58 -o OPTION override Isabelle system OPTION (via NAME=VAL or NAME) 59 -s system build mode for session image 60 -v verbose logging 61 62 Run the VSCode Language Server protocol (JSON RPC) over stdin/stdout. 63""", 64 "A:" -> (arg => logic_ancestor = Some(arg)), 65 "L:" -> (arg => log_file = Some(Path.explode(File.standard_path(arg)))), 66 "R:" -> (arg => { logic = arg; logic_requirements = true }), 67 "S:" -> (arg => { logic = arg; logic_requirements = true; logic_focus = true }), 68 "d:" -> (arg => dirs = dirs ::: List(Path.explode(File.standard_path(arg)))), 69 "i:" -> (arg => include_sessions = include_sessions ::: List(arg)), 70 "l:" -> (arg => logic = arg), 71 "m:" -> (arg => modes = arg :: modes), 72 "o:" -> (arg => options = options + arg), 73 "s" -> (_ => system_mode = true), 74 "v" -> (_ => verbose = true)) 75 76 val more_args = getopts(args) 77 if (more_args.nonEmpty) getopts.usage() 78 79 val log = Logger.make(log_file) 80 val channel = new Channel(System.in, System.out, log, verbose) 81 val server = 82 new Server(channel, options, session_name = logic, session_dirs = dirs, 83 include_sessions = include_sessions, session_ancestor = logic_ancestor, 84 session_requirements = logic_requirements, session_focus = logic_focus, 85 all_known = !logic_focus, modes = modes, system_mode = system_mode, log = log) 86 87 // prevent spurious garbage on the main protocol channel 88 val orig_out = System.out 89 try { 90 System.setOut(new PrintStream(new OutputStream { def write(n: Int) {} })) 91 server.start() 92 } 93 finally { System.setOut(orig_out) } 94 } 95 catch { 96 case exn: Throwable => 97 val channel = new Channel(System.in, System.out, No_Logger) 98 channel.error_message(Exn.message(exn)) 99 throw(exn) 100 } 101 }) 102} 103 104class Server( 105 val channel: Channel, 106 options: Options, 107 session_name: String = Server.default_logic, 108 session_dirs: List[Path] = Nil, 109 include_sessions: List[String] = Nil, 110 session_ancestor: Option[String] = None, 111 session_requirements: Boolean = false, 112 session_focus: Boolean = false, 113 all_known: Boolean = false, 114 modes: List[String] = Nil, 115 system_mode: Boolean = false, 116 log: Logger = No_Logger) 117{ 118 server => 119 120 121 /* prover session */ 122 123 private val session_ = Synchronized(None: Option[Session]) 124 def session: Session = session_.value getOrElse error("Server inactive") 125 def resources: VSCode_Resources = session.resources.asInstanceOf[VSCode_Resources] 126 127 def rendering_offset(node_pos: Line.Node_Position): Option[(VSCode_Rendering, Text.Offset)] = 128 for { 129 model <- resources.get_model(new JFile(node_pos.name)) 130 rendering = model.rendering() 131 offset <- model.content.doc.offset(node_pos.pos) 132 } yield (rendering, offset) 133 134 private val dynamic_output = Dynamic_Output(server) 135 136 137 /* input from client or file-system */ 138 139 private val delay_input: Standard_Thread.Delay = 140 Standard_Thread.delay_last(options.seconds("vscode_input_delay"), channel.Error_Logger) 141 { resources.flush_input(session, channel) } 142 143 private val delay_load: Standard_Thread.Delay = 144 Standard_Thread.delay_last(options.seconds("vscode_load_delay"), channel.Error_Logger) { 145 val (invoke_input, invoke_load) = 146 resources.resolve_dependencies(session, editor, file_watcher) 147 if (invoke_input) delay_input.invoke() 148 if (invoke_load) delay_load.invoke 149 } 150 151 private val file_watcher = 152 File_Watcher(sync_documents(_), options.seconds("vscode_load_delay")) 153 154 private def close_document(file: JFile) 155 { 156 if (resources.close_model(file)) { 157 file_watcher.register_parent(file) 158 sync_documents(Set(file)) 159 delay_input.invoke() 160 delay_output.invoke() 161 } 162 } 163 164 private def sync_documents(changed: Set[JFile]) 165 { 166 resources.sync_models(changed) 167 delay_input.invoke() 168 delay_output.invoke() 169 } 170 171 private def change_document(file: JFile, version: Long, changes: List[Protocol.TextDocumentChange]) 172 { 173 val norm_changes = new mutable.ListBuffer[Protocol.TextDocumentChange] 174 @tailrec def norm(chs: List[Protocol.TextDocumentChange]) 175 { 176 if (chs.nonEmpty) { 177 val (full_texts, rest1) = chs.span(_.range.isEmpty) 178 val (edits, rest2) = rest1.span(_.range.nonEmpty) 179 norm_changes ++= full_texts 180 norm_changes ++= edits.sortBy(_.range.get.start)(Line.Position.Ordering).reverse 181 norm(rest2) 182 } 183 } 184 norm(changes) 185 norm_changes.foreach(change => 186 resources.change_model(session, editor, file, version, change.text, change.range)) 187 188 delay_input.invoke() 189 delay_output.invoke() 190 } 191 192 193 /* caret handling */ 194 195 private val delay_caret_update: Standard_Thread.Delay = 196 Standard_Thread.delay_last(options.seconds("vscode_input_delay"), channel.Error_Logger) 197 { session.caret_focus.post(Session.Caret_Focus) } 198 199 private def update_caret(caret: Option[(JFile, Line.Position)]) 200 { 201 resources.update_caret(caret) 202 delay_caret_update.invoke() 203 delay_input.invoke() 204 } 205 206 207 /* preview */ 208 209 private lazy val preview_panel = new Preview_Panel(resources) 210 211 private lazy val delay_preview: Standard_Thread.Delay = 212 Standard_Thread.delay_last(options.seconds("vscode_output_delay"), channel.Error_Logger) 213 { 214 if (preview_panel.flush(channel)) delay_preview.invoke() 215 } 216 217 private def request_preview(file: JFile, column: Int) 218 { 219 preview_panel.request(file, column) 220 delay_preview.invoke() 221 } 222 223 224 /* output to client */ 225 226 private val delay_output: Standard_Thread.Delay = 227 Standard_Thread.delay_last(options.seconds("vscode_output_delay"), channel.Error_Logger) 228 { 229 if (resources.flush_output(channel)) delay_output.invoke() 230 } 231 232 def update_output(changed_nodes: Traversable[JFile]) 233 { 234 resources.update_output(changed_nodes) 235 delay_output.invoke() 236 } 237 238 def update_output_visible() 239 { 240 resources.update_output_visible() 241 delay_output.invoke() 242 } 243 244 private val prover_output = 245 Session.Consumer[Session.Commands_Changed](getClass.getName) { 246 case changed => 247 update_output(changed.nodes.toList.map(resources.node_file(_))) 248 } 249 250 private val syslog_messages = 251 Session.Consumer[Prover.Output](getClass.getName) { 252 case output => channel.log_writeln(resources.output_xml(output.message)) 253 } 254 255 256 /* init and exit */ 257 258 def init(id: Protocol.Id) 259 { 260 def reply_ok(msg: String) 261 { 262 channel.write(Protocol.Initialize.reply(id, "")) 263 channel.writeln(msg) 264 } 265 266 def reply_error(msg: String) 267 { 268 channel.write(Protocol.Initialize.reply(id, msg)) 269 channel.error_message(msg) 270 } 271 272 val try_session = 273 try { 274 val base_info = 275 Sessions.base_info( 276 options, session_name, dirs = session_dirs, include_sessions = include_sessions, 277 session_ancestor = session_ancestor, session_requirements = session_requirements, 278 session_focus = session_focus, all_known = all_known) 279 val session_base = base_info.check_base 280 281 def build(no_build: Boolean = false): Build.Results = 282 Build.build(options, build_heap = true, no_build = no_build, system_mode = system_mode, 283 dirs = session_dirs, infos = base_info.infos, sessions = List(base_info.session)) 284 285 if (!build(no_build = true).ok) { 286 val start_msg = "Build started for Isabelle/" + base_info.session + " ..." 287 val fail_msg = "Session build failed -- prover process remains inactive!" 288 289 val progress = channel.progress(verbose = true) 290 progress.echo(start_msg); channel.writeln(start_msg) 291 292 if (!build().ok) { progress.echo(fail_msg); error(fail_msg) } 293 } 294 295 val resources = new VSCode_Resources(options, session_base, log) 296 { 297 override def commit(change: Session.Change): Unit = 298 if (change.deps_changed || undefined_blobs(change.version.nodes).nonEmpty) 299 delay_load.invoke() 300 } 301 302 val session_options = options.bool("editor_output_state") = true 303 val session = new Session(session_options, resources) 304 305 Some((base_info, session)) 306 } 307 catch { case ERROR(msg) => reply_error(msg); None } 308 309 for ((base_info, session) <- try_session) { 310 session_.change(_ => Some(session)) 311 312 session.commands_changed += prover_output 313 session.syslog_messages += syslog_messages 314 315 dynamic_output.init() 316 317 var session_phase: Session.Consumer[Session.Phase] = null 318 session_phase = 319 Session.Consumer(getClass.getName) { 320 case Session.Ready => 321 session.phase_changed -= session_phase 322 reply_ok("Welcome to Isabelle/" + base_info.session + " (" + Distribution.version + ")") 323 case Session.Terminated(result) if !result.ok => 324 session.phase_changed -= session_phase 325 reply_error("Prover startup failed: return code " + result.rc) 326 case _ => 327 } 328 session.phase_changed += session_phase 329 330 Isabelle_Process.start(session, options, modes = modes, 331 sessions_structure = Some(base_info.sessions_structure), logic = base_info.session) 332 } 333 } 334 335 def shutdown(id: Protocol.Id) 336 { 337 def reply(err: String): Unit = channel.write(Protocol.Shutdown.reply(id, err)) 338 339 session_.change({ 340 case Some(session) => 341 session.commands_changed -= prover_output 342 session.syslog_messages -= syslog_messages 343 344 dynamic_output.exit() 345 346 delay_load.revoke() 347 file_watcher.shutdown() 348 delay_input.revoke() 349 delay_output.revoke() 350 delay_caret_update.revoke() 351 delay_preview.revoke() 352 353 val result = session.stop() 354 if (result.ok) reply("") else reply("Prover shutdown failed: return code " + result.rc) 355 None 356 case None => 357 reply("Prover inactive") 358 None 359 }) 360 } 361 362 def exit() { 363 log("\n") 364 sys.exit(if (session_.value.isDefined) 1 else 0) 365 } 366 367 368 /* completion */ 369 370 def completion(id: Protocol.Id, node_pos: Line.Node_Position) 371 { 372 val result = 373 (for ((rendering, offset) <- rendering_offset(node_pos)) 374 yield rendering.completion(node_pos.pos, offset)) getOrElse Nil 375 channel.write(Protocol.Completion.reply(id, result)) 376 } 377 378 379 /* spell-checker dictionary */ 380 381 def update_dictionary(include: Boolean, permanent: Boolean) 382 { 383 for { 384 spell_checker <- resources.spell_checker.get 385 caret <- resources.get_caret() 386 rendering = caret.model.rendering() 387 range = rendering.before_caret_range(caret.offset) 388 Text.Info(_, word) <- Spell_Checker.current_word(rendering, range) 389 } { 390 spell_checker.update(word, include, permanent) 391 update_output_visible() 392 } 393 } 394 395 def reset_dictionary() 396 { 397 for (spell_checker <- resources.spell_checker.get) 398 { 399 spell_checker.reset() 400 update_output_visible() 401 } 402 } 403 404 405 /* hover */ 406 407 def hover(id: Protocol.Id, node_pos: Line.Node_Position) 408 { 409 val result = 410 for { 411 (rendering, offset) <- rendering_offset(node_pos) 412 info <- rendering.tooltips(VSCode_Rendering.tooltip_elements, Text.Range(offset, offset + 1)) 413 } yield { 414 val range = rendering.model.content.doc.range(info.range) 415 val contents = 416 info.info.map(t => Protocol.MarkedString(resources.output_pretty_tooltip(List(t)))) 417 (range, contents) 418 } 419 channel.write(Protocol.Hover.reply(id, result)) 420 } 421 422 423 /* goto definition */ 424 425 def goto_definition(id: Protocol.Id, node_pos: Line.Node_Position) 426 { 427 val result = 428 (for ((rendering, offset) <- rendering_offset(node_pos)) 429 yield rendering.hyperlinks(Text.Range(offset, offset + 1))) getOrElse Nil 430 channel.write(Protocol.GotoDefinition.reply(id, result)) 431 } 432 433 434 /* document highlights */ 435 436 def document_highlights(id: Protocol.Id, node_pos: Line.Node_Position) 437 { 438 val result = 439 (for ((rendering, offset) <- rendering_offset(node_pos)) 440 yield { 441 val model = rendering.model 442 rendering.caret_focus_ranges(Text.Range(offset, offset + 1), model.content.text_range) 443 .map(r => Protocol.DocumentHighlight.text(model.content.doc.range(r))) 444 }) getOrElse Nil 445 channel.write(Protocol.DocumentHighlights.reply(id, result)) 446 } 447 448 449 /* main loop */ 450 451 def start() 452 { 453 log("Server started " + Date.now()) 454 455 def handle(json: JSON.T) 456 { 457 try { 458 json match { 459 case Protocol.Initialize(id) => init(id) 460 case Protocol.Initialized(()) => 461 case Protocol.Shutdown(id) => shutdown(id) 462 case Protocol.Exit(()) => exit() 463 case Protocol.DidOpenTextDocument(file, _, version, text) => 464 change_document(file, version, List(Protocol.TextDocumentChange(None, text))) 465 delay_load.invoke() 466 case Protocol.DidChangeTextDocument(file, version, changes) => 467 change_document(file, version, changes) 468 case Protocol.DidCloseTextDocument(file) => close_document(file) 469 case Protocol.Completion(id, node_pos) => completion(id, node_pos) 470 case Protocol.Include_Word(()) => update_dictionary(true, false) 471 case Protocol.Include_Word_Permanently(()) => update_dictionary(true, true) 472 case Protocol.Exclude_Word(()) => update_dictionary(false, false) 473 case Protocol.Exclude_Word_Permanently(()) => update_dictionary(false, true) 474 case Protocol.Reset_Words(()) => reset_dictionary() 475 case Protocol.Hover(id, node_pos) => hover(id, node_pos) 476 case Protocol.GotoDefinition(id, node_pos) => goto_definition(id, node_pos) 477 case Protocol.DocumentHighlights(id, node_pos) => document_highlights(id, node_pos) 478 case Protocol.Caret_Update(caret) => update_caret(caret) 479 case Protocol.State_Init(()) => State_Panel.init(server) 480 case Protocol.State_Exit(id) => State_Panel.exit(id) 481 case Protocol.State_Locate(id) => State_Panel.locate(id) 482 case Protocol.State_Update(id) => State_Panel.update(id) 483 case Protocol.State_Auto_Update(id, enabled) => State_Panel.auto_update(id, enabled) 484 case Protocol.Preview_Request(file, column) => request_preview(file, column) 485 case Protocol.Symbols_Request(()) => channel.write(Protocol.Symbols()) 486 case _ => if (!Protocol.ResponseMessage.is_empty(json)) log("### IGNORED") 487 } 488 } 489 catch { case exn: Throwable => channel.log_error_message(Exn.message(exn)) } 490 } 491 492 @tailrec def loop() 493 { 494 channel.read() match { 495 case Some(json) => 496 json match { 497 case bulk: List[_] => bulk.foreach(handle(_)) 498 case _ => handle(json) 499 } 500 loop() 501 case None => log("### TERMINATE") 502 } 503 } 504 loop() 505 } 506 507 508 /* abstract editor operations */ 509 510 object editor extends Server.Editor 511 { 512 /* session */ 513 514 override def session: Session = server.session 515 override def flush(): Unit = resources.flush_input(session, channel) 516 override def invoke(): Unit = delay_input.invoke() 517 518 519 /* current situation */ 520 521 override def current_node(context: Unit): Option[Document.Node.Name] = 522 resources.get_caret().map(_.model.node_name) 523 override def current_node_snapshot(context: Unit): Option[Document.Snapshot] = 524 resources.get_caret().map(_.model.snapshot()) 525 526 override def node_snapshot(name: Document.Node.Name): Document.Snapshot = 527 { 528 resources.get_model(name) match { 529 case Some(model) => model.snapshot() 530 case None => session.snapshot(name) 531 } 532 } 533 534 def current_command(snapshot: Document.Snapshot): Option[Command] = 535 { 536 resources.get_caret() match { 537 case Some(caret) => snapshot.current_command(caret.node_name, caret.offset) 538 case None => None 539 } 540 } 541 override def current_command(context: Unit, snapshot: Document.Snapshot): Option[Command] = 542 current_command(snapshot) 543 544 545 /* overlays */ 546 547 override def node_overlays(name: Document.Node.Name): Document.Node.Overlays = 548 resources.node_overlays(name) 549 550 override def insert_overlay(command: Command, fn: String, args: List[String]): Unit = 551 resources.insert_overlay(command, fn, args) 552 553 override def remove_overlay(command: Command, fn: String, args: List[String]): Unit = 554 resources.remove_overlay(command, fn, args) 555 556 557 /* hyperlinks */ 558 559 override def hyperlink_command( 560 focus: Boolean, snapshot: Document.Snapshot, id: Document_ID.Generic, 561 offset: Symbol.Offset = 0): Option[Hyperlink] = 562 { 563 if (snapshot.is_outdated) None 564 else 565 snapshot.find_command_position(id, offset).map(node_pos => 566 new Hyperlink { 567 def follow(unit: Unit) { channel.write(Protocol.Caret_Update(node_pos, focus)) } 568 }) 569 } 570 571 572 /* dispatcher thread */ 573 574 override def assert_dispatcher[A](body: => A): A = session.assert_dispatcher(body) 575 override def require_dispatcher[A](body: => A): A = session.require_dispatcher(body) 576 override def send_dispatcher(body: => Unit): Unit = session.send_dispatcher(body) 577 override def send_wait_dispatcher(body: => Unit): Unit = session.send_wait_dispatcher(body) 578 } 579} 580