ejgallego/coq-lsp 0.1.6+8.16

on GitHub

CHANGES:

• The info / goal view now uses jsCoq's client-side rendering, with
  better highlighting and layout rendering (@artagnon, @ejgallego,
  #143, fixes #96)
• Printing method is now configurable by the user (@ejgallego, #143,
  fixes #321)
• Trigger completion on quote char "'" (@ejgallego, #350)
• Fix typo on keybinding config for show goals (@tomtomjhj, #357)
• New request coq/getDocument to get serialized full document
  contents. Thanks to Clément Pit-Claudel for feedback and ideas.
  (@ejgallego, #350)
• Auto-ignore Coq object files; can be disabled in config
  (@ejgallego, #365)
• Support workspaces with multiple roots, this is very useful for
  projects that contain several _CoqProject files in different
  directories (@ejgallego, #374)
• Add VS Code commands to start / stop the server (@ejgallego, #377,
  cc #209)
• Fix bug that made the server not exit on exit LSP notification
  (@artagnon, @ejgallego, #375, fixes #230)
• Lay the foundation for server tests (@artagnon, #356)
• Remove the coq-lsp.ok_diagnostics setting (@artagnon, #129)
• Print abbreviations on hover (@ejgallego, #384)
• Print hover types without parenthesis (@ejgallego, #384)
• Parse identifiers with dot for hover and jump to definition
  (@ejallego, #385)
• Update vscode-languageclient to 8.1.0 (@ejgallego, @Alizter,
  #383, fixes #273)
• Fix typo on max_errors checking, this made coq-lsp stop on the
  number of total diagnostics, instead of only errors (@ejgallego,
  #386)
• Hover symbol information: hypothesis names must shadow globals of
  the same name (@ejgallego, #391, fixes #388)
• De-schedule document on didClose, otherwise the scheduler will keep
  trying to resume it if it didn't finish (@ejgallego, #392)
• Hover symbol information: correctly handle identifiers before '.'
  and containing a quote (') themselves (@ejgallego, #393)
• Add children entries to the table-of-contents (@ejgallego, #394)
• Invalidate Coq's imperative cache on error (@ejgallego, @r-muhairi,
  #395)
• Add status bar button to toggle server run status (@ejgallego,
  @Alizter, #378, closes #209)
• Support for COQLIB and COQCORELIB environment variables, added
  --coqcorelib command line argument (@ejgallego, #403)
• Protocol infrastructure for code lenses (@ejgallego, #396)
• Set binary more for protocol input / output (@ejgallego, #408)
• Allow to set ocamlpath from the command line (@ejgallego, #408)
• Windows support (@ejgallego, @jim-portegies, #408)
• Scroll active goal into view (@ejgallego, #410, fixes #381)
• Server status icon will now react properly to fatal server errors
  (@ejgallego, reported by @Alizter, #411, fixes #399)
• Info on memory and time is now disabled by default, new option
  coq-lsp.stats_on_hover_option to re-enable it (@ejgallego, #412,
  fixes #398).
• coq-lsp can now save .vo files for files opened in the
  editor. Use the new "Save to .vo" command, or the new protocol
  coq/saveVo request (@ejgallego, #417, fixes #339)