|
boris@cs.caltech.edu http://www.cs.caltech.edu/~boris |
| 1 Introduction
Juno-2 is an extensible constraint-based drawing editor created by Greg Nelson and Allan Heydon [1], which was originally designed for producing high-quality still illustrations. Juno-2 permits arbitrary constraints to be specified using a declarative notation based on the theory of real numbers with a pairing function and equality. After the constraints have been specified, any degrees of freedom that remain in the drawing may be adjusted interactively with the mouse. Thus, Juno-2 makes it easy to illustrate and to explore virtually any geometric construction in the Euclidean plane. Long before my internship, Allan and Greg had written in the Juno language [2] a module for playing animations [3]. Greg had animated a fragment of Archimedes's reasoning for the area of the circle. Most SRCers who had seen Greg's animation thought that it communicated superbly the crux of Archimedes's proof. My job this summer was to extend Juno-2 with features that would make it easier to produce such animations. 2 DimiTeX One difficulty that Greg had encountered in animating Archimedes proof was that typesetting mathematical formulas with Juno-2 was a very tedious task. In order for Juno to display πr2, Greg had to type a 30 line program that switched the current font to "Symbol" and back again as the letter π was displayed, and then raised the superscript "2" up by one-third of the current font's height. Because Greek letters, mathematical symbols, superscripts and subscripts occur commonly in proofs, I implemented a subset of TeX's functionality in Juno. My implementation, which Greg named DimiTeX, mostly adheres to TeX's syntax; however, DimiTeX's escape character is the exclamation mark '!', because the backslash '\' was already taken by Juno. For example, here is what we would have to type in Juno-xyt for the formula πr2 to appear at position a. DimiTeX.Show(a, "$!pi r^2$") Greg wrote the documentation for DimiTeX's syntax which is included in the Juno-xyt manual page. Some proofs use symbols that are not available in the bundled PostScript and X fonts. With Juno, it is easy to draw a new symbol and to encapsulate the resulting closure as a DimiTeX glyph. This glyph can be bound to a DimiTeX control sequence, such as "!mynewsym". (Even animated drawings can be encapsulated as DimiTeX glyphs. That's how we created the DimiTeX "!circle{...}" macro, which slowly draws a circle around any formula.) While dragging a compound formula across the screen, I observed a
curious effect which Greg called "rounding flicker". Consider the distance
between a superscript and a subscript in the same 3 Animation An animation can be fun even if it does not prove a theorem. Early in the summer, Greg and I created an animation showing how a calligrapher might write "Juno xyt". Juno-2 already had a calligraphic pen that could be easily applied to the current PostScript path. Still, given a PostScript path which consists of a few dozen Bezier segments, how would you draw that fraction of the path which is visible in the animation's current frame? We first solved this problem for a single Bezier segment by using De Casteljau's construction. That is, we obtained Bezier control points for the visible fraction of our segment by nesting a number of simultaneous "sliders". (After this exercise, we created a graphical slider in the Juno user interface and connected it to the Juno variable "UISlider.val"). Then we encapsulated each segment of the PostScript path into a separate animation closure. Finally, we defined a new composition primitive called "Seq2" which right-reduced the list of single-segment animations into a single closure that animated the entire path. Toward summer's end, we used the same "Seq2" to tie together the steps of a calculational "Feijen style" proof that the Fermat numbers (2 exp 2n)+1 are pairwise relatively prime. Actually, only two of the animated slides in that proof were "Feijen style" --- more traditional "title slides" stated the results that were to be proved. We grouped the various slides into "scenes" so that slide transitions within a scene were made automatically by Juno, whereas "show mode" transitions from one scene to the next would occur only in response to user events. We also implemented a "Scene menu" in the user interface that allowed us to view the scenes in random order while working in "edit mode". Edit mode is the mode that Juno starts in; show mode is a mode for giving full-screen presentations that we added this summer. 4 Conclusion Some of the extensions that we added this summer -- for example DimiTeX -- work just as well in Juno-2 as they do in Juno-xyt. Although this is also true of the last and the least trivial to implement addition that I will describe --- a facility for unfolding and refolding predicates and templates and for "narrowing" predicates --- we were not hard-pressed to make this addition to Juno until we started producing larger animations. That's because still illustrations seldom use the same predicates and the same templates instantiated over and over for the exact same parameter values, which would be required for automated editing operations to pay off. But that's just what happens in slide shows and animations --- they usually consist of many scenes all of which are derived from the same template. For example, all scenes in Greg's animation of Archimedes's proof display a caption at the exact same anchor point. What if, while editing scene N, Greg needed to move down that anchor point in order to make room for a larger caption? In Juno-2, he would have had to edit manually all other scenes in addition to editing scene N (please note that storing the anchor point in a global variable is not a valid option, because there may be non-trivial constraints relating the anchor point to other points in the same template). In Juno-xyt, Greg would get away by editing just the common template --- assuming that he has read the "Using Schemes" section of the Juno-xyt manual page. 5 References 1. Allan Heydon and Greg Nelson,
2. Greg Nelson and Allan Heydon,
3. Allan Heydon and Greg Nelson,
|