Idea: New fragment selector button "insert or elide"

[david-a-wheeler]

I can't figure out a good way to help handle parentheses in "edit" mode. I think the fundamental problem is that the editor can't know which part of the expression you care about. But there's already functionality for this - the fragment selector.

So I propose adding a new button to the fragment selector, "Insert or Elide", with icon "+A".

This would let you insert text, plus the parentheses that surround it, in a way sensitive to fragments. It would even let you insert text "on both sides", e.g., of an equation. It'd also let you elide (remove) text in a way that automatically handles parentheses.

When you click on it, it pops up a dialogue box (mockup below) that lets you insert or elide text in a fragment-aware way. The heading just says "Insert or Elide" It then shows the field name "Initial:" followed below by a copy of whatever fragment had been selected. In this case, "A = B".

Then there are checkboxes (all checked by default):

• Insert (else elide) - normally this inserts new text, but if unchecked this will elide some text of the fragment.
• on left (else right)
• on both sides (else one side)

I am intentionally picking checkboxes and NOT dropdowns - dropdowns take longer to manipulate, and you want this selection process to be fast. There are only 2 options in each case, too, making dropdowns pointless.

This followed by:

• An editable box for the "start of parentheses" symbol, "(" by default. It can be empty. If you edit this, its corresponding "end of parentheses" symbol is updated.
• An editable box of what to insert. I drew two boxes, but I just realized that 1 are unnecessary, one will do & might be easier to use. If "insert" is not checked, this editable box disappears.
• The fixed text "initial" ("what to insert" and "initial" are swapped in position with "on left" is unchecked).
• An editable box for the "end of parentheses" symbol, ")" by default. It can be empty. Editing this doesn't change the "start of parentheses" symbol in case you're doing an unusual pair of "parentheses".

Then the fixed text "Result:"

This is followed by the calculated result based on what's above. The result is updated whenever the inputs are changed. The calculations are pretty simple, e.g.:

• Initial "A = B" with "insert" "left" "on both sides" with text "(" "1 +" ")" would produce "( 1 + A ) = ( 1 + B )".
• Initial "A = B" with "insert" "left" "NOT on both sides" with text "(" "1 +" ")" would produce "( 1 + (A = B ) )".
• Initial "A = B" with "insert" "NOT left" "on both sides" with text "(" "+ 1" ")" would produce "( A + 1 ) = ( B + 1 )".
• Initial "( A + B )" with "NOT insert" "left" "NOT on both sides" with text "(" ... ")" would produce "B".

Under this is what to do with the results (these might be icons):

• Copy - Copy to clipboard
• Cancel
• Initial - Copy the reult into a new "initial" value, for insertion inception. You might also want an "undo" button on this row.
• Paste - (only in editor) paste into the current fragment selection
• Step above / step below - create a new step using the result as the step's statement (after a copy of the original typecode).

I put this into a single dialogue box because "initial" looks handy & it'd be hard to understand if it weren't all in one dialogue box.

Here's a mock-up picture.

[david-a-wheeler]

I picked "+A" as the icon because "A+" looks like a grade, "+1" looks like a vote, and "1+" looks like a hint at "one or more" (which isn't the point). If the icon is "+A", maybe the checkbox should be "on the right" instead of "on the left".

[david-a-wheeler]

Also, in the result, the parentheses & editable box outcomes should be marked somehow, perhaps surrounded by a box (like visualization). The editable box, if empty, should still be obvious somehow (e.g., as a box or underlined empty area).

[expln]

That's a good idea. I also was thinking on implementing of different "smart" actions on selected fragments. For example, swapping left and right, applying associativity law (e.g. transforming ( a op ( b op c ) ) to ( ( a op b ) op c )), etc. The one you proposed is also very good, I will implement it too. I am also thinking if it is possible to do something very generic when users define transformation changes via regexp and/or some special language. In that case such transformations will not be hardcoded and users will be able to define custom ones without waiting for them to be implemented in mm-lamp.

[david-a-wheeler]

I also was thinking on implementing of different "smart" actions on selected fragments. For example, swapping left and right, applying associativity law (e.g. transforming ( a op ( b op c ) ) to ( ( a op b ) op c )), etc. The one you proposed is also very good, I will implement it too. I am also thinking if it is possible to do something very generic when users define transformation changes via regexp and/or some special language.

Cool, great minds think alike :-). I'm sure it's possible to define a special language, but I don't think users will want to define a language for simple cases. Having a few buttons to quickly apply "common cases" should be fine for now. After undo/redo, full unification, and a few other goodies, I imagine it'd be useful to eventually implement a full language for processing. However, I think that'd be a longer-term effort, best done after other things are addressed.

[david-a-wheeler]

I think the "basic" operations are something like:

• Insert, e.g., X => ( X + A ).
  • "Both sides", e.g., X = Y => ( X + A ) = ( Y + A )
  • left/right side
• Elide, e.g., ( X + A ) => X
  • left/right side
• Commute (swap), e.g., X = Y => Y = X
• Associate as above, e.g., ( A + ( B + C ) ) => ( ( A + B ) + C )

I think all of them would sensibly have a "both sides" option, though that doesn't mean that should be implemented.

There are a lot of ways to do this: dialogue box, menus with submenus, etc. As always, easy is good, and having some feedback of "this is what it will look like" before doing it would be helpful.

[expln]

I understand that it is better to implement something which is very specific but at least works, than something very generic which will require more time for implementation. But it is very boring for me to implement that simple and straightforward solution :) I don't want mm-lamp to turn from a hobby project to a "second job" for me :)

Currently I am considering two possible implementations. One is as you suggested when there is a dialog with few options which affect the final result. Another is a list where each list item shows a ready result (with background highlighting to understand the change faster), so users can see what is available in current context and can click it to select. Clicking one of the list items may open another dialog where the user will have to provide some additional data, for example, what new text to add, and chose how to apply the result - replace existing or add a new step below/above. I will chose which one to implement later. However, since I am considering the "customizable" version of this feature, the later approach seems more suitable.

As the language for custom transformations, I think, I will use regular JS which I will "evaluate" in a sandboxed iframe. So users will not have to learn a very specific new language. The transformations you mentioned will be available as a predefined ones in the settings. However users will be able to add their own ones if they need by adding some JS code in the settings.

[david-a-wheeler]

I understand that it is better to implement something which is very specific but at least works, than something very generic which will require more time for implementation. But it is very boring for me to implement that simple and straightforward solution :) I don't want mm-lamp to turn from a hobby project to a "second job" for me :)

You know your own motivations best, so if you want to go elaborate, enjoy!!

Currently I am considering two possible implementations. One is as you suggested when there is a dialog with few options which affect the final result. Another is a list where each list item shows a ready result (with background highlighting to understand the change faster), so users can see what is available in current context and can click it to select.

Both approaches make sense to me. To me a key would be to "only enter what you need", that is, if you're doing "( ... + 1 )" on both sides, you shouldn't need to enter "+ 1" twice. Bonus points if you can paste from the clipboard into the "main" text entry area in a dialogue box.

I suggest just letting it stew in your subconscious for a bit, sometimes the best results come from that.

In any case, I think this is all much less important than undo/redo and full unification.

[david-a-wheeler]

Another is a list where each list item shows a ready result (with background highlighting to understand the change faster), so users can see what is available in current context and can click it to select. Clicking one of the list items may open another dialog where the user will have to provide some additional data, for example, what new text to add, and chose how to apply the result - replace existing or add a new step below/above.

That's an interesting approach. As I mentioned earlier, I think this is less important than undo/redo or full unification, but it's definitely worth discussion.

That would be flexible (especially if you can easily add your own). Let's call these "tranforms" so we have a name. I was wondering how to make it so commonly-used transforms would be quick to select. Here's one idea: establish a convention where the name is a comma+space separated list of terms. The user could type into a search box, and each alphanumeric should select only the case where the first alphenum in search matched the first term alphanum in the name, the second the second, and so on. I think matching should ignore upper/lowercase to make it easier on smartphones. E.g., if you have:

• Associate, 1-sided, left
• Associate, 1-sided, right
• Associate, both sides, left
• Commute (swap), 1-sided

Then when the user enters "a" into the search bar only the "Associate" ones are displayed, then when the user makes the search "a1" then only the "Associate, 1-sided" ones are still displayed, etc. At any time the user could select an option left over, which would also show the result of that selection.

Also: I suspect the "add new step below/above" should be for the whole expression, not just the selected fragment, or at least that should be an option.

Anyway, I thought I'd share the idea.

[expln]

@david-a-wheeler

This feature is ready on dev. I plan to do some small changes to it (also depending on feedback if any), but its main functionality is ready.

There are two new settings on the Settings tab - "Use default transforms" and "Use custom transforms". The latter one allows to write custom transforms on JavaScript. At the moment I am not providing a documentation on how to write custom transforms. Partially because I may change the API soon. But eventually I will write such a documentation. Most probably I will put it as comments into the default transforms script. The default transforms script is available by clicking "View default transforms" to the right of the "Use default transforms" setting. The default transforms are written the same way as custom ones can be written. The default transforms are read-only but they could be used as an example of how to write custom transforms.

I picked "+A" as the icon because "A+" looks like a grade, "+1" looks like a vote, and "1+" looks like a hint at "one or more" (which isn't the point). If the icon is "+A", maybe the checkbox should be "on the right" instead of "on the left".

I chose another icon - an icon with a circle and a square. I interpret it as "changing shape". The proposed "+A" is also good. But it is very similar to the substitute icon ("A" with an arrow below), so I decided to pick something very different.

Also, in the result, the parentheses & editable box outcomes should be marked somehow, perhaps surrounded by a box (like visualization). The editable box, if empty, should still be obvious somehow (e.g., as a box or underlined empty area).

I implemented highlighting of the added/removed text and/or of the parts being moved.

I think the "basic" operations are something like...

I've implemented all the proposed basic operations. Please check if anything from the initial proposal is missing. I tried to implement all the mentioned cases.

I was wondering how to make it so commonly-used transforms would be quick to select. Here's one idea: establish a convention where the name is a comma+space separated list of terms. The user could type into a search box, and each alphanumeric should select only the case where the first alphenum in search matched the first term alphanum in the name, the second the second, and so on. I think matching should ignore upper/lowercase to make it easier on smartphones.

Current implementation is very simple. There is a list of available transforms, and you just select one and then configure it with its specific parameters and see the result. However, if needed, the search capability could be added too in the future.

Also: I suspect the "add new step below/above" should be for the whole expression, not just the selected fragment, or at least that should be an option.

Yes, the whole expression is added as a new step.

[david-a-wheeler]

Nevermind my earlier comment, this is a fragment selector so I have to invoke the fragment selector icon bar. Hmm, maybe I need some sleep :-).

[david-a-wheeler]

The new fragment selector doesn't seem to be working currently. If I select "(3 + 1)" or anything else in 2p2e4 when set.mm is fully loaded as the context, I get this error message:

Error: [3] Cannot parse transforms: t._0 is undefined

[expln]

Could you please check that the setting "Use custom transforms" is unselected, and "Use default transforms" is selected? I reproduced Error: [3] Cannot parse transforms: t._0 is undefined in Firefox when I checked "Use custom transforms" but I have not provided any script for custom transforms.

[david-a-wheeler]

Great! Turning off "Use custom transforms" does seem to fix it. It would be nice to have a clearer error message in this case :-).

I plan to play with it more, but it looks really awesome as a first cut.

A few comments/nits:

• Having two transforms with the same name is confusing ("Insert"). I suggest the latter one have a different name, e.g., "Insert two-sided" or "Two-sided insert".
• Eventually all of these transforms should have two-sided variations. That's not necessary for a release, just a nice direction to head towards. However, I think the "two-sided" variations are where the transforms really start showing their value, because suddenly you're doing 1/2 the work and ensuring that they're happening in the right place.
• Once there are many two-sided variations, maybe the "two-sided" ones should be in their own group (show the non-two-sided ones, then the two-sided ones).
• There are a number of checkboxes where only one can be selected. It seems to me those should be displayed as radio buttons instead (that is, instead of square checkboxes they should be circles with a dot inside the selected option). Checkboxes are usually used when selections are independent, while radio buttons suggest that it's one of a set of mutually exclusive options.
• The big dialogue box (after selecting the transform) doesn't clearly indicate the name of the transform being used. I think at the dialogue box should clearly show the name of the transform as a constant (maybe in bold or italics) to make it clear what transform is being used.

This looks really awesome!

[expln]

Thank you for the feedback! I will check what I can do.

[david-a-wheeler]

I found these URLs about radio buttons in React/Material Design, they might be helpful to you:

• https://mdbootstrap.com/docs/react/forms/radio/
• https://coreui.io/react/docs/forms/checks-radios/

[expln]

Thanks, David. I will use radio buttons similar to the ones in the bottom-up prover for "Logging level".

[david-a-wheeler]

A few more thoughts:

On elide, "left" should say "Keep left" and "right" should say "Keep right". It's not eluding the left, it keeps the left (for example). I like what it does, I just think the labels are confusing.

This is good stuff. I plan to add a new section in the tutorial showing how to use them.

[expln]

@david-a-wheeler

I addressed some of your suggestions and updated dev. Please check how it works now.

Having two transforms with the same name is confusing ("Insert"). I suggest the latter one have a different name, e.g., "Insert two-sided" or "Two-sided insert".

I merged those two "Insert" items into one menu item. Now you may select the single "Insert" and then there is an option "one-sided" or "two-sided".

Eventually all of these transforms should have two-sided variations.

I added the two-sided variation for Elide. But Swap and Associate will be one-sided for now.

[david-a-wheeler]

Merging two-sided into elide & insert makes sense & looks good. Eventually it'd be nice for swap and associate to grow two-sided versions, but that's not necessary for a release.

I suggest that the "no parentheses" etc. row be after the other configuration options. In practice, I find that I must answer "is this two-sided", then "left or right?" then "what text to add (for insert)", and then finally the parentheses question. It's hard to answer the parentheses question without answering the other questions first.

Is there a way to show a highlighted space in an "insert" when there's no text (yet) to insert? It's currently not obvious where the inserted text will appear in the result until you type something in. Once you enter some text, the highlight makes things clear, but when there's no text there's no highlight to help.

Thanks so much! I think this is a nifty feature. I've started writing the tutorial text to go with it.

[expln]

The latest suggestions are implemented on dev (except of two-sidedness for swap and associate for which I don't have time as of now)

I plan to improve info messages which appear when something is not working and also add a warning about using JS code in custom transforms. And then I will release this feature. As of instructions how to write custom transforms, I will postpone this a bit, depending on how big demand would be on writing custom transforms. If people start asking questions how to do this I will write a documentation taking into account that questions.

[david-a-wheeler]

The latest suggestions are implemented on dev

Awesome!

(except of two-sidedness for swap and associate for which I don't have time as of now)

That makes complete sense. I don't think their lack should block release. There's always another transform you could think of :-).

I plan to improve info messages which appear when something is not working and also add a warning about using JS code in custom transforms. And then I will release this feature. As of instructions how to write custom transforms, I will postpone this a bit, depending on how big demand would be on writing custom transforms. If people start asking questions how to do this I will write a documentation taking into account that questions.

That makes sense. Again, I don't think any of that should block a release. I suspect other items, such as full unification and basic automation, are far more important really. These simple transforms cover many common cases.

[expln]

I suspect other items, such as full unification and basic automation, are far more important really.

I continue working on full unification. But it doesn't look very easy. So I plan to implement it bit by bit. The next bit will be to add it to the search - find all available assertions which "full-unify" with a given statement.

As of basic automation, I plan to add something similar to macroses when users will be able to write their JS code to manipulate the editor state and have programmatic access to some of the available features like search, substitute, bottom-up prover. Technically this should not be difficult. What I have to do is to provide bindings from custom JS code to the internal code. That will be similar to custom transforms but on a bigger scale. I want to do this in three steps: 1) Divide the mm-lamp code onto UI dependent and UI independent parts. And then publish the UI independent part as an npm module. 2) Create a project with examples how to use the "mm-lamp-as-npm-module" to create standalone JS programs to do some useful things with Metamath databases programmatically. 3) Add possibility to write JS macroses in mm-lamp website using approaches from the previous step.

Creating the npm module first and then using it in standalone programs will help me to come up with better JS bindings for macroses.

[david-a-wheeler]

I continue working on full unification. But it doesn't look very easy. So I plan to implement it bit by bit.

I understand. If you have a specific problem, I encourage you to ask Mario Carneiro. He's a genius and a nice person. As you know, he's already provided the general outline on how to efficiently do full unification. His problem is lack of time, so it's good to try to focus on a specific question for him.

[expln]

If you have a specific problem, I encourage you to ask Mario Carneiro.

Yeah, that's what I will probably do soon.

[expln]

This feature is available in version 18. I don't announce it in the Metamath group, because I decided to collect few more features and announce all at once.