search

expln / metamath-lamp

Metamath-lamp (Lite Assistant for Metamath Proofs) is a GUI-based proof assistant for creating formal mathematical proofs in Metamath that does not require installation (just run it directly using your web browser).
https://expln.github.io/lamp/latest/index.html
MIT License
12 stars 5 forks source link

Discuss short/long click mappings #97

Closed expln closed 1 year ago

expln commented 1 year ago

This is a place to discuss the solution for short/long click mappings, which was initiated here https://github.com/expln/metamath-lamp/issues/83#issuecomment-1586236073

expln commented 1 year ago

I presume click==tap and long-click==long-tap throughout.

Yes, that is correct. So, I will always write long-click, but that will mean both long click and long tap.

Checkmark: Click = show compressed proof; Long-click no different

Click = show compressed proof - yes. Long-click no different - long-click is not supported for the checkmark. But the sequence of mouse down-wait-mouse up results in a short click, independently of how long wait was. Probably I will change this, please keep reading, I am providing my thoughts below.

There are also other options: Clicking on ? launches the bottom-up prover with search depth = 1, logging level = 1 and other parameters with some specific values which should emulate "unify all" but will let you explore the proof tree. I've implemented that with an intention this may help to understand why "unify all" doesn't find some particular assertion if a user believes it should be found. Clicking on ✗ also launches the bottom-up prover with similar parameters as for ? but with logging level = 2. The intention is the same - to give a user ability to explore the proof tree.

Label: click=visualization IF there's a green checkmark (must use unification to get that), long-click = edit

That's correct.

Step type: click=show/hide justification (when they aren't always shown), long-click=edit step type via dropdown

That's correct.

Justification: Click = edit, long-click no different.

Currently - yes, however long-click is not supported currently for justifications. But probably I will change this, please keep reading, I am explaining this below.

Statement: Click = edit, long-click = select statement fragment

By default - yes. But this is configurable in the settings. I strongly prefer the opposite: click=selection. And I actually set it this way in my settings. But I made click=edit by default because there was an ask in the Google Metamath group to edit by click by default.

More generally, the mapping seems inconsistent. Editing is sometimes a long click and is sometimes a short click, depending on the field. I think that in an editor (at least) a "simple click" should always cause an edit if an edit makes sense, as that would be more consistent. The long-click would be used for some other behavior (like fragment selection). So I suggest this default mapping:

  • Checkmark: Click = show compressed proof; Long-click visualization toggle
  • Label: click=edit; long-click=visualization toggle
  • Step type: click=edit (step type via dropdown), long-click: show/hide justification
  • Justification: Click = edit, long-click visualization toggle.
  • Statement: Click = edit, long-click = select statement fragment

I agree, the mapping is inconsistent. I have a different solution in mind which also makes mappings consistent. Please check if you also find the below consistent. My idea of consistency is as follows. Manual typing requires increased mental efforts comparing to clicking. Long-clicking also requires a bit increased mental efforts than short-clicking (you have to wait for a moment and keep a finger or mouse not moving during this time). I think it will be consistent if long-clicking is associated with something which requires increase of mental efforts or which is rarely needed. And short clicking is associated with something simple and fast. Therefore, the mapping I am thinking of is as follows:

As you can see, short-clicking on either of the first three UI elements (Checkmark, Label, Step type) toggles justification/visualization. This should decrease probability of mis-touching.

Also assigning long-clicking to "edit" actions resolves the inconsistency with editing the description.

Assigning short-clicking to fragment selection resolves another inconsistency not discussed so far. Currently, in the proof explorer, short-click = fragment selection. Long-click is not supported in the proof explorer, because it involves some technical issues. I implemented long-clicking by storing a small state object for each symbol and each space between symbols. I am not expecting this to be a problem in the editor because I am not expecting it will be used to create very long proofs. But in the proof explorer there are a lot of proof steps, especially if inessential steps are shown. Storing a small state object for each symbol and space between them would be too much overhead. I am not ready to implement a more efficient solution at the moment. So, assigning short-click for fragment selection in the editor will make it consistent with the proof explorer.

Showing a compressed proof is a very rare action, so I don't see any problem with assigning this action to a long-click. Moreover, there is an issue "Make it more obvious how to get a completed proof" (https://github.com/expln/metamath-lamp/issues/11), so most probably I will implement a separate menu item for that in the "hamburger" menu.

I note this now because I want to talk about the UI in my video, so if the default mappings are going to get changed I'd like that to happen sooner :-).

Thanks for pointing this out now, this is really an important item to think on!

expln commented 1 year ago

@david-a-wheeler please check my comment above. What are your thoughts on the mapping I described?

david-a-wheeler commented 1 year ago

Hmm!! Not the direction I was thinking of going, but you're right, the approach you outlined above would resolve the UI inconsistencies. It'd also quietly fix the inconsistencies in some other areas, such as the explorer, proof tabs (I did notice that), and how you edit the description field.

The new rule is simple: "it's always long click to edit; both alt+click and long-tap is considered a long click. A short click selects or reveals information."

So yes, these proposed mappings as the defaults make sense to me! The concerns I had with that earlier seem to have been addressed by (1) adding support for long-click as an alternative to alt+click, and (2) keeping the ability to change the default meaning of click & long-click when operating on a statement within the editor. I do think it's important to be able to swap that specific UI item, since editing statements is something some people will do a lot of. If the default is consistent, but it can be changed, that sounds great.

BTW: I don't know if you've considered #42 - add a "paste" button on the fragment selector, that if used during editing, copies the clipboard onto the selected items. If that might be added some day, then using short-click to select a statement fragment makes even more sense, because it provides an easy way to edit a statement without necessarily "opening it up for arbitrary edits".

There are also other options: Clicking on ? launches the bottom-up prover with search depth = 1, logging level = 1 ... this may help to understand why "unify all" doesn't find some particular assertion Clicking on ✗ also launches the bottom-up prover with similar parameters as for ? but with logging level = 2.

I like that!

Okay, this wasn't what I originally had in mind, but you've convinced me. Thanks for taking the time to discuss this!

expln commented 1 year ago

So yes, these proposed mappings as the defaults make sense to me!

Great! I will include it into v11.

The concerns I had with that earlier seem to have been addressed by (1) adding support for long-click as an alternative to alt+click

Yes, support for long-click makes UI easier to use.

I do think it's important to be able to swap that specific UI item, since editing statements is something some people will do a lot of. If the default is consistent, but it can be changed, that sounds great.

I agree. Users also may develop their own Metamath databases where fragment selection may not work well. In such scenarios, editing statements will be the only available option.

BTW: I don't know if you've considered https://github.com/expln/metamath-lamp/issues/42 - add a "paste" button on the fragment selector, that if used during editing, copies the clipboard onto the selected items. If that might be added some day, then using short-click to select a statement fragment makes even more sense, because it provides an easy way to edit a statement without necessarily "opening it up for arbitrary edits".

Yes, I noticed that proposition and I like it. But I decided to move it out from v11 scope. Most probably it will be in v12.

david-a-wheeler commented 1 year ago

Great!

Yes, I noticed that (paste) proposition and I like it. But I decided to move it out from v11 scope. Most probably it will be in v12.

Agreed. Paste would be cool, but there's no reason to delay v11 for that.

I would like the v11 to be a relatively stable UI, so v11 should be the one that (re)assigns click and long click. That will increase the likelihood of a video being "not too wrong" in the future.

I would also prefer that it allow for future growth. In particular, I'm hoping that someday you'd be able to short-click within a justification: click on a hyp to jump to the step, or click on the ref to open a tab on the named reference. There's no need to implement that now, just don't make that harder in the future.

expln commented 1 year ago

This is implemented on dev as discussed:

The new rule is simple: "it's always long click to edit; both alt+click and long-tap is considered a long click. A short click selects or reveals information."