// Placeholders (function(baselib) { var exports = {}; baselib.placeholders = exports; // Placeholders: same thing as boxes. Distinct type just to support make-reader-graph. var Placeholder = function(x, mutable) { this.val = x; }; Placeholder.prototype.ref = function() { return this.val; }; Placeholder.prototype.set = function(newVal) { this.val = newVal; }; Placeholder.prototype.toString = function(cache) { return "#"; }; Placeholder.prototype.toWrittenString = function(cache) { return "#"; }; Placeholder.prototype.toDisplayedString = function(cache) { return "#"; }; Placeholder.prototype.toDomNode = function(cache) { var parent = document.createElement("span"); parent.appendChild(document.createTextNode('#')); return parent; }; Placeholder.prototype.equals = function(other, aUnionFind) { return ((other instanceof Placeholder) && plt.baselib.equality.equals(this.val, other.val, aUnionFind)); }; var isPlaceholder = function(x) { return x instanceof Placeholder; }; ////////////////////////////////////////////////////////////////////// exports.Placeholder = Placeholder; exports.isPlaceholder = isPlaceholder; })(this['plt'].baselib);