Set default goal comment to --- and merge from upstream

.github/workflows/build.yml

@@ -16,7 +16,11 @@ name: Build
 on:
   # Trigger the workflow on pushes to only the 'main' branch (this avoids duplicate checks being run e.g., for dependabot pull requests)
   push:
-    branches: [ main ]
+    branches:
+      - main
+      # also on feat branches
+      # this does not work
+      # - feat/.+
   # Trigger the workflow on any pull request
   pull_request:
 

CHANGELOG.md

@@ -3,6 +3,9 @@
 # lean4ij Changelog
 
 ## [Unreleased]
+- fix caret of internal infoview at first line first col while refreshing
+- tuning size for internal infoview popup window
+- remove click in internal infoview, some optimization for popup up doc
 
 ## [0.0.17] - 2024-10-06
 

README.md

@@ -21,7 +21,7 @@ This plugin uses [LSP4IJ](https://github.com/redhat-developer/lsp4ij) for connec
   `Install`
 
 - Manually: Download the [latest release](https://github.com/onriv/lean4ij/releases/latest) and install it manually using
-  `Settings/Preferences` > `Plugins` > `⚙️` > `Install plugin from disk...`
+  `Settings/Preferences` > `Plugins` > `⚙️` > `Install plugin from disk...` For nightly builds go to [Actions/build](https://github.com/onriv/lean4ij/actions/workflows/build.yml) and download from the buttom of eachsuccess run.
 
 The plugin should be compatible from version 2024.1 and can not support the earlier versions for depending on textmate plugin's extension api.
 ## Usage
@@ -45,6 +45,21 @@ Messages and logs about the lean lsp server can be found in the language server
 | RestartCurrentLeanFile | Lean4 : Restart Current Lean File | restart current file        |
 | RestartJcefInfoview    | Lean4 : Restart Jcef Infoview     | restart the jcef infoview   |
 
+## Settings
+
+Since version 0.0.17 there are some settings available:
+- General setting is under `Settings/Preferences` > `Leanguages & Frameworks` > `Lean4`. Available settings are:
+  - (TODO) Enable Lsp Completion: Currently not support, waiting lsp4ij's new release. This is for currently discovering that sometimes lsp completion is slow. But it's enable by default.
+- Enable the native infoview, and timeout for popping the doc
+- Enable the external infoview
+- Extra css for external infoview. The most relevant I found is changing font-size
+
+The inlay hints related settings are under `Settings/Preferences` > `Inlay Hints` > `textmate`:
+- `Show inlay hint for omit type`
+- `Show value for placeholder _`
+
+Some color settings are under `Settings/Preferences` > `Editor` > `Color Scheme` >  `Lean Infoview`. It contains color settings for both the external and internal infoview.
+
 <!-- Plugin description end -->
 
 ## Development
@@ -56,13 +71,15 @@ Please check [DEVELOP.md](./DEVELOP.md).
 The plugin is still on an early stage, check [ISSUES.md](./ISSUES.md) for known and logged issues, and [TODO.md](./TODO.md)
 
 ## Troubleshooting
+- Currently, the plugin seems capable to open the same project with vscode in the same time (Although it may consume twice the cpu and memory resources). Try open the project simultaneously in VSC and JB-IDE while troubleshooting.
 - Currently, some log is printed in the build window for the progressing file and the url to the external/jcef infoview, if something does not work normally, some log there may help.
 - There are also detailed logs for the lsp server supported by LSP4IJ via the "language servers" tool window after setting the debug/trace level to verbose.
 - Some logs are also sent in the standard log file like `idea.log`. For different systems the path of it's the following paths, it can also be opened via `Help/Show log in ...` in the menu.
   - (Linux) `$HOME.cache/JetBrains/<Product>/log/idea.log`
   - (Windows) `$HOME\AppData\Local\JetBrains\<Product>\log\idea.log`
   - (Macos) `~/Library/Caches/<Product>/log/idea.log`
-
+- If the IDE is freezing, try check also the `threadDumps-freeze-***` files under the log folder.
+
 ## Acknowledgments
 
 The following projects give great help for developing the plugin:

TODO.md

@@ -48,6 +48,7 @@
 - [ ] weird, is it just me or any other reason making only word autocompletion not working? In comment, it works but in normal pos it does not. It seems it's superseded by 
   some semantic autocompletion. --- yeah it's because semantic autocompletion is too slow. Can it be done in two steps? first show alphabet autocompletion and then add more semantic 
   autocompletion 
+- [ ] after bump lsp4ij to 0.7.0, make autocompletion configurable
 - [ ] quick fix for field missing
 - [x] color for error message
 - [ ] code completion seems slow and requires manually press ctrl+space
@@ -57,16 +58,24 @@
 – [x] two cases still exists for all messages: this should already be fixed
   1. it's not shown
   2. it's outdated
-– [x] some snippets to things like \<>
+– [x] some snippets to things like `\<>`
+- [ ] for some snippets maybe it's better to add a space, like `\to`, now for triggering it, it requires a space. But most case it will continue with a space.
+  - But not sure for the design, some absolutely don't want a auto created space
 – [ ] TODO weird brackets does not complete
 – [ ] maybe it's still better define some lang-like feature using parser/lexer, although it cannot be full parsed, but for the level like textmate it should be OK
 – [ ] is it possible do something like pygments/ctags/gtags completion?
 – [ ] option to skip library or backend files
 – [ ] error seems quite delay vanish... it shows errors event it has been fixed.
+- [ ] the internal infoview some case also delay (especially using ideavim one does not move caret)
 – [ ] comment auto comment like /-- trigger block comment
 – [ ] bock/line comment command
 – [ ] impl simp? which replace the code
 - [ ] settings for getAllMessages, both internal/external infoview
+- [ ] maybe it's just me with my idea settings, the gap between first column and line number is a little width
+- [ ] autogenerate missing fields
+- [ ] internal infoview when expanding all messages it seems jumping
+- [ ] check if live templates can dynamically define or not, in this way we can control if suffix space add automatically or not
+- [ ] internal infoview will automatically scroll to the end, kind of disturbing
 
 # Maybe some improvements
 

docs/inlayhints.md

@@ -0,0 +1,11 @@
+
+Some docs on positions that maybe enable inlay hints
+
+# instance field impl
+
+It seems useful with inlay hints at:
+
+```
+instance SomeImpl : SomeInst where
+  some_field /--add inlay hint here?-/:= 
+```

gradle.properties

@@ -4,7 +4,7 @@ pluginGroup = lean4ij
 pluginName = lean4ij
 pluginRepositoryUrl = https://github.com/onriv/lean4ij
 # SemVer format -> https://semver.org
-pluginVersion = 0.0.17
+pluginVersion = 0.0.18.beta.0
 
 # Supported build number ranges and IntelliJ Platform versions -> https://plugins.jetbrains.com/docs/intellij/build-number-ranges.html
 # For the dependence on textmate bundle api, the plugin must start build from 241