I wanted to use a specific Unicode character as an operator. It took a
little poking around, so I'm sharing my solution to save you some time.
First I looked at the file
github.com/JuliaLang/julia/blob/master/src/julia-parser.scm
Starting on line 9 is a grouping of all the operators supported by Julia.
Operators with the lowest precedence are at the top, those with the highest
precedence at the bottom.
I selected the character ⟺which is in the prec-arrow group.
The next problem was how to enter that character in the Julia console or in
IJulia (Jupyter). For that I wrote the following bit of code.
include("path\\to\\julia\sourcecode\\base\\latex_symbols.jl")
import Base.find
function find(dict::Dict, valuetofind::AbstractString)
for (k,v) in dict
if v == valuetofind return k end
end
""
end
find(latex_symbols, "⟺") # returns "\\Longleftrightarrow"
In the Julia console or IJulia type \Longleftrightarrow and press the tab
key to see it being converted to ⟺
Note: Some Unicode characters may show up as open boxes in your favorite
editor. This is because the current font does not support it. Use a
different font. Lookup "Unicode font" in Wikipedia to find one that might
work for you.
Enjoy.
