This is the source code for Pantograph, a structure editor. It was written by Jacob Prinz and Henry Blanchette.
POPL 2025 paper: Pantograph: A Fluid and Typed Structure Editor.
Watch the Pantograph presentation.
Table of Contents
Unlike a traditional code editor in which text is parsed and then typechecked, Pantograph operates directly on a typed syntax tree.
Users may fill in typed holes to input programs, here by inserting a list l2:
Many existing structure editors allow the user to fill holes, and manipulate entire terms. But how can one edit existing programs? In particular, suppose that the programmer realizes that l2 never contains negative numbers, and decides to optimize the expression by moving the execution of the append operation to after the filter.
To make this edit by only manipulating entire terms would be difficult. One could imagine various user interfaces, but generally the manipulation would look like this:
Pantograph makes edits to existing program easier by introducing a notion of a tree selection. If a text selection goes between two text cursors, and a tree cursor goes on a subtree, then a tree selection goes between two subtrees. It is the area inside one subtree and outside another, also known as a one-hole context. Using this notion, the programmer can make the above edit easily:
Even better, it turns out that nearly all common program edits on functional code have this form:
We call this editing scheme with tree cursors and selection zipper editing.
Zipper editing, like the traditional structure editing it extends, preserves the syntactic well-formedness of programs. However, it does not necessarily preserve well-typedness.
Any system that aims to operate on intrinsically typed terms needs to account for how such an edit changes types in the program. In Pantograph, every edit is a typed refactoring operation.
When the user inserts a λ expression around the body of map, Pantograph automatically makes the edits necessary to keep the program well typed. The system adds an application to a hole at the two call sites, and alters the type signature.
Pantograph fully takes into account the intrinsically-typed structure of the program, so it can handle more deeply-nested edits, for example, adding a higher-order argument.
Of course, it is not always desirable for an editor to fix typing issues automatically. Sometimes, Pantograph leaves errors in the program for the user to fix later. For example, suppose that the user deletes the f parameter from a finished map function.
When the user makes the deletion, it leaves a couple of errors in the program. There is an unbound call to f, and an out of place argument at the two call sites to map. While the system could simply replace the former with a hole and remove the latter two from the program, this would likely erase valuable work that the programmer wanted to keep.
To allow such errors to exist in an otherwise well typed program, Pantograph has three final constructions:
- free variables e.g. in the first code example below, the references to
fafterλ fis deleted - commented applications e.g. in the first code example below, the argument
notwhich is given tomapeven thoughmaponly takes 1 argument afterλ fis deleted - type error boundaries e.g. in the second code example below,
(f h)andnotno longer have the correct type and Pantograph did not have a canonical way to fix it
To some extent, type error boundaries are similar to the type errors placed by familiar type checker. But they are actually first-class terms in the program. Below, the user deletes the type error boundary with a selection, which tell's Pantograph to update the surrounding program to fit the type inside the error boundary.
In the paper, we describe the math behind this typed refactoring system.
To develop Pantograph, you need the following command line tools installed:
To build the project:
pnpm install
pnpm buildTo serve the web application:
pnpm serveThis implementation is designed to be language-generic.
The Language.Pantograph.Generic.* modules implement the mechanics of a Pantograph editor given an editor specification.
To define a new editor, you must define a term of the type Language.Pantograph.Generic.Rendering.Base.EditorSpec l r, where l is the type of sort labels, and r is the type of derivation labels.
Additionally, l and r must instantiate Language.Pantograph.Generic.Grammar.IsRuleLabel l r.
One complete specific editor is given in the codebase, and can be found in Language.Pantograph.Specific.Currying.
The editor implemented here is the same as the one demonstrated in the Pantograph paper, used in the Pantograph paper's user study, and available in the runnable artifact (and hosted online at jeprinz.github.com/pantograph).
This is a good place to start in order to understand how to define a new editor.
Other related editor fragments can be found among the other Language.Pantograph.Specific.* modules.
The general paradigm behind how languages are implemented is described in Section 5 of the paper.
A language consists of a set of sorts (which are encoded trees of sort labels; see Language.Pantograph.Generic.Grammar.Sort), which are essentially the possible judgements, while a program is a derivation (which are encoded as trees of derivation labels, which are pairs of a derivation rule label and a rule variable substitution; see Language.Pantograph.Generic.Grammar.DerivTerm) of a sort.
The implementation in src/ is organized as follows:
Data.*modules contain miscelleneous generic data typesHalogen.*modules contain extra Halogen-related functionalitiesLanguage.Pantograph.Generic.*modules contain the language-generic implementation of PantographLanguage.Pantograph.Specific.*modules contain editor instances for specific languages- in particular, in the current version of the repository, only
Language.Pantograph.Specific.Curryingis fully implemented
- in particular, in the current version of the repository, only
Language.Pantograph.Lib.*modules contain useful functionalities for defining specific editor instances (for example, language-generically deriving the propagation rules as mentioned in the paper)Tutorial.*contains all the functionalities specific to the Pantograph tutorial (e.g. defining the tutorial UI and lessons)
To cite the Pantograph paper associated with this repository:
@article{pantograph,
author = {Prinz J, Blanchette H, Lampropoulos L},
title = {Pantograph: Pantograph: A Fluid and Typed Structure Editor},
journal = {POPL},
year = {2025},
doi = {10.1145/3704864}
}