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