12
$\begingroup$

I'd like to create a shortcut to convert a selected symbol, say \[Delta], into its rough equivalent formal symbol (i.e., \[FormalCapitalDelta]). That is, how does one create a shortcut to perform a front-end operation on a selected character?

This would only make sense for those single characters which have formal rough equivalents, so the shortcut should not do anything when multiple or a non-convertible single character is selected.

(comment: I'm finding formal symbols to be handy for function definitions where SetDelayed isn't a great idea (or turning an expression into a function Turning Expression into a Function: e.g., instead of

f[x_] := expensiveSymbolicFunction[x]

use

f[\[FormalX]_] = expensiveSymbolicFunction[\[FormalX]]

)

I find \[FormalCapitalDelta] (esc-.CapitalDelta-esc) tedious to type.

Improve this question
$\endgroup$

2 Answers 2

Reset to default
8
$\begingroup$

An alternative is to create a notebook containing all the automatic replacements using InputAutoReplacements:

enter image description here

Test:

enter image description here

Improve this answer
$\endgroup$
1
  • 1
    $\begingroup$ Nice. I've never seen InputAutoReplacements before. Thanks. $\endgroup$ Commented Jan 3, 2023 at 19:40
15
$\begingroup$

Here's an attempt:

Button["Formalize", NotebookWrite[EvaluationNotebook[], NotebookRead[EvaluationNotebook[]] /. s_String /; StringLength@s == 1 :> With[{res = ToExpression[ "\\[Formal" <> StringReplace[ CharacterName[s], { "LatinSmallLetter" ~~ l_ :> l, "LatinCapitalLetter" ~~ l_ :> "Capital" <> l } ] <> "]" ]}, ToString@res /; ! FailureQ@res ] ] ]

enter image description here

As can be seen, clicking the button replaces all single-letter symbols in the current selection by their formal counterpart. This is done by first getting the name of the symbol using CharacterName, then processing it to handle the different cases. Finally, it is converted back to the correct symbol using ToString[ToExpression["\["<>name<>"]"]]

Improve this answer
$\endgroup$
3
  • $\begingroup$ Thanks @Lukas, Well done. This works nicely. I'll accept as answered in a few days. I am hoping someone might offer a solution for the selected character only. $\endgroup$ Commented Jan 2, 2023 at 22:32
  • 1
    $\begingroup$ @CraigCarter I have updated the answer to only replace the contents that are explicitly selected $\endgroup$ Commented Jan 3, 2023 at 13:25
  • $\begingroup$ Very nice solution. Thanks $\endgroup$ Commented Jan 4, 2023 at 14:45

Start asking to get answers

Find the answer to your question by asking.

Ask question

Explore related questions

See similar questions with these tags.