yairchu on master
add failing test Fix red cursor when changing ta… (compare)
yairchu on master
Add failing test for punned fie… Fix punning of auto-named varia… (compare)
yairchu on wip
Add failing test for punned fie… wip (compare)
yairchu on master
Remove redundant parameter (compare)
yairchu on wip
Add failing test for punned fie… wip (compare)
yairchu on wip
Add failing test for punned fie… wip (compare)
yairchu on master
minor cleanups (compare)
yairchu on master
Use Compose Remove special case in emplace … (compare)
yairchu on master
Add failing test for new tag re… Fix failing test and regression… (compare)
yairchu on alt
Remove hole extra results: UI s… (compare)
yairchu on master
Remove unused exts (compare)
yairchu on master
dont pass redundant parameter (compare)
yairchu on ux-redo
replaceOptions wip (compare)
yairchu on ux-redo
Temporary broken state: Removed… (compare)
yairchu on master
Group TH boilerplate lines toge… (compare)
yairchu on ux-redo
Temporary broken state: Removed… (compare)
master
you can switch from coding in English and Hebrew!if x: 5 else: <"hello">
(angle brackets mark mismatch) I can press space on the <"hello">
fragment and it becomes if x: <5> else: "hello"
.Hi! I definitely agree that structural editors and rich IDEs are very suitable for proof assistants, and making a framework for those is certainly useful. But that's a pretty grand task and our focus in Lamdu for now is creating a single language and environment.
Where we can we try to apply good software engineering principles so we try to make our components as re-usable as we can and hopefully other folks could re-use them for other environments :)
In other words: for Lamdu, the optimal layout may not be ideal - as it may be chaotic: change too much between small incremental edits.
Also: Wadler's pretty printer, IIRC, prefers to split vertically as late as possible, so you get lots of tiny trees hanging at the end of a horizontal line.
We prefer the opposite: split vertically as early as possible (in the outer-most expression), and have the lower levels of the AST fit together horizontally in lines.