diff options
Diffstat (limited to 'gui.js')
| -rw-r--r-- | gui.js | 13 |
1 files changed, 12 insertions, 1 deletions
@@ -69,7 +69,7 @@ SpeechBubbleMorph*/ // Global stuff //////////////////////////////////////////////////////// -modules.gui = '2015-February-23'; +modules.gui = '2015-February-28'; // Declarations @@ -2267,6 +2267,17 @@ IDE_Morph.prototype.settingsMenu = function () { 'check to prioritize\nscript execution' ); addPreference( + 'Cache Inputs', + function () { + SyntaxElementMorph.prototype.isCachingInputs = + !SyntaxElementMorph.prototype.isCachingInputs; + }, + SyntaxElementMorph.prototype.isCachingInputs, + 'uncheck to stop caching\ninputs (for debugging the evaluator)', + 'check to cache inputs\nboosts recursion', + true + ); + addPreference( 'Rasterize SVGs', function () { MorphicPreferences.rasterizeSVGs = |
