api/src/docs/js/index.html

<!--~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
  ~ Copyright (c) 2018 Contributors to the Eclipse Foundation
  ~
  ~ See the NOTICE file(s) distributed with this work for additional
  ~ information regarding copyright ownership.
  ~
  ~ Licensed under the Apache License, Version 2.0 (the "License");
  ~ You may not use this file except in compliance with the License.
  ~ You may obtain a copy of the License at
  ~
  ~     http://www.apache.org/licenses/LICENSE-2.0
  ~
  ~ Unless required by applicable law or agreed to in writing, software
  ~ distributed under the License is distributed on an "AS IS" BASIS,
  ~ WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
  ~ See the License for the specific language governing permissions and
  ~ limitations under the License.
  ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~-->

<!-- Used for seeing all the diagrams in the browser. -->

<html>
<head>
    <script type="text/javascript" src="../../../node_modules/svg.js/dist/svg.js"></script>
    <script type="text/javascript" src="svg-marbles.js"></script>
    <script type="text/javascript" src="mp-rs-ops-marbles.js"></script>
    <style>
        @font-face {
            font-family: "Source Code Pro";
            src: url(SourceCodePro-Regular.ttf);
        }
        #loadfont {
            position: absolute;
            left: -500px;
            width: 500px;
            font-family: "Source Code Pro";
        }
        .diagram { margin: 50px; }
        h3 {
            padding-top: 20px;
        }
    </style>
</head>
<body>
<div id="marbles"></div>
<div id="loadfont">This div exists so that the browser will load the Source Code Pro font before we render the marbles,
    ensuring it gets the leading and sizes right.</div>
<script type="text/javascript">
    window.setTimeout(function() {
        createMarbles().draw(window.document.getElementById("marbles"), window.document);
        if (window.location.hash) {
            // And if we were on a hash, navigate to it now that it's there.
            window.location.href = window.location.hash;
        }
    }, 100);
</script>
</body>
</html>