juicy-ace-editor.html

<script src="//leanprover.github.io/ace/ace/ace.js" type="text/javascript" charset="utf-8"></script>

<template>
    <style shim-shadowdom>
        :host{
            display: block;
        }

        polyfill-next-selector { content: ':host #juicy-ace-editor-container'; }
        ::content #juicy-ace-editor-container{
            width: 100%;
            height: 100%;
            display: block;
        }
    </style>
    <content></content>
</template>
<script>
(function(window, document, undefined) {
    // Refers to the "importer", which is index.html
    var thatDoc = document;

    // Refers to the "importee", which is src/juicy-ace-editor.html
    var thisDoc = document._currentScript.ownerDocument;

    // Gets content from <template>
    var template = thisDoc.querySelector('template').content;

    // Creates an object based in the HTML Element prototype
    var TomalecAceEditorPrototype = Object.create(HTMLElement.prototype);

    // Fires when an instance of the element is created
    TomalecAceEditorPrototype.createdCallback = function() {
        // Creates the shadow root
        var shadowRoot = this.createShadowRoot();

        // Shim CSS if needed
        // http://stackoverflow.com/questions/24497569/content-polyfill-for-vanillajs-templates-and-custom-elements
        if (Platform.ShadowCSS) {
          var style = template.querySelector('style');

          var cssText = Platform.ShadowCSS.shimCssText(
              style.textContent, 'juicy-ace-editor');
          Platform.ShadowCSS.addCssToDocument(cssText);
        }
        // Adds a template clone into shadow root
        var clone = thatDoc.importNode(template, true);
        shadowRoot.appendChild(clone);
    };

    // Fires when an instance was inserted into the document
    TomalecAceEditorPrototype.attachedCallback = function() {

        var text = this.childNodes[0];
        var trimed_text = text.data.trim();
        var container = document.createElement("div");
            container.id = "juicy-ace-editor-container";
        // shadowRoot.appendChild(container);
        // Workaround as CSS styles are added to main document, and does not cross Shadow DOM boundry
            // this.appendChild(container);
            this.insertBefore(container, this.firstChild);
            text && container.appendChild(text);

        var editor = this.editor || ace.edit(container);
            editor.$blockScrolling = Infinity;
            editor.setValue(trimed_text, 1);
        // initial attributes
            editor.setTheme( this.getAttribute("theme") || "ace/theme/chrome");
            editor.setFontSize( this.getAttribute("fontsize") || "15px" );
            editor.setOptions({maxLines:Infinity});
            editor.setOption("highlightActiveLine", false);
            editor.setShowPrintMargin(false);
            editor.renderer.setShowGutter(false);
            editor.renderer.setPadding(20);
            editor.renderer.setScrollMargin(0, 0, 0, 0);
            editor.renderer.$cursorLayer.element.style.opacity=0
            editor.setReadOnly(true);
            editor.getSession().setUseWrapMode(true);
        var session = editor.getSession();
            session.setMode( this.getAttribute("mode") );
            session.setUseSoftTabs( this.getAttribute("softtabs") );
            session.on('changeScrollTop', function(scroll) { });
            session.on('changeScrollLeft', function(scroll) { });
        this.editor = editor;
        // Observe input textNode changes
        // Could be buggy as editor was also added to Light DOM;
            var observer = new MutationObserver(function(mutations) {
              mutations.forEach(function(mutation) {
                console.log("observation", mutation.type, arguments, mutations, editor, text);
                if(mutation.type == "characterData"){
                    editor.setValue(text.data);
                }
              });
            });
            text && observer.observe(text, { characterData: true });
        // container.appendChild(text);
        this._attached = true;
    };

    // Fires when an instance was removed from the document
    TomalecAceEditorPrototype.detachedCallback = function() {
        this._attached = false;
    };

    // Fires when an attribute was added, removed, or updated
    TomalecAceEditorPrototype.attributeChangedCallback = function(attr, oldVal, newVal) {
        if(!this._attached){
            return false;
        }
        switch(attr){
            case "theme":
                this.editor.setTheme( newVal );
                break;
            case "mode":
                this.editor.getSession().setMode( newVal );
                break;
            case "fontsize":
                this.editor.setFontSize( newVal );
                break;
            case "softtabs":
                this.editor.getSession().setUseSoftTabs( newVal );
                break;
            case "readonly":
                this.editor.setReadOnly( newVal );
                break;

        }
    };

    document.registerElement('juicy-ace-editor', {
        prototype: TomalecAceEditorPrototype
    });
}(window, document));

function invoke_leanjs(code) {
    if (typeof myModule !== 'undefined') {
        myModule.editor_main.setValue(code, 1)
        myModule.process_main_buffer();
    } else {
        var encodedText = btoa(unescape(encodeURIComponent(code)));
        var url = "https://leanprover.github.io/live/?code=" + encodedText; window.open(url);
    }
}
</script>