footer.html

<hr />

<script type="text/javascript">

  function load_coq_snippets() {
    for (i = 0; i < coqdoc_ids.length; ++i) {
      document.getElementById(coqdoc_ids[i]).nextSibling.CodeMirror.setValue(
        localStorage.getItem('coq-snippet-' + coqdoc_ids[i]));
    }
  }

  function save_coq_snippets() {
    for (i = 0; i < coqdoc_ids.length; ++i) {
      localStorage.setItem('coq-snippet-' + coqdoc_ids[i], document.getElementById(coqdoc_ids[i]).nextSibling.CodeMirror.getValue());
    }
    alert("Coq snippets saved.");
  }

  function download_coq_snippets() {
    var chunks = []
    for (i = 0; i < coqdoc_ids.length; ++i) {
      chunks.push(document.getElementById(coqdoc_ids[i]).nextSibling.CodeMirror.getValue())
    }
    var data = new Blob(chunks, { type: "text/plain;charset=utf-8" });
    saveAs(data, 'source.v');
  }



  alignWithTop = true;
  current = 0;
  slides = [];
  function select_current() {
    for (var i = 0; i < slides.length; i++) {
      var s = document.getElementById('slideno' + i);
      if (i == current) {
        s.setAttribute('class', 'slideno selected');
      } else {
        s.setAttribute('class', 'slideno');
      }
    }
  }

  function mk_tooltip(label, text) {
    var t = document.createElement("div");
    t.setAttribute('class', 'slide-tooltip');
    t.innerHTML = label;

    var s = document.createElement("span");
    s.setAttribute('class', 'slide-tooltiptext slide-tooltip-left');
    s.innerHTML = text;

    t.appendChild(s);
    return t;
  }

  function find_hx(e) {
    for (var i = 0; i < e.children.length; i++) {
      var x = e.children[i];
      if (x.tagName == "H1" ||
        x.tagName == "H2" ||
        x.tagName == "H3" ||
        x.tagName == "H4") return x.textContent;
    }
    return null;
  }

  function init_slides() {
    var toolbar = document.getElementById('document');
    if (toolbar) {
      var tools = document.createElement("div");
      var tprev = document.createElement("div");
      var tnext = document.createElement("div");
      tools.setAttribute('id', 'tools');
      tprev.setAttribute('id', 'prev');
      tprev.setAttribute('onclick', 'prev_slide();');
      tnext.setAttribute('id', 'next');
      tnext.setAttribute('onclick', 'next_slide();');
      toolbar.prepend(tools);
      tools.appendChild(tprev);
      tools.appendChild(tnext);

      slides = document.getElementsByClassName('slide');
      for (var i = 0; i < slides.length; i++) {
        var s = document.createElement("div");
        s.setAttribute('id', 'slideno' + i);
        s.setAttribute('class', 'slideno');
        s.setAttribute('onclick', 'goto_slide(' + i + ');');
        var title = find_hx(slides[i]);
        if (title == null) {
          title = "goto slide " + i;
        }
        var t = mk_tooltip(i, title);
        s.appendChild(t)
        tools.appendChild(s);
      }
      select_current();
    } else {
      //retry later
      setTimeout(init_slides, 100);
    }
  }
  function on_screen(rect) {
    return (
      rect.top >= 0 &&
      rect.top <= (window.innerHeight || document.documentElement.clientHeight)
    );
  }
  function update_scrolled() {
    for (var i = slides.length - 1; i >= 0; i--) {
      var rect = slides[i].getBoundingClientRect();
      if (on_screen(rect)) {
        current = i;
        select_current();
      }
    }
  }
  function goto_slide(n) {
    current = n;
    var element = slides[current];
    console.log(element);
    element.scrollIntoView(alignWithTop);
    select_current();
  }
  function next_slide() {
    current++;
    if (current >= slides.length) { current = slides.length - 1; }
    var element = slides[current];
    console.log(element);
    element.scrollIntoView(alignWithTop);
    select_current();
  }
  function prev_slide() {
    current--;
    if (current < 0) { current = 0; }
    var element = slides[current];
    element.scrollIntoView(alignWithTop);
    select_current();
  }

  window.onload = init_slides;
  window.onbeforeunload = save_coq_snippets;
  window.onscroll = update_scrolled;
</script>

</div> <!-- /#document     -->
</div> <!-- /#code-wrapper -->
</div> <!-- /#ide-wrapper  -->

<script src="./jscoq/ui-js/jscoq-loader.js" type="text/javascript"></script>
<script type="text/javascript">
  var coq;

  loadJsCoq('./jscoq/')
    .then(loadJs("./jscoq/node_modules/codemirror/addon/runmode/runmode"))
    .then(loadJs("./jscoq/node_modules/codemirror/addon/runmode/colorize"))
    .then(function () {
      var coqInline = document.getElementsByClassName("inline-coq");
      CodeMirror.colorize(coqInline);
    })
    .then(function () {
      coq = new CoqManager(coqdoc_ids,
        { base_path: './jscoq/',
          init_pkgs: ['init'],
          all_pkgs: ['init','math-comp']
         }
      );
    });
</script>
</body>

</html>