07 / Reference
Reference
Shortcuts, commands, menus, file formats and vocabulary — the things you
look up rather than read.
Keyboard shortcuts
| Keys |
Action |
| Ctrl + N |
New workspace |
| Ctrl + O |
Open a .bfj file |
| Ctrl + S |
Save the workspace |
| Ctrl + J |
Toggle the bottom dock |
| Ctrl + Shift + F |
Search blocks |
| Ctrl + F5 |
Run the program |
| Ctrl + Shift + P / F1 |
Command palette |
Arrow keys navigate between tabs on the FJ Inspector and the bottom dock, and along a resizer
handle once it has focus.
Command palette
Ctrl + Shift + P or F1, fuzzy-searchable and grouped
by category:
| Group |
Commands |
| File |
New · Open… · Save · Export FJ source…
· Restore Autosave |
| Run |
Run program (Ctrl + F5) |
| Analysis |
Show Typing Derivation · Show CK Machine · Show Reduction ·
Show Problems |
| View |
Toggle Sidebar · Toggle FJ Inspector · Toggle Bottom Dock ·
Toggle Color Theme |
| Workspace |
Zoom In · Zoom Out · Zoom to Fit |
| Perspective |
Edit · Debug · Type Analysis · Presentation |
| Preferences |
Settings · Autosave Interval… |
| Menu |
Contents |
| File |
New · Open… · Save · Export… · Restore
Autosave |
| Examples |
The nine programs listed in Overview, with a
Replace/Merge prompt when the workspace already has blocks |
| View |
Sidebar · FJ Inspector · Bottom dock · Perspective picker
· Dark theme |
| More |
Command Palette… · About BFJ |
The activity rail on the far left holds Blocks, Search Blocks, Run and
Analysis and Settings. The workspace title bar holds undo/redo, zoom, the
bottom-dock toggle and ▶ Run.
File formats
| Format |
Holds |
.bfj |
A BFJ workspace, as JSON. Saved and opened locally — nothing is
uploaded. |
| Local storage |
The rolling autosave backup, plus your layout, theme, autosave interval and
active tabs. A malformed payload falls back to the default layout rather than
failing to start. |
| FJ / Java text |
Not a saved file format on its own, but the Editable Code tab
round-trips a program as text — see
Translation — and .fj/.txt
files can be exported or opened directly through that same parser. |
Glossary
| Term |
Means |
| Bijection |
The proved one-to-one correspondence between block trees and ASTs, and between
block trees and text under β/τ. See
Translation. |
| BFJ-Thrasos |
BFJ's renderer. Blockly's Thrasos plus connector shapes for FJ's non-terminals.
|
| CK machine |
Control + Kontinuation. No store — FJ has no mutable state, so there is
nothing to keep one for. |
| Featherweight Java (FJ) |
The minimal class-based OO core calculus (Igarashi, Pierce, Wadler) that BFJ
encodes as blocks. |
| Frame |
One hole-shaped piece of pending context in the CK machine's kontinuation, e.g.
◻.f. |
| Hole |
The type given to an empty socket. Consistent with everything, so unfinished
work never cascades into a diagnostic storm. |
| Kontinuation |
The pending work — what the machine still owes the value it is computing.
|
| Nominal subtyping |
Subtyping by declared extends, not by structure. |
| Override rule |
FJ requires an exact signature match on an override — no
covariant returns, no overloading. |
R-Field / R-Invk / R-Cast |
The three computation rules of the substitution semantics — field access,
method invocation, cast. |
| Stupid cast |
A downcast to an unrelated type. Type-checks under T-SCast with a
warning, but always fails at runtime. |
Elsewhere in the workshop
B-MJ help — MiniJava, where the machine gains an
extra letter: CESK's S is a
store, needed because MiniJava has mutable objects. BFJ's CK machine has no such letter,
because FJ has nothing to mutate.
