IDE Features

[Jazzpirate]

We need an IDE for sTeX3, so that semantic annotation becomes easier. The functionality should include

• [x] semantic highlighting,
• [x] semantic hyperrefs,
• [ ] semantic autocompletion,
• [x] semantic linting,
• [x] flagging redundant \importmodule or \usemodule, and helping remove them. This is less trivial than it sounds; An import may redundant because
  1. some other import already provides the theory (these are safe to delete)
  2. the contents of the importing theory do not use the imported theory (if we delete this import, then upstream theories may have to be extended).
• [ ] suggesting symname, symref, etc. For this we need to port and extend the "trefier" from stexls to the sTeX3 setting.
• [ ] refactoring and renaming support
• [ ] redefinition support: if we have a definition definame{bar}in theory baz (e.g. in the AI course notes), and we want to change it to make this into a redefinition of a definition \definame{foobar}in theory foobaz (e.g. in SMGloM), then we need to
  • add a \importmodule{foobaz} change \definame{bar} to \definame{foobaz?foobar} locally
  • change \symname{baz?bar} to \symname{foobar?foobaz} everywhere else (i.e. in the whole sTeX project).
• [ ] suggesting duplicate definienda, i.e. if the concept foo is defined in two (or more) theories, then there is a good chance that one should be a redefinition (or that both should be refactored into an SMGloM theory and both are redefinitions). Then we could use the functionality above to resolve this.
• [x] searching for existing symbols/semantic macros; both locally (in a user's mathhub directory) and remote (in repositories on mathhub.info). In both cases an MMT instance would serve the required index (what are the requirements?). Search needs to take a certain context into account, so that e.g. searching for "abelian group" can yield algebra/commutative-group?cgroup.
• [ ] associated javascript/typescript UI using Monaco for web-editing?
• [ ] warn about modules that do not contain any \symdecl and \symdef, they should probably be removed in favor of \usemodule. Exceptions are "union convenience modules".
• [ ] MANIFEST.mf depdendency management, whenever an \importmodule mentions an archive that is not mentioned in MANIFEST.mf (including recurively) then the user is prompted to add it.
• [x] symbol ambiguity management: We often habe \symref{bar}{...} in the notes. This is a short form for \symref{foo?bar}{...} which has the advantage of being shorter and more resistant to symbols being moved between theories, but it has the problem that there might be more than one theory (i.e. not just foo) that export the symbol bar. Then we cannot predict which theory sTeX picks. The IDE should warn about such ambituities (and help the user pick a disambiguation). Analogously, the IDE might want to prompt the user to shorten \symref{foo?bar}{...} when no ambiguity arises. The same service is relevanto for \symname and maybe semantic macros (established via \symdef).
• [x] warn about missing definienda, i.e. modules with \symdecl*{foo} and \symdef{foo}... which do not have a \definiendum{foo}{bar} or \definame{foo} somewhere. When https://github.com/slatex/sTeX/issues/326 gets resolved, also a \foo[definiendum] counts against missing definienda.
• [ ] (automatically) support inserting file=,archive= in \srefs
• [ ] warn about spurious imports, i.e. if there is an \importmodule{foo} but none of the symbols exported by the module foo is used (this feature might be costly), but would lead to better theory graphs.
• [ ] for a symbol, display all the "inheritance paths how this becomes visible in the current context.

We can build on the stexls language server and its vscode client.

[rappatoni]

Suggested improvement: support search operators and potentially regexes in search.