Home

Awesome

Unicode-Input: Agda and HTML-style Unicode character input in PowerToys Run

Build Pipeline

Introduction

TLDR: this plugin lets you type \ne and get ≠ typed or in your clipboard, × and get ×, 😝 to get 😝, or thousands of other combinations!

Do you often need to type unicode symbols like ™ or ≤? Do you have the wikipedia page for box drawing characters saved as a bookmark? Have you ever tried to write digital notes about Agda outside of Emacs? This might just be the plugin for you!

Unicode-Input is a PowerToys Run plugin that emulates the input capabilities of both HTML entities and Emacs in agda-mode.

If you are unfamiliar, Agda's input method allows you to type the Latex form of (almost) any character - this will then be replaced with the equivalent unicode character in your document, allowing for very the construction of very dense programs!

For example, you can type \lambda and the plugin will either copy λ into your clipboard or enter λ into your current document, depending on how you have it configured. For some longer latex strings, such as \mathbb{N} (for ℕ), a shorter version is often - in this case, you would type \bN. It's not just limited to mathematics - for example, you could type \'a to get the accented character á

HTML entities attempts to accomplish a broadly similar task (representing unicode characters with text), but are slightly more verbose in cases.

This plugin is based upon a complete export of Agda's input mapping library and WHATWG's entity mappings - as such, any alias that works in Agda or in your browser should also work here!

Installation

Automatic Installation (winget)

This doesn't work yet, sorry!

Manual Installation

  1. Go to the latest release and download the .zip file that matches your architecture - this is probably x64 if you are unsure.
  2. Close PowerToys
  3. Locate your plugin installation folder: for me, this was ~\AppData\Local\Microsoft\PowerToys\PowerToys Run\Plugins
  4. Copy the plugin folder from the zip into this folder (such that the path ...\PowerToys Run\Plugins\UnicodeInput\plugin.json exists)
  5. Open PowerToys and enable the plugin!
  6. (optional) Decide whether you want to use it in clipboard or typing mode - there is a checkbox to toggle this
  7. 🥳

Development / Contributing

Attribution