Proposal for an API based "Suggestions" detail in infoview

[timlacroix]

As described in the title. Some missing things on which I'd like help :

• clicking -> paste into editor. I imagine I should do something similar to

  text = text.replace(trythis.regexGM, (_, tactic) => {
      const command = encodeURI('command:_lean.pasteTacticSuggestion?' +
          JSON.stringify([m, tactic]));
      return `${trythis.magicWord}<a class="link" href="${command}" title="${tactic}">${tactic}</a>`
  });

  But I'm not sure how to build $m$ in my case.

• debouncing queries to the API when editing the "prefix" field. (If we want to keep this field. Not sure it's super valuable)

• Suggestions status change (loading or not) doesn't seem perfect, refreshing suggestions requires a bit of cursor fiddling in the editor currently, and I think behaviour is weird on file change. Maybe I'm not handling widgets properly ?

[gebner]

debouncing queries to the API when editing the "prefix" field. (If we want to keep this field. Not sure it's super valuable)

You might want to check out the delayedThrottle function. https://github.com/leanprover/vscode-lean/blob/master/infoview/info.tsx#L66-L82

I think the prefix field is actually a nice idea.

[gebner]

clicking -> paste into editor. I imagine I should do something similar to

The pasteTacticSuggestion stuff replaces the current tactic, which is not what we want here.

What we actually want here is to insert a tactic before the current one. But doing this properly is pretty hard in Lean 3, so I would suggest to just insert the suggestion on the line above. This should do the trick:

    post({ command: 'insert_text', text: `\n${suggestion}\n`, insert_type: 'relative'});

[gebner]

The mechanics are great now. I think it's good enough to try out on real users now.