conv zoom button

Stream: lean4 dev

[Jakob von Raumer]

Let's continue here @Robin Böhne @Gabriel Ebner @Wojciech Nawrocki @Edward Ayers, then we don't have to copy any previous discussion if anybody else wants to chime in.

[Jakob von Raumer]

I think @Robin Böhne was about to implement an rpc procedure to set the cursor to a given position, in order to place the cursor after the inserted enter [...] conv command which is inserted by the Zoom button in the infoview

[Gabriel Ebner]

Please more context! What is Zoom?

[Jakob von Raumer]

@Robin Böhne has, as part of his Bachelor project, implemented a button for the Infoview Type Info which lets the user zoom in to a subterm using conv

[Jakob von Raumer]

The only part that's missing for it to be smooth is to place the cursor after the commands we insert, so the state after clicking the button is actually the zoomed in one.

[Gabriel Ebner]

Can you please elaborate a bit more? What is "zoom"?

[Jakob von Raumer]

conv { enter[...] }

[Jakob von Raumer]

Sorry, I have to leave, I'll add more details later, or someone else can :grinning_face_with_smiling_eyes:

[Johan Commelin]

It sounds to me like "Zoom" is a widget functionality that is a GUI for conv mode?

[Gabriel Ebner]

That's my guess as well.

[Gabriel Ebner]

It would be great if somebody could post a "before" and an "after" state.

[Gabriel Ebner]

And also where this "zoom" button appears. Is this a button in popups, or somewhere else?

[Sebastian Ullrich]

Johan Commelin said:

It sounds to me like "Zoom" is a widget functionality that is a GUI for conv mode?

Yes, map a subterm in the info view to a conv step making that subterm the "conv goal"

[Robin Böhne]

To give a bit more context, what I'm doing is I'm writing a function that makes using conv easier. In the infoview, you can hover over subterm, and I added a "zoom" button to those popups that automatically inserts the correct enter command to get from the goal to the subterm. For example, let's say our goal is x + y = y + x + 0, now we can hover over the second x, click "zoom", and the button will insert enter [2, 1, 2] at the correct position.

For that I used the cursor position, for example, I use it to find the position in the document syntax tree that I need to insert the enter at and I use it to get the goal.

[Gabriel Ebner]

The cursor position is going to be super flaky, but okay for a tech preview. For example, |rw [xyz] shows a different conv state than r|w [xyz] (where | is the cursor position). In one case you'd want to insert the tactic on the line above, in the other one on the line below.

[Gabriel Ebner]

(Inserting lines is of course not particularly robust either, but all we've got atm.)

[Gabriel Ebner]

The only part that's missing for it to be smooth is to place the cursor after the commands we insert, so the state after clicking the button is actually the zoomed in one.

In the private discussion, I understood that the problem was something else, namely that you don't know the position at which you want to insert the tactic. Can you elaborate on where you're stuck?

[Robin Böhne]

Gabriel Ebner said:

The only part that's missing for it to be smooth is to place the cursor after the commands we insert, so the state after clicking the button is actually the zoomed in one.

In the private discussion, I understood that the problem was something else, namely that you don't know the position at which you want to insert the tactic. Can you elaborate on where you're stuck?

Well, I know how to get the position at which I want to insert the tactic from the cursor position. The problem right now is that I can't get the cursor position in the first place. Before, I could just pass the posproperty from the popup, but now that the position is hidden in RpcSessionAtPos, I can't get the cursor position anymore.

[Robin Böhne]

As for placing the cursor at the correct position after inserting, that's an entirely seperate issue

[Gabriel Ebner]

Hmm, we could add a InfoPosition React context..

[Robin Böhne]

Yes, that could work.