Filling Typed Holes with Live GUIs
Filling Typed Holes with Live GUIs
复制标题
使用实时 GUI 填充键入的孔
DOI：
10.1145/3453483.3454059
复制
发表时间：
2021
期刊：
影响因子：
--
通讯作者：
Chugh, Ravi
中科院分区：
文献类型：
--
作者：
Omar, Cyrus;Moon, David;Blinn, Andrew;Voysey, Ian;Collins, Nick;Chugh, Ravi
文本编辑功能强大，但某些类型的表达式更自然地以图形方式表示和操作。示例包括计算颜色、音乐、动画、表格数据、绘图、图表和其他特定于域的数据结构的表达式。本文介绍了live literals，或livelits，它允许客户端通过直接操作持久嵌入到代码中的用户定义GUI来填充这些类型的漏洞。独特的是，livelit是组合的：livelit GUI本身可以嵌入拼接表达式，这些表达式是有类型的，有词法作用域的，并且可以反过来嵌入其他livelit。Livelits也是一个很好的live：即使当拼接提到绑定变量时，Livelit也可以提供关于客户机选择的运行时含义的连续反馈，因为系统连续地收集与Livelit正在填充的洞相关联的闭包。我们将livelits集成到Hazel中，这是一个活洞驱动的编程环境，并描述了运用这些新功能的案例研究。然后，我们定义了一个简单类型的livelit演算，它指定livelit如何作为实时图形宏操作。宏观扩张的元理论在阿格达已经机械化了。
Text editing is powerful, but some types of expressions are more naturally represented and manipulated graphically. Examples include expressions that compute colors, music, animations, tabular data, plots, diagrams, and other domain-specific data structures. This paper introduceslive literals, orlivelits, which allow clients to fill holes of types like these by directly manipulating a user-defined GUI embedded persistently into code. Uniquely, livelits arecompositional: a livelit GUI can itself embed spliced expressions, which are typed, lexically scoped, and can in turn embed other livelits. Livelits are also uniquelylive: a livelit can provide continuous feedback about the run-time implications of the client’s choices even when splices mention bound variables, because the system continuously gathers closures associated with the hole that the livelit is filling. We integrate livelits into Hazel, a live hole-driven programming environment, and describe case studies that exercise these novel capabilities. We then define a simply typed livelit calculus, which specifies how livelits operate as live graphical macros. The metatheory of macro expansion has been mechanized in Agda.