user_guide:tutorials:latest:ilp_and_hilbertbases

Differences

This shows you the differences between two versions of the page.


user_guide:tutorials:latest:ilp_and_hilbertbases [2023/11/06 10:57] (current) – created - external edit 127.0.0.1
Line 1: Line 1:
 +===== ILP and Hilbert bases =====
 +
 +==== A first example ====
 +
 +First we will construct a new rational polytope:
 +
 +<code perl>
 +> $p=new Polytope<Rational>;
 +> $p->POINTS=<<".";
 +> 1 0 0 0
 +> 1 1 0 0
 +> 1 0 1 0
 +> 1 1 1 0
 +> 1 0 0 1
 +> 1 1 0 1
 +> 1 0 1 1
 +> 1 1 1 1
 +> .
 +</code>
 +Note that points in ''%%polymake%%'' are always given in homogenous coordinates. I.e., the point (a,b,c) in R<sup>3</sup> is represented as ''%%1 a b c%%'' in ''%%polymake%%''.
 +
 +Now we can examine some properties of ''%%$p%%''. For instance we can determine the number of facets or whether ''%%$p%%'' is simple:
 +
 +<code perl>
 +> print $p->N_FACETS;
 +6
 +> print $p->SIMPLE;
 +true
 +</code>
 +As you might already have noticed, our polytope is just a 3-dimensional cube. So there would have been an easier way to create it using the client ''%%cube%%'':
 +
 +<code perl>
 +> $c = cube(3,0);
 +</code>
 +(You can check out the details of any function in the [[documentation:latest:polytope|documentation]].)
 +
 +And we can also verify that the two polytopes are actually equal:
 +
 +<code perl>
 +> print equal_polyhedra($p,$c);
 +true
 +</code>
 +==== Another example ====
 +
 +Now let us proceed with a somewhat more interesting example: The convex hull of 20 randomly chosen points on the 2-dimensional sphere.
 +
 +<code perl>
 +> $rs = rand_sphere(3,20);
 +</code>
 +''%%polymake%%'' can of course visualise this polytope:
 +
 +<code perl>
 +> $rs->VISUAL;
 +</code>
 +<HTML>
 +<!--
 +polymake for knusper
 +Thu Mar  3 00:34:23 2022
 +rs
 +-->
 +
 +
 +<html>
 +   <head>
 +      <meta charset=utf-8>
 +      <title>rs</title>
 +      <style>
 +/*
 +// COMMON_CODE_BLOCK_BEGIN
 +*/
 +         html {overflow: scroll;}
 +         strong{font-size: 18px;}
 +         canvas { z-index: 8; }
 +         input[type='radio'] {margin-left:0;}
 +         input[type='checkbox'] {margin-right:7px; margin-left: 0px; padding-left:0px;}
 +         .group{padding-bottom: 15px;}
 +         .settings * {z-index: 11; }
 +         .settings{z-index: 10; font-family: Arial, Helvetica, sans-serif; margin-left: 30px; visibility: hidden; width: 14em; height: 96%; border: solid 1px silver; padding: 2px; overflow-y: scroll; box-sizing: border-box; background-color: white; position: absolute;}
 +         .indented{margin-left: 20px; margin-top: 10px; padding-bottom: 0px;} 
 +         .shownObjectsList{overflow: auto; max-width: 150px; max-height: 150px;}
 +         .showSettingsButton{visibility: visible; z-index: 12; position: absolute }
 +         .hideSettingsButton{visibility: hidden; z-index: 12; position: absolute; opacity: 0.5}
 +         button{margin-left: 0; margin-top: 10px}
 +         img{cursor: pointer;}
 +         .suboption{padding-top: 15px;}
 +         #model8219031067 { width: 100%; height: 100%; }
 +         .threejs_container { width: 100%; height: 75vh;}
 +         .settings{max-height: 74vh} 
 +         input[type=range] {
 +           -webkit-appearance: none;
 +           padding:0; 
 +           width:90%; 
 +           margin-left: auto;
 +           margin-right: auto;
 +           margin-top: 15px;
 +           margin-bottom: 15px;
 +           display: block;
 +         }
 +         input[type=range]:focus {
 +           outline: none;
 +         }
 +         input[type=range]::-webkit-slider-runnable-track {
 +           height: 4px;
 +           cursor: pointer;
 +           animate: 0.2s;
 +           box-shadow: 0px 0px 0px #000000;
 +           background: #E3E3E3;
 +           border-radius: 0px;
 +           border: 0px solid #000000;
 +         }
 +         input[type=range]::-webkit-slider-thumb {
 +           box-shadow: 1px 1px 2px #B8B8B8;
 +           border: 1px solid #ABABAB;
 +           height: 13px;
 +           width: 25px;
 +           border-radius: 20px;
 +           background: #E0E0E0;
 +           cursor: pointer;
 +           -webkit-appearance: none;
 +           margin-top: -5px;
 +         }
 +         input[type=range]:focus::-webkit-slider-runnable-track {
 +           background: #E3E3E3;
 +         }
 +         input[type=range]::-moz-range-track {
 +           height: 4px;
 +           cursor: pointer;
 +           animate: 0.2s;
 +           box-shadow: 0px 0px 0px #000000;
 +           background: #E3E3E3;
 +           border-radius: 0px;
 +           border: 0px solid #000000;
 +         }
 +         input[type=range]::-moz-range-thumb {
 +           box-shadow: 1px 1px 2px #B8B8B8;
 +           border: 1px solid #ABABAB;
 +           height: 13px;
 +           width: 25px;
 +           border-radius: 20px;
 +           background: #E0E0E0;
 +           cursor: pointer;
 +         }
 +         input[type=range]::-ms-track {
 +           height: 4px;
 +           cursor: pointer;
 +           animate: 0.2s;
 +           background: transparent;
 +           border-color: transparent;
 +           color: transparent;
 +         }
 +         input[type=range]::-ms-fill-lower {
 +           background: #E3E3E3;
 +           border: 0px solid #000000;
 +           border-radius: 0px;
 +           box-shadow: 0px 0px 0px #000000;
 +         }
 +         input[type=range]::-ms-fill-upper {
 +           background: #E3E3E3;
 +           border: 0px solid #000000;
 +           border-radius: 0px;
 +           box-shadow: 0px 0px 0px #000000;
 +         }
 +         input[type=range]::-ms-thumb {
 +           box-shadow: 1px 1px 2px #B8B8B8;
 +           border: 1px solid #ABABAB;
 +           height: 13px;
 +           width: 25px;
 +           border-radius: 20px;
 +           background: #E0E0E0;
 +           cursor: pointer;
 +         }
 +         input[type=range]:focus::-ms-fill-lower {
 +           background: #E3E3E3;
 +         }
 +         input[type=range]:focus::-ms-fill-upper {
 +           background: #E3E3E3;
 +         }
 +/*
 +// COMMON_CODE_BLOCK_END
 +*/
 + </style>
 +   </head>
 +<body>
 +   <div class='threejs_container'>
 + <div id='settings_0' class='settings'>
 + <div class=group id='transparency_0' class='transparency'>
 + <strong>Transparency</strong>
 + <input id='transparencyRange_0' type='range' min=0 max=1 step=0.01 value=0>
 +            <div class=indented><input id='depthWriteCheckbox_0' type='checkbox'>depthWrite</div>
 + </div>
 +
 + <div class=group id='rotation_0'>
 + <strong>Rotation</strong>
 + <div class=indented>
 + <div><input type='checkbox' id='changeRotationX_0'> x-axis</div>
 + <div><input type='checkbox' id='changeRotationY_0'> y-axis</div>
 + <div><input type='checkbox' id='changeRotationZ_0'> z-axis</div>
 + <button id='resetButton_0'>Reset</button>
 + </div>
 +
 + <div class=suboption>Rotation speed</div>
 + <input id='rotationSpeedRange_0' type='range' min=0 max=5 step=0.01 value=2>
 + </div>
 +
 +
 + <div class=group id='display_0'>
 + <strong>Display</strong>
 + <div class=indented>
 + <div id='shownObjectTypesList_0' class='shownObjectsList'></div>
 + </div>
 + <div class=suboption>Objects</div>
 + <div class=indented>
 +    <div id='shownObjectsList_0' class='shownObjectsList'></div>
 + </div>
 + </div>
 +         
 +         <div class=group id='camera_0'>
 +            <strong>Camera</strong>
 +            <div class=indented>
 +               <form>
 +                  <select id="cameraType_0">
 +                     <option value='perspective' selected> Perspective<br></option>
 +                     <option value='orthographic' > Orthographic<br></option>
 +                  </select>
 +               </form>
 +            </div>
 +         </div>
 +
 + <div class=group id='svg_0'>
 + <strong>SVG</strong>
 + <div class=indented>
 + <form>
 + <input type="radio" name='screenshotMode' value='download' id='download_0' checked> Download<br>
 + <input type="radio" name='screenshotMode' value='tab' id='tab_0' > New tab<br>
 + </form>
 + <button id='takeScreenshot_0'>Screenshot</button>
 + </div>
 + </div>
 +
 + </div> <!-- end of settings -->
 + <img id='hideSettingsButton_0' class='hideSettingsButton' src='/kernelspecs/r118/polymake/close.svg' width=20px">
 + <img id='showSettingsButton_0' class='showSettingsButton' src='/kernelspecs/r118/polymake/menu.svg' width=20px">
 +<div id="model8219031067"></div>
 +</div>
 +   <script>
 +    requirejs.config({
 +      paths: {
 +        three: '/kernelspecs/r118/polymake/three',
 +        TrackballControls: '/kernelspecs/r118/polymake/TrackballControls',
 +        OrbitControls: '/kernelspecs/r118/polymake/OrbitControls',
 +        Projector: '/kernelspecs/r118/polymake/Projector',
 +        SVGRenderer: '/kernelspecs/r118/polymake/SVGRenderer',
 +        WEBGL: '/kernelspecs/r118/polymake/WebGL',
 +      },
 +      shim: {
 +        'three': { exports: 'THREE'},
 +        'SVGRenderer': { deps: [ 'three' ], exports: 'THREE.SVGRenderer' },
 +        'WEBGL': { deps: [ 'three' ], exports: 'THREE.WEBGL' },
 +        'Projector': { deps: [ 'three' ], exports: 'THREE.Projector' },
 +        'TrackballControls': { deps: [ 'three' ], exports: 'THREE.TrackballControls' },
 +        'OrbitControls': { deps: [ 'three' ], exports: 'THREE.OrbitControls' },
 +      }
 +    });
 +    
 +    require(['three'],function(THREE){
 +        window.THREE = THREE;
 +      require(['TrackballControls', 'OrbitControls', 'Projector', 'SVGRenderer', 'WEBGL'],
 +               function(TrackballControls, OrbitControls, Projector, SVGRenderer, WEBGL) {
 +    THREE.TrackballControls = TrackballControls;
 +    THREE.OrbitControls = OrbitControls;
 +    THREE.Projector = Projector;
 +    THREE.SVGRenderer = SVGRenderer;
 +    THREE.WEBGL = WEBGL;
 +
 +// COMMON_CODE_BLOCK_BEGIN
 +
 +const intervalLength = 25; // for automatic animations
 +const explodableModel = false; 
 +const modelContains = { points: false, pointlabels: false, lines: false, edgelabels: false, faces: false, arrowheads: false };
 +const foldables = [];
 +
 +var three = document.getElementById("model8219031067");
 +var scene = new THREE.Scene();
 +var renderer = new THREE.WebGLRenderer( { antialias: true } );
 +var svgRenderer = new THREE.SVGRenderer( { antialias: true } );
 +renderer.setPixelRatio( window.devicePixelRatio );
 +renderer.setClearColor(0xFFFFFF, 1);
 +svgRenderer.setClearColor(0xFFFFFF, 1);
 +three.appendChild(renderer.domElement);
 +
 +var frustumSize = 4;
 +var cameras = [new THREE.PerspectiveCamera(75, 1, 0.1, 1000), new THREE.OrthographicCamera()];
 +cameras.forEach(function(cam) {
 +    cam.position.set(0, 0, 5);
 +    cam.lookAt(0, 0, 0);  
 +    cam.up.set(0, 1, 0);         
 +});
 +var controls = [new THREE.TrackballControls(cameras[0], three), new THREE.OrbitControls(cameras[1], three)];
 +var camera, control;
 +
 +controls[0].zoomSpeed = 0.2;
 +controls[0].rotateSpeed = 4;
 +
 +
 +// class to allow move points together with labels and spheres
 +var PMPoint = function (x,y,z) {
 +   this.vector = new THREE.Vector3(x,y,z);
 +   this.sprite = null;
 +   this.sphere = null;
 +}
 +PMPoint.prototype.addLabel = function(labelsprite) {
 +   this.sprite = labelsprite;
 +   this.sprite.position.copy(this.vector);
 +}
 +PMPoint.prototype.addSphere = function(spheremesh) {
 +   this.sphere = spheremesh;
 +   this.sphere.position.copy(this.vector);
 +}
 +PMPoint.prototype.set = function(x,y,z) {
 +   this.vector.set(x,y,z);
 +   if (this.sprite) {
 +      this.sprite.position.copy(this.vector);
 +   }
 +   if (this.sphere) {
 +      this.sphere.position.copy(this.vector);
 +   }
 +}
 +PMPoint.prototype.radius = function() {
 +   if (this.sphere) {
 +      return this.sphere.geometry.parameters.radius;
 +   } else {
 +      return 0;
 +   }
 +};
 +// select the target node
 +var target = document.querySelector('#model8219031067');
 +
 +// create an observer instance
 +var observer = new MutationObserver(function(mutations) {
 +   mutations.forEach(function(mutation) {
 +      if (mutation.removedNodes && mutation.removedNodes.length > 0) {
 +         cancelAnimationFrame(renderId);
 +         observer.disconnect();
 +         console.log("cancelled frame "+renderId);
 +      }
 +   });
 +});
 +
 +// configuration of the observer:
 +var config = { childList: true, characterData: true }
 +
 +// pass in the target node, as well as the observer options
 +while (target) {
 +   if (target.className=="output") {
 +      observer.observe(target, config);
 +      break;
 +   }
 +   target = target.parentNode;
 +}
 +
 +// COMMON_CODE_BLOCK_END
 +
 +var obj0 = new THREE.Object3D();
 +obj0.name = "rs";
 +obj0.userData.explodable = 1;
 +obj0.userData.points = [];
 +obj0.userData.points.push(new PMPoint(-0.440503, 0.836768, 0.325232));
 +obj0.userData.points.push(new PMPoint(0.665111, 0.350117, -0.65958));
 +obj0.userData.points.push(new PMPoint(0.249757, -0.792592, 0.556255));
 +obj0.userData.points.push(new PMPoint(-0.577844, -0.815895, -0.0202731));
 +obj0.userData.points.push(new PMPoint(-0.112342, 0.811068, 0.574063));
 +obj0.userData.points.push(new PMPoint(0.541203, 0.0340188, 0.840204));
 +obj0.userData.points.push(new PMPoint(-0.456164, -0.618041, -0.640265));
 +obj0.userData.points.push(new PMPoint(-0.652696, 0.315439, 0.688829));
 +obj0.userData.points.push(new PMPoint(-0.307662, -0.881097, 0.359182));
 +obj0.userData.points.push(new PMPoint(-0.194799, 0.46658, -0.862761));
 +obj0.userData.points.push(new PMPoint(0.0373143, 0.30347, -0.95211));
 +obj0.userData.points.push(new PMPoint(0.693347, 0.333122, 0.638983));
 +obj0.userData.points.push(new PMPoint(0.662852, -0.174229, 0.728197));
 +obj0.userData.points.push(new PMPoint(-0.660007, 0.66114, 0.356769));
 +obj0.userData.points.push(new PMPoint(-0.0512853, -0.107809, 0.992848));
 +obj0.userData.points.push(new PMPoint(-0.791998, 0.511463, 0.333385));
 +obj0.userData.points.push(new PMPoint(0.737893, 0.54063, -0.40402));
 +obj0.userData.points.push(new PMPoint(0.0472492, 0.848375, 0.527283));
 +obj0.userData.points.push(new PMPoint(-0.750783, -0.0197826, 0.660253));
 +obj0.userData.points.push(new PMPoint(0.331489, -0.134575, 0.933812));
 +
 +obj0.userData.pointradii = 0.02;
 +   <!-- Vertex style -->
 +obj0.userData.pointmaterial = new THREE.MeshBasicMaterial( { color: 0xFF0000, side: THREE.DoubleSide, transparent: false } );
 +obj0.userData.pointlabels = ["0", "1", "2", "3", "4", "5", "6", "7", "8", "9", "10", "11", "12", "13", "14", "15", "16", "17", "18", "19"];
 +obj0.userData.edgeindices = [1, 2, 0, 4, 4, 5, 1, 6, 2, 6, 3, 6, 4, 7, 2, 8, 3, 8, 6, 8, 0, 9, 1, 9, 6, 9, 1, 10, 6, 10, 9, 10, 5, 11, 1, 12, 2, 12, 5, 12, 11, 12, 0, 13, 4, 13, 7, 13, 9, 13, 2, 14, 4, 14, 5, 14, 7, 14, 8, 14, 3, 15, 6, 15, 7, 15, 9, 15, 13, 15, 0, 16, 1, 16, 9, 16, 11, 16, 12, 16, 0, 17, 4, 17, 5, 17, 11, 17, 16, 17, 3, 18, 7, 18, 8, 18, 14, 18, 15, 18, 2, 19, 5, 19, 12, 19, 14, 19];
 +   <!-- Edge style -->
 +obj0.userData.edgematerial = new THREE.LineBasicMaterial( { color: 0x000000, linewidth: 1.5, transparent: false } );
 +obj0.userData.facets = [[5, 11, 17], [12, 11, 5], [12, 5, 19], [12, 19, 2], [19, 14, 2], [4, 17, 0], [14, 4, 7], [14, 18, 8], [14, 7, 18], [0, 9, 13], [13, 9, 15], [15, 9, 6], [18, 15, 3], [7, 13, 15], [18, 7, 15], [15, 6, 3], [8, 18, 3], [6, 8, 3], [4, 13, 7], [4, 0, 13], [9, 10, 6], [2, 14, 8], [6, 2, 8], [5, 4, 14], [5, 17, 4], [5, 14, 19], [9, 1, 10], [1, 6, 10], [1, 2, 6], [1, 12, 2], [0, 16, 9], [17, 16, 0], [16, 1, 9], [16, 12, 1], [17, 11, 16], [16, 11, 12]];
 +   <!-- Facet style -->
 +obj0.userData.facetmaterial = new THREE.MeshBasicMaterial( { color: 0x77EC9E, depthFunc: THREE.LessDepth, depthWrite: false, opacity: 1, polygonOffset: true, polygonOffsetFactor: 1, polygonOffsetUnits: 0.5, side: THREE.DoubleSide, transparent: true } );
 +init_object(obj0);
 +scene.add(obj0);
 +
 +// COMMON_CODE_BLOCK_BEGIN
 +function textSpriteMaterial(message, parameters) {
 +    if ( parameters === undefined ) parameters = {};
 +    var fontface = "Helvetica";
 +    var fontsize = parameters.hasOwnProperty("fontsize") ? parameters["fontsize"] : 15;
 +    fontsize = fontsize*10;
 +    var lines = message.split('\\n');
 +    var size = 512;
 +    for(var i = 0; i<lines.length; i++){
 +        var tmp = lines[i].length;
 +        while(tmp*fontsize > size){
 +           fontsize--;
 +        }
 +    }
 +    
 +    var canvas = document.createElement('canvas');
 +    canvas.width = size;
 +    canvas.height = size;
 +    var context = canvas.getContext('2d');
 +    context.fillStyle = "rgba(255, 255, 255, 0)";
 +    context.fill();
 +    context.font = fontsize + "px " + fontface;
 +    
 +    // text color
 +    context.fillStyle = "rgba(0, 0, 0, 1.0)";
 +     for(var i = 0; i<lines.length; i++){
 +        context.fillText(lines[i], size/2, size/2+i*fontsize);
 +     }
 +    
 +    // canvas contents will be used for a texture
 +    var texture = new THREE.Texture(canvas);
 +    texture.needsUpdate = true;
 +    
 +    var spriteMaterial = new THREE.SpriteMaterial({map: texture, depthTest: true, depthWrite: false, polygonOffset: true, polygonOffsetFactor: -1, polygonOffsetUnits: 1 });
 +    return spriteMaterial;
 +}
 +
 +
 +// ---------------------- INITIALIZING OBJECTS--------------------------------------
 +// ---------------------------------------------------------------------------------
 +
 +function init_object(obj) {
 +    if (obj.userData.hasOwnProperty("pointmaterial")) {
 +        init_points(obj);
 +        modelContains.points = true;
 +    }
 +    if (obj.userData.hasOwnProperty("pointlabels")) {
 +        init_pointlabels(obj);
 +        modelContains.pointlabels = true;
 +    }
 +    if (obj.userData.hasOwnProperty("edgematerial")) {
 +        init_lines(obj);
 +        modelContains.lines = true;
 +    }
 +    if (obj.userData.hasOwnProperty("edgelabels")) {
 +        init_edgelabels(obj);
 +        modelContains.edgelabels = true;
 +    }
 +    if (obj.userData.hasOwnProperty("arrowstyle")) {
 +        init_arrowheads(obj);
 +        modelContains.arrowheads = true;
 +    }
 +    if (obj.userData.hasOwnProperty("facetmaterial")) {
 +        init_faces(obj);
 +        modelContains.faces = true;
 +    }
 +}
 +
 +function init_points(obj) {
 +    var pointgroup = new THREE.Group();
 +    pointgroup.name = "points";
 +    var points = obj.userData.points;
 +    var radii = obj.userData.pointradii;
 +    var materials = obj.userData.pointmaterial;
 +    var geometry,material;
 +    if (!Array.isArray(radii)) {
 +        geometry = new THREE.SphereBufferGeometry(radii);  
 +    }
 +    if (!Array.isArray(materials)) {
 +        material = materials;
 +    }
 +    for (var i=0; i<points.length; i++) {
 +        var point = points[i];
 +        if (Array.isArray(radii)) {
 +            if (radii[i] == 0) {
 +                continue;
 +            }
 +            geometry = new THREE.SphereBufferGeometry(radii[i]);  
 +        } 
 +        if (Array.isArray(materials)) {
 +            material = materials[i];     
 +        } 
 +        var sphere = new THREE.Mesh(geometry, material);
 +        point.addSphere(sphere);
 +        pointgroup.add(sphere);
 +    }
 +    obj.add(pointgroup);
 +}
 +
 +function init_pointlabels(obj) {
 +    var points = obj.userData.points;
 +    var labels = obj.userData.pointlabels;
 +    var pointlabels = new THREE.Group();
 +    pointlabels.name = "pointlabels";
 +    if (Array.isArray(labels)) {
 +        for (var i=0; i<points.length; i++) {
 +            var point = points[i];
 +            var spriteMaterial = textSpriteMaterial( labels[i] );
 +         var sprite = new THREE.Sprite(spriteMaterial);
 +            point.addLabel(sprite);
 +            pointlabels.add(sprite);
 +        }
 +    } else {
 +        var spriteMaterial = textSpriteMaterial( labels );
 +        for (var i=0; i<points.length; i++) {
 +            var point = points[i];
 +         var sprite = new THREE.Sprite(spriteMaterial);
 +            point.addLabel(sprite);
 +            pointlabels.add(sprite);
 +        }
 +    }
 +    obj.add(pointlabels);
 +}
 +
 +function init_lines(obj) {
 +    var edgeindices = obj.userData.edgeindices;
 +    var points = obj.userData.points;
 +    var materials = obj.userData.edgematerial;
 +    var geometry = new THREE.BufferGeometry();
 +    var bufarr = new Float32Array( obj.userData.edgeindices.length * 3 );
 +    var bufattr = new THREE.Float32BufferAttribute( bufarr, 3 );
 +    var geometry = new THREE.BufferGeometry();
 +    geometry.setAttribute('position', bufattr);
 +    if (Array.isArray(materials)) {     
 +        for (var i=0; i<materials.length; i++) {
 +            geometry.addGroup(2*i,2,i);
 +        }
 +    }
 +    var lines = new THREE.LineSegments(geometry, materials);
 +    lines.name = "lines";
 +    obj.add(lines);
 +    updateEdgesPosition(obj);
 +}
 +
 +function init_edgelabels(obj) {
 +    var points = obj.userData.points;
 +    var edgeindices = obj.userData.edgeindices;
 +    var labels = obj.userData.edgelabels;
 +    var edgelabels = new THREE.Group();
 +    edgelabels.name = "edgelabels";
 +    if (Array.isArray(labels)) {
 +        for (var i=0; i<edgeindices.length/2; i++) {
 +            var spriteMaterial = textSpriteMaterial( labels[i] );
 +            var sprite = new THREE.Sprite(spriteMaterial);
 +            sprite.position.copy(new THREE.Vector3().addVectors(points[edgeindices[2*i]].vector,points[edgeindices[2*i+1]].vector).multiplyScalar(0.5));
 +            edgelabels.add(sprite);
 +        }
 +    } else {
 +        var spriteMaterial = textSpriteMaterial( labels );
 +        for (var i=0; i<edgeindices.length/2; i++) {
 +            var sprite = new THREE.Sprite(spriteMaterial);
 +            sprite.position.copy(new THREE.Vector3().addVectors(points[edgeindices[2*i]].vector,points[edgeindices[2*i+1]].vector).multiplyScalar(0.5));
 +            edgelabels.add(sprite);
 +        }
 +    }
 +    obj.add(edgelabels);
 +}
 +
 +function init_arrowheads(obj) {
 +    var arrowheads = new THREE.Group();
 +    arrowheads.name = "arrowheads";
 +    var arrowstyle = obj.userData.arrowstyle;
 +    var edgeindices = obj.userData.edgeindices;
 +    var edgematerials = obj.userData.edgematerial;
 +    var points = obj.userData.points;
 +    var material;
 +    if (!Array.isArray(edgematerials)) {
 +        material = new THREE.MeshBasicMaterial( {color: edgematerials.color} );
 +    }
 +
 +    for (var i=0; i<edgeindices.length; i=i+2) {
 +        var start = points[edgeindices[i]];
 +        var end = points[edgeindices[i+1]];
 +        var dist = start.vector.distanceTo( end.vector ) - start.radius() - end.radius();
 +        if (dist <= 0) {
 +            continue;
 +        }
 +        var dir = new THREE.Vector3().subVectors(end.vector,start.vector);
 +        dir.normalize();
 +        var axis = new THREE.Vector3().set(dir.z,0,-dir.x);
 +        axis.normalize();
 +        var radians = Math.acos( dir.y );
 +        var radius = dist/25;
 +        var height = dist/5;
 +        var geometry = new THREE.ConeBufferGeometry(radius,height);
 +        var position = new THREE.Vector3().addVectors(start.vector,dir.clone().multiplyScalar(start.radius()+dist-height/2));
 +        if (Array.isArray(edgematerials)) {
 +            material = new THREE.MeshBasicMaterial( {color: edgematerials[i].color} );
 +        }
 +        var cone = new THREE.Mesh( geometry, material );
 +        cone.quaternion.setFromAxisAngle(axis,radians);;
 +        cone.position.copy(position);;
 +        arrowheads.add(cone);
 +    }
 +    obj.add(arrowheads);
 +}
 +
 +function init_faces(obj) {
 +    var points = obj.userData.points;
 +    var facets = obj.userData.facets;
 +    obj.userData.triangleindices = [];
 +    for (var i=0; i<facets.length; i++) {
 +        facet = facets[i];
 +        for (var t=0; t<facet.length-2; t++) {
 +            obj.userData.triangleindices.push(facet[0],facet[t+1],facet[t+2]);  
 +        }
 +    }
 +    var bufarr = new Float32Array( obj.userData.triangleindices.length * 3 );
 +    var bufattr = new THREE.Float32BufferAttribute(bufarr,3);
 +    
 +    var materials = obj.userData.facetmaterial;
 +    var geometry = new THREE.BufferGeometry();
 +    var frontmaterials = [];
 +    var backmaterials = [];
 +    geometry.setAttribute('position',bufattr);
 +    if (Array.isArray(materials)) {
 +        var tricount = 0;
 +        var facet;
 +        for (var i=0; i<facets.length; i++) {
 +            facet = facets[i];
 +            geometry.addGroup(tricount,(facet.length-2)*3,i);
 +            tricount += (facet.length-2)*3;
 +        }
 +        for (var j=0; j<materials.length; j++) {
 +            var fmat = materials[j].clone()
 +            fmat.side = THREE.FrontSide;
 +            frontmaterials.push(fmat);
 +            var bmat = materials[j].clone()
 +            bmat.side = THREE.BackSide;
 +            backmaterials.push(bmat);
 +            obj.userData.facetmaterial = frontmaterials.concat(backmaterials);
 +        }
 +    } else if (materials instanceof THREE.Material) {
 +        frontmaterials = materials.clone()
 +        frontmaterials.side = THREE.FrontSide;
 +        backmaterials = materials.clone()
 +        backmaterials.side = THREE.BackSide;
 +        obj.userData.facetmaterial = [frontmaterials, backmaterials];
 +    }
 +    // duplicating the object with front and back should avoid transparency issues
 +    var backmesh = new THREE.Mesh(geometry, backmaterials);
 +    // meshname is used to show/hide objects
 +    backmesh.name = "backfaces";
 +    obj.add(backmesh);
 +    var frontmesh = new THREE.Mesh(geometry, frontmaterials);
 +    frontmesh.name = "frontfaces";
 +    obj.add(frontmesh);
 +    updateFacesPosition(obj);
 +}
 +// //INITIALIZING
 +
 +
 +function updateFacesPosition(obj) {
 +    var points = obj.userData.points;
 +    var indices = obj.userData.triangleindices;
 +    var faces = obj.getObjectByName("frontfaces");
 +    var ba = faces.geometry.getAttribute("position");
 +    for (var i=0; i<indices.length; i++) {
 +        ba.setXYZ(i, points[indices[i]].vector.x, points[indices[i]].vector.y ,points[indices[i]].vector.z); 
 +    }
 +    faces.geometry.attributes.position.needsUpdate = true;
 +    
 +}
 +
 +function updateEdgesPosition(obj) {
 +    var points = obj.userData.points;
 +    var indices = obj.userData.edgeindices;
 +    var lines = obj.getObjectByName("lines");
 +    var ba = lines.geometry.getAttribute("position"); 
 +    for (var i=0; i<indices.length; i++) {
 +        ba.setXYZ(i, points[indices[i]].vector.x, points[indices[i]].vector.y ,points[indices[i]].vector.z); 
 +    }
 +    lines.geometry.attributes.position.needsUpdate = true;
 +}
 +
 +function onWindowResize() {
 +    renderer.setSize( three.clientWidth, three.clientHeight );
 +    svgRenderer.setSize( three.clientWidth, three.clientHeight );
 +    updateCamera();
 +}
 +
 +function updateCamera() {
 +    var width = three.clientWidth;
 +    var height = three.clientHeight;
 +    var aspect = width / height;
 +    if (camera.type == "OrthographicCamera") {
 +        camera.left = frustumSize * aspect / - 2;
 +        camera.right = frustumSize * aspect / 2;
 +        camera.top = frustumSize / 2;
 +        camera.bottom = - frustumSize / 2;
 +    } else if (camera.type == "PerspectiveCamera") {
 +        camera.aspect = aspect;
 +    }
 +    camera.updateProjectionMatrix();
 +}
 +
 +function changeCamera(event) {
 +    var selindex = event.currentTarget.selectedIndex;
 +    camera = cameras[selindex];
 +    control = controls[selindex];
 +    control.enabled = true; 
 +    for (var i=0; i<controls.length; i++) {
 +        if (i!=selindex) {
 +            controls[i].enabled = false;
 +        }
 +    }
 +    updateCamera();
 +}
 +
 +var camtypenode = document.getElementById('cameraType_0');
 +camtypenode.onchange = changeCamera;
 +camtypenode.dispatchEvent(new Event('change'));
 +
 +onWindowResize();
 +window.addEventListener('resize', onWindowResize);
 +
 +
 +var xRotationEnabled = false;
 +var yRotationEnabled = false;
 +var zRotationEnabled = false;
 +var rotationSpeedFactor = 1;
 +var settingsShown = false;
 +var labelsShown = true;
 +var intervals = [];
 +var timeouts = [];
 +var explodingSpeed = 0.05;
 +var explodeScale = 0.000001;
 +var XMLS = new XMLSerializer();
 +var svgElement;
 +var renderId;
 +
 +var render = function () {
 +
 + renderId = requestAnimationFrame(render);
 +
 +// comment in for automatic explosion
 +// explode(updateFactor());
 +
 +    var phi = 0.02 * rotationSpeedFactor;
 +
 +    if (xRotationEnabled) {
 +        scene.rotation.x += phi;
 +    }
 +    if (yRotationEnabled) {
 +        scene.rotation.y += phi;
 +    }
 +    if (zRotationEnabled) {
 +        scene.rotation.z += phi;
 +    }
 +
 +    control.update();
 +    renderer.render(scene, camera);
 +};
 +
 +if ( THREE.WEBGL.isWebGLAvailable() ) {
 + render();
 +} else {
 + var warning = WEBGL.getWebGLErrorMessage();
 + three.appendChild( warning );
 +}
 +    
 +function changeTransparency() {
 +    var opacity = 1-Number(event.currentTarget.value);
 +    for (var i=0; i<scene.children.length; i++) {
 +        child = scene.children[i];
 +        if ( child.userData.hasOwnProperty("facetmaterial") ) {
 +            if (Array.isArray(child.userData.facetmaterial)) {
 +                for (var j=0; j<child.userData.facetmaterial.length; j++) {
 +                    child.userData.facetmaterial[j].opacity = opacity;
 +                }
 +            } else {
 +                child.userData.facetmaterial.opacity = opacity;
 +            }    
 +        }
 +    }
 +}
 +
 +function toggleDepthWrite(event) {
 +    depthwrite = event.currentTarget.checked;
 +    for (var i=0; i<scene.children.length; i++) {
 +        child = scene.children[i];
 +        if ( child.userData.hasOwnProperty("facetmaterial") ) {
 +            if (Array.isArray(child.userData.facetmaterial)) {
 +                for (var j=0; j<child.userData.facetmaterial.length; j++) {
 +                    child.userData.facetmaterial[j].depthWrite = depthwrite;
 +                }
 +            } else {
 +                child.userData.facetmaterial.depthWrite = depthWrite;
 +            }    
 +        }
 +    }
 +}
 +
 +function changeRotationX(event){
 +    xRotationEnabled = event.currentTarget.checked;
 +}
 +
 +function changeRotationY(event){
 +    yRotationEnabled = event.currentTarget.checked;
 +}
 +
 +function changeRotationZ(event){
 +    zRotationEnabled = event.currentTarget.checked;
 +}
 +
 +
 +function changeRotationSpeedFactor(event){
 +    rotationSpeedFactor = Number(event.currentTarget.value);
 +}
 +
 +function resetScene(){
 +    scene.rotation.set(0,0,0);
 +    camera.position.set(0,0,5);
 +    camera.up.set(0,1,0);
 +}
 +
 +function showSettings(event){
 +    document.getElementById('settings_0').style.visibility = 'visible';
 +    document.getElementById('showSettingsButton_0').style.visibility = 'hidden';
 +    document.getElementById('hideSettingsButton_0').style.visibility = 'visible';
 +    settingsShown = true;
 +}
 +
 +function hideSettings(event){
 +    document.getElementById('settings_0').style.visibility = 'hidden';
 +    document.getElementById('showSettingsButton_0').style.visibility = 'visible';
 +    document.getElementById('hideSettingsButton_0').style.visibility = 'hidden';
 +    settingsShown = false;
 +}
 +
 +
 +
 +var pos = 150* Math.PI;
 +
 +function updateFactor() {
 +    pos++;
 +    return Math.sin(.01*pos)+1;
 +}
 +
 +// ------------------------ FOLDING ------------------------------------------------
 +// ---------------------------------------------------------------------------------
 +// rotate point p around axis defined by points p1 and p2 by given angle
 +function rotate(p, p1, p2, angle ){   
 +    angle = -angle;
 +    var x = p.x, y = p.y, z = p.z, 
 +    a = p1.x, b = p1.y, c = p1.z, 
 +    u = p2.x-p1.x, v = p2.y-p1.y, w = p2.z-p1.z;
 +    var result = [];
 +    var L = u*u + v*v + w*w;
 +    var sqrt = Math.sqrt;
 +    var cos = Math.cos;
 +    var sin = Math.sin;
 +
 +    result[0] = ((a*(v*v+w*w)-u*(b*v+c*w-u*x-v*y-w*z))*(1-cos(angle))+L*x*cos(angle)+sqrt(L)*(-c*v+b*w-w*y+v*z)*sin(angle))/L;
 +    result[1] = ((b*(u*u+w*w)-v*(a*u+c*w-u*x-v*y-w*z))*(1-cos(angle))+L*y*cos(angle)+sqrt(L)*(c*u-a*w+w*x-u*z)*sin(angle))/L;
 +    result[2] = ((c*(u*u+v*v)-w*(a*u+b*v-u*x-v*y-w*z))*(1-cos(angle))+L*z*cos(angle)+sqrt(L)*(-b*u+a*v-v*x+u*y)*sin(angle))/L;
 +
 +    return result;
 +}
 +
 +var fold = function(event){
 +    var obj = foldables[Number(event.currentTarget.name)];
 +    var foldvalue = Number(event.currentTarget.value);
 +    var scale = foldvalue - obj.userData.oldscale;
 +
 +    for (var j=0; j<obj.userData.axes.length; j++) {
 +        rotateVertices(obj, j, scale);
 +    }
 +    update(obj);
 +    obj.userData.oldscale += scale;
 +    lookAtBarycenter(obj);
 +}
 +
 +function lookAtBarycenter(obj){
 +    control.target = barycenter(obj);
 +}
 +
 +function barycenter(obj) {
 +    var center = new THREE.Vector3(0,0,0);
 +    var points = obj.userData.points;
 +    for (var i=0; i<points.length; i++){
 +        center.add(points[i].vector);
 +    }
 +    center.divideScalar(points.length);
 +    return center;
 +}
 +
 +function rotateVertices(obj, edge, scale) {
 +    var axes = obj.userData.axes;
 +    var subtrees = obj.userData.subtrees;
 +    var points = obj.userData.points;
 +    var angles = obj.userData.angles;
 +    if (edge < axes.length){
 +        for (var j=0; j<subtrees[edge].length; j++){
 +            var rotP = rotate(points[subtrees[edge][j]].vector, points[axes[edge][0]].vector,points[axes[edge][1]].vector, scale * (Math.PI - angles[edge]));
 +            points[subtrees[edge][j]].set(rotP[0],rotP[1],rotP[2]);
 +        }
 +    }
 +}
 +
 +function update(obj) {
 +   updateFacesPosition(obj);
 +   updateEdgesPosition(obj);
 +}
 +
 +if (foldables.length) {
 +    var settings = document.getElementById('settings_0');
 +    var foldDiv = document.createElement('div');
 +    foldDiv.id = 'fold_0';
 +    var title = document.createElement('strong');
 +    title.innerHTML = 'Fold';
 +    foldDiv.appendChild(title);
 +    foldDiv.className = 'group';
 +    for (var i=0; i<foldables.length; i++) {
 +        var range = document.createElement('input');
 +        range.type = 'range';
 +        range.min = 0;
 +        range.max = 1;
 +        range.value = 0;
 +        range.step = 0.001;
 +        range.name = String(i);
 +        range.oninput = fold;
 +        foldDiv.appendChild(range);
 +    }
 +    lookAtBarycenter(foldables[0]);
 +    settings.insertBefore(foldDiv,settings.childNodes[0]);
 +}
 +
 +    
 +// ---------------------- EXPLOSION ------------------------------------------------
 +// ---------------------------------------------------------------------------------
 +
 +if (explodableModel) {
 +    for (var i=0; i<scene.children.length; i++) {
 +        obj = scene.children[i];
 +        if ( obj.userData.explodable ) {
 +            computeCentroid(obj);
 +        }
 +    }
 +    document.getElementById('explodeRange_0').oninput = triggerExplode;
 +    document.getElementById('explodeCheckbox_0').onchange = triggerAutomaticExplode;
 +    document.getElementById('explodingSpeedRange_0').oninput = setExplodingSpeed;
 +    explode(0.000001);
 +}
 +
 +function computeCentroid(obj) {
 +    centroid = new THREE.Vector3();
 +    obj.userData.points.forEach(function(pmpoint) {
 +        centroid.add(pmpoint.vector);
 +    });
 +    centroid.divideScalar(obj.userData.points.length);
 +    obj.userData.centroid = centroid;
 +}
 +
 +function explode(factor) {
 +    for (var i=0; i<scene.children.length; i++) {
 +        var obj = scene.children[i];
 +        if (obj.userData.hasOwnProperty("centroid")) { 
 +            var c = obj.userData.centroid;
 +            obj.position.set(c.x*factor, c.y*factor, c.z*factor);
 +        }
 +    }
 +}
 +
 +function triggerExplode(event){
 +    explodeScale = Number(event.currentTarget.value);
 +    explode(explodeScale);
 +}
 +
 +function setExplodingSpeed(event){
 +    explodingSpeed = Number(event.currentTarget.value);
 +}
 +
 +function triggerAutomaticExplode(event){
 +    if (event.currentTarget.checked){
 +        startExploding();
 +    } else {
 +        clearIntervals();
 +    }
 +}
 +
 +function startExploding(){
 +    intervals.push(setInterval(explodingInterval, 25));
 +}
 +
 +
 +function explodingInterval(){
 +    explodeScale += explodingSpeed;
 +    if (explodeScale <= 6){ 
 +        explode(explodeScale);
 +    }
 +    else{
 +        explode(6);
 +        explodeScale = 6;
 +        clearIntervals();
 +        timeouts.push(setTimeout(startUnexploding, 3000));
 +    }
 +    document.getElementById('explodeRange_0').value = explodeScale;
 +}
 +
 +
 +function startUnexploding(){
 +    intervals.push(setInterval(unexplodingInterval, 25));
 +}
 +
 +function unexplodingInterval(){
 +    explodeScale -= explodingSpeed;
 +    if (explodeScale >= 0){
 +        explode(explodeScale);
 +    }
 +    else {
 +        explode(0);
 +        explodeScale = 0;
 +        clearIntervals();
 +        timeouts.push(setTimeout(startExploding, 3000));
 +    }
 +    document.getElementById('explodeRange_0').value = explodeScale;
 +}
 +
 +function clearIntervals(){
 +    intervals.forEach(function(interval){
 +        clearInterval(interval);
 +    });
 +    intervals = [];
 +    timeouts.forEach(function(timeout){
 +        clearTimeout(timeout);
 +    });
 +    timeouts = [];
 +}
 +
 +// ---------------------- DISPLAY --------------------------------------------------
 +// ---------------------------------------------------------------------------------
 +
 +const objectTypeInnerHTMLs = { points: "Points", pointlabels: "Point labels", lines: "Edges", edgelabels: "Edge labels", faces: "Faces", arrowheads: "Arrow heads" };
 +const objectTypeVisible = {};
 +Object.assign(objectTypeVisible,modelContains);
 +const sortedObjectTypeKeys = Object.keys(objectTypeInnerHTMLs).sort();
 +const shownObjectTypesList = document.getElementById('shownObjectTypesList_0');
 +
 +function setVisibility(bool,objname) {
 +    for (var i=0; i<scene.children.length; i++){
 +        var obj = scene.children[i].getObjectByName(objname);
 +        if (obj) {
 +            obj.visible = bool;
 +        }
 +    }
 +}
 +
 +function toggleObjectTypeVisibility(event){
 +    var name = event.currentTarget.name;
 +    var checked = event.currentTarget.checked;
 +    objectTypeVisible[name] = checked;
 +    if (name == "faces") {
 +        setVisibility(checked,"frontfaces");
 +        setVisibility(checked,"backfaces");
 +    } else {
 +        setVisibility(checked,name);
 +    }
 +}
 +
 +for (var i=0; i<sortedObjectTypeKeys.length; i++){
 +    var key = sortedObjectTypeKeys[i];
 +    if (modelContains[key]) {
 +        var objTypeNode = document.createElement('span');
 +        objTypeNode.innerHTML = objectTypeInnerHTMLs[key] + '<br>';
 +        var checkbox = document.createElement('input');
 +        checkbox.type = 'checkbox';
 +        checkbox.checked = true;
 +        checkbox.name = key;
 +        checkbox.onchange = toggleObjectTypeVisibility;
 +        shownObjectTypesList.appendChild(checkbox);
 +        shownObjectTypesList.appendChild(objTypeNode);
 +    }
 +}
 +
 +// ------------------------------------------------------
 +
 +function toggleObjectVisibility(event){
 +    var nr = Number(event.currentTarget.name);
 +    scene.children[nr].visible = event.currentTarget.checked;
 +}
 +
 +// append checkboxes for displaying or hiding objects
 +var shownObjectsList = document.getElementById('shownObjectsList_0');
 +for (var i=0; i<scene.children.length; i++){
 +    obj = scene.children[i];
 +    var objNode = document.createElement('span');
 +    objNode.innerHTML = obj.name + '<br>';
 +    var checkbox = document.createElement('input');
 +    checkbox.type = 'checkbox';
 +    checkbox.checked = true;
 +    checkbox.name = String(i);
 +    checkbox.onchange = toggleObjectVisibility;
 +    shownObjectsList.appendChild(checkbox);
 +    shownObjectsList.appendChild(objNode);
 +}
 +
 +// ---------------------- SVG ------------------------------------------------------
 +// ---------------------------------------------------------------------------------
 +
 +function takeSvgScreenshot() {
 +    if (objectTypeVisible["pointlabels"]) {
 +        setVisibility(false,"pointlabels");
 +    }
 +    if (objectTypeVisible["edgelabels"]) {
 +        setVisibility(false,"edgelabels");
 +    }
 +    svgRenderer.render(scene,camera);
 +    svgElement = XMLS.serializeToString(svgRenderer.domElement);
 +    
 +    if (objectTypeVisible["pointlabels"]) {
 +        setVisibility(true,"pointlabels");
 +    }
 +    if (objectTypeVisible["edgelabels"]) {
 +        setVisibility(true,"edgelabels");
 +    }
 +
 +    if (document.getElementById('tab_0').checked){
 +        //show in new tab
 +        var myWindow = window.open("","");
 +        myWindow.document.body.innerHTML = svgElement;
 +    } else{
 +        // download svg file 
 +        download("screenshot.svg", svgElement);
 +    }
 +}
 +
 +function download(filename, text) {
 +    var element = document.createElement('a');
 +    element.setAttribute('href', 'data:text/plain;charset=utf-8,' + encodeURIComponent(text));
 +    element.setAttribute('download', filename);
 +
 +    element.style.display = 'none';
 +    document.body.appendChild(element);
 +
 +    element.click();
 +
 +    document.body.removeChild(element);
 +}
 +
 +
 +document.getElementById('transparencyRange_0').oninput = changeTransparency;
 +document.getElementById('depthWriteCheckbox_0').onchange = toggleDepthWrite;
 +document.getElementById('changeRotationX_0').onchange = changeRotationX;
 +document.getElementById('changeRotationY_0').onchange = changeRotationY;
 +document.getElementById('changeRotationZ_0').onchange = changeRotationZ;
 +document.getElementById('resetButton_0').onclick = resetScene;
 +document.getElementById('rotationSpeedRange_0').oninput = changeRotationSpeedFactor;
 +document.getElementById('takeScreenshot_0').onclick = takeSvgScreenshot;
 +document.getElementById('showSettingsButton_0').onclick = showSettings;
 +document.getElementById('hideSettingsButton_0').onclick = hideSettings;
 +
 +
 +// ------------------ SHORTCUTS --------------------------------------------
 +// -------------------------------------------------------------------------
 +
 +/**
 + * http://www.openjs.com/scripts/events/keyboard_shortcuts/
 + * Version : 2.01.B
 + * By Binny V A
 + * License : BSD
 + */
 +shortcut = {
 + 'all_shortcuts':{},//All the shortcuts are stored in this array
 + 'add': function(shortcut_combination,callback,opt) {
 + //Provide a set of default options
 + var default_options = {
 + 'type':'keydown',
 + 'propagate':false,
 + 'disable_in_input':false,
 + 'target':document,
 + 'keycode':false
 + }
 + if(!opt) opt = default_options;
 + else {
 + for(var dfo in default_options) {
 + if(typeof opt[dfo] == 'undefined') opt[dfo] = default_options[dfo];
 + }
 + }
 +
 + var ele = opt.target;
 + if(typeof opt.target == 'string') ele = document.getElementById(opt.target);
 + var ths = this;
 + shortcut_combination = shortcut_combination.toLowerCase();
 +
 + //The function to be called at keypress
 + var func = function(e) {
 + e = e || window.event;
 +
 + if(opt['disable_in_input']) { //Don't enable shortcut keys in Input, Textarea fields
 + var element;
 + if(e.target) element=e.target;
 + else if(e.srcElement) element=e.srcElement;
 + if(element.nodeType==3) element=element.parentNode;
 +
 + if(element.tagName == 'INPUT' || element.tagName == 'TEXTAREA') return;
 + }
 +
 + //Find Which key is pressed
 + if (e.keyCode) code = e.keyCode;
 + else if (e.which) code = e.which;
 + var character = String.fromCharCode(code).toLowerCase();
 +
 + if(code == 188) character=","; //If the user presses , when the type is onkeydown
 + if(code == 190) character="."; //If the user presses , when the type is onkeydown
 +
 + var keys = shortcut_combination.split("+");
 + //Key Pressed - counts the number of valid keypresses - if it is same as the number of keys, the shortcut function is invoked
 + var kp = 0;
 +
 + //Work around for stupid Shift key bug created by using lowercase - as a result the shift+num combination was broken
 + var shift_nums = {
 + "`":"~",
 + "1":"!",
 + "2":"@",
 + "3":"#",
 + "4":"$",
 + "5":"%",
 + "6":"^",
 + "7":"&",
 + "8":"*",
 + "9":"(",
 + "0":")",
 + "-":"_",
 + "=":"+",
 + ";":":",
 + "'":"\"",
 + ",":"<",
 + ".":">",
 + "/":"?",
 + "\\":"|"
 + }
 + //Special Keys - and their codes
 + var special_keys = {
 + 'esc':27,
 + 'escape':27,
 + 'tab':9,
 + 'space':32,
 + 'return':13,
 + 'enter':13,
 + 'backspace':8,
 +
 + 'scrolllock':145,
 + 'scroll_lock':145,
 + 'scroll':145,
 + 'capslock':20,
 + 'caps_lock':20,
 + 'caps':20,
 + 'numlock':144,
 + 'num_lock':144,
 + 'num':144,
 +
 + 'pause':19,
 + 'break':19,
 +
 + 'insert':45,
 + 'home':36,
 + 'delete':46,
 + 'end':35,
 +
 + 'pageup':33,
 + 'page_up':33,
 + 'pu':33,
 +
 + 'pagedown':34,
 + 'page_down':34,
 + 'pd':34,
 +
 + 'left':37,
 + 'up':38,
 + 'right':39,
 + 'down':40,
 +
 + 'f1':112,
 + 'f2':113,
 + 'f3':114,
 + 'f4':115,
 + 'f5':116,
 + 'f6':117,
 + 'f7':118,
 + 'f8':119,
 + 'f9':120,
 + 'f10':121,
 + 'f11':122,
 + 'f12':123
 + }
 +
 + var modifiers = { 
 + shift: { wanted:false, pressed:false},
 + ctrl : { wanted:false, pressed:false},
 + alt  : { wanted:false, pressed:false},
 + meta : { wanted:false, pressed:false} //Meta is Mac specific
 + };
 +                        
 + if(e.ctrlKey) modifiers.ctrl.pressed = true;
 + if(e.shiftKey) modifiers.shift.pressed = true;
 + if(e.altKey) modifiers.alt.pressed = true;
 + if(e.metaKey)   modifiers.meta.pressed = true;
 +                        
 + for(var i=0; k=keys[i],i<keys.length; i++) {
 + //Modifiers
 + if(k == 'ctrl' || k == 'control') {
 + kp++;
 + modifiers.ctrl.wanted = true;
 +
 + } else if(k == 'shift') {
 + kp++;
 + modifiers.shift.wanted = true;
 +
 + } else if(k == 'alt') {
 + kp++;
 + modifiers.alt.wanted = true;
 + } else if(k == 'meta') {
 + kp++;
 + modifiers.meta.wanted = true;
 + } else if(k.length > 1) { //If it is a special key
 + if(special_keys[k] == code) kp++;
 +
 + } else if(opt['keycode']) {
 + if(opt['keycode'] == code) kp++;
 +
 + } else { //The special keys did not match
 + if(character == k) kp++;
 + else {
 + if(shift_nums[character] && e.shiftKey) { //Stupid Shift key bug created by using lowercase
 + character = shift_nums[character]; 
 + if(character == k) kp++;
 + }
 + }
 + }
 + }
 +
 + if(kp == keys.length && 
 + modifiers.ctrl.pressed == modifiers.ctrl.wanted &&
 + modifiers.shift.pressed == modifiers.shift.wanted &&
 + modifiers.alt.pressed == modifiers.alt.wanted &&
 + modifiers.meta.pressed == modifiers.meta.wanted) {
 + callback(e);
 +
 + if(!opt['propagate']) { //Stop the event
 + //e.cancelBubble is supported by IE - this will kill the bubbling process.
 + e.cancelBubble = true;
 + e.returnValue = false;
 +
 + //e.stopPropagation works in Firefox.
 + if (e.stopPropagation) {
 + e.stopPropagation();
 + e.preventDefault();
 + }
 + return false;
 + }
 + }
 + }
 + this.all_shortcuts[shortcut_combination] = {
 + 'callback':func, 
 + 'target':ele, 
 + 'event': opt['type']
 + };
 + //Attach the function with the event
 + if(ele.addEventListener) ele.addEventListener(opt['type'], func, false);
 + else if(ele.attachEvent) ele.attachEvent('on'+opt['type'], func);
 + else ele['on'+opt['type']] = func;
 + },
 +
 + //Remove the shortcut - just specify the shortcut and I will remove the binding
 + 'remove':function(shortcut_combination) {
 + shortcut_combination = shortcut_combination.toLowerCase();
 + var binding = this.all_shortcuts[shortcut_combination];
 + delete(this.all_shortcuts[shortcut_combination])
 + if(!binding) return;
 + var type = binding['event'];
 + var ele = binding['target'];
 + var callback = binding['callback'];
 +
 + if(ele.detachEvent) ele.detachEvent('on'+type, callback);
 + else if(ele.removeEventListener) ele.removeEventListener(type, callback, false);
 + else ele['on'+type] = false;
 + }
 +}
 +
 +shortcut.add("Alt+Left",function() {
 + var event = new Event('click');
 + if (settingsShown){
 + document.getElementById('hideSettingsButton_0').dispatchEvent(event);
 + } else {
 + document.getElementById('showSettingsButton_0').dispatchEvent(event);
 + }
 +});
 +
 +
 +// COMMON_CODE_BLOCK_END
 +
 +});});
 +      </script>
 +   </body>
 +</html>
 +</HTML>
 +Now we will create yet another new polytope by scaling our random sphere by a factor lambda. (Otherwise there are rather few integral points contained in it.)
 +
 +To this end, we have to multiply every coordinate (except for the homogenising 1 in the beginning) of every vertex by lamda. Then we can create a new polytope by specifying its vertices.
 +
 +<code perl>
 +> $lambda=2;
 +> $s=new Matrix<Rational>([[1,0,0,0],[0,$lambda,0,0],[0,0,$lambda,0],[0,0,0,$lambda]]);
 +> print $s;
 +1 0 0 0
 +0 2 0 0
 +0 0 2 0
 +0 0 0 2
 +> $scaled_rs=new Polytope<Rational>(VERTICES=>($rs->VERTICES * $s), LINEALITY_SPACE=>[]);
 +</code>
 +''%%polymake%%'' can visualise the polytope together with its lattice points:
 +
 +<code perl>
 +> $scaled_rs->VISUAL->LATTICE_COLORED;
 +</code>
 +<HTML>
 +<!--
 +polymake for knusper
 +Thu Mar  3 00:34:23 2022
 +scaled_rs
 +-->
 +
 +
 +<html>
 +   <head>
 +      <meta charset=utf-8>
 +      <title>scaled_rs</title>
 +      <style>
 +/*
 +// COMMON_CODE_BLOCK_BEGIN
 +*/
 +         html {overflow: scroll;}
 +         strong{font-size: 18px;}
 +         canvas { z-index: 8; }
 +         input[type='radio'] {margin-left:0;}
 +         input[type='checkbox'] {margin-right:7px; margin-left: 0px; padding-left:0px;}
 +         .group{padding-bottom: 15px;}
 +         .settings * {z-index: 11; }
 +         .settings{z-index: 10; font-family: Arial, Helvetica, sans-serif; margin-left: 30px; visibility: hidden; width: 14em; height: 96%; border: solid 1px silver; padding: 2px; overflow-y: scroll; box-sizing: border-box; background-color: white; position: absolute;}
 +         .indented{margin-left: 20px; margin-top: 10px; padding-bottom: 0px;} 
 +         .shownObjectsList{overflow: auto; max-width: 150px; max-height: 150px;}
 +         .showSettingsButton{visibility: visible; z-index: 12; position: absolute }
 +         .hideSettingsButton{visibility: hidden; z-index: 12; position: absolute; opacity: 0.5}
 +         button{margin-left: 0; margin-top: 10px}
 +         img{cursor: pointer;}
 +         .suboption{padding-top: 15px;}
 +         #model52769332382 { width: 100%; height: 100%; }
 +         .threejs_container { width: 100%; height: 75vh;}
 +         .settings{max-height: 74vh} 
 +         input[type=range] {
 +           -webkit-appearance: none;
 +           padding:0; 
 +           width:90%; 
 +           margin-left: auto;
 +           margin-right: auto;
 +           margin-top: 15px;
 +           margin-bottom: 15px;
 +           display: block;
 +         }
 +         input[type=range]:focus {
 +           outline: none;
 +         }
 +         input[type=range]::-webkit-slider-runnable-track {
 +           height: 4px;
 +           cursor: pointer;
 +           animate: 0.2s;
 +           box-shadow: 0px 0px 0px #000000;
 +           background: #E3E3E3;
 +           border-radius: 0px;
 +           border: 0px solid #000000;
 +         }
 +         input[type=range]::-webkit-slider-thumb {
 +           box-shadow: 1px 1px 2px #B8B8B8;
 +           border: 1px solid #ABABAB;
 +           height: 13px;
 +           width: 25px;
 +           border-radius: 20px;
 +           background: #E0E0E0;
 +           cursor: pointer;
 +           -webkit-appearance: none;
 +           margin-top: -5px;
 +         }
 +         input[type=range]:focus::-webkit-slider-runnable-track {
 +           background: #E3E3E3;
 +         }
 +         input[type=range]::-moz-range-track {
 +           height: 4px;
 +           cursor: pointer;
 +           animate: 0.2s;
 +           box-shadow: 0px 0px 0px #000000;
 +           background: #E3E3E3;
 +           border-radius: 0px;
 +           border: 0px solid #000000;
 +         }
 +         input[type=range]::-moz-range-thumb {
 +           box-shadow: 1px 1px 2px #B8B8B8;
 +           border: 1px solid #ABABAB;
 +           height: 13px;
 +           width: 25px;
 +           border-radius: 20px;
 +           background: #E0E0E0;
 +           cursor: pointer;
 +         }
 +         input[type=range]::-ms-track {
 +           height: 4px;
 +           cursor: pointer;
 +           animate: 0.2s;
 +           background: transparent;
 +           border-color: transparent;
 +           color: transparent;
 +         }
 +         input[type=range]::-ms-fill-lower {
 +           background: #E3E3E3;
 +           border: 0px solid #000000;
 +           border-radius: 0px;
 +           box-shadow: 0px 0px 0px #000000;
 +         }
 +         input[type=range]::-ms-fill-upper {
 +           background: #E3E3E3;
 +           border: 0px solid #000000;
 +           border-radius: 0px;
 +           box-shadow: 0px 0px 0px #000000;
 +         }
 +         input[type=range]::-ms-thumb {
 +           box-shadow: 1px 1px 2px #B8B8B8;
 +           border: 1px solid #ABABAB;
 +           height: 13px;
 +           width: 25px;
 +           border-radius: 20px;
 +           background: #E0E0E0;
 +           cursor: pointer;
 +         }
 +         input[type=range]:focus::-ms-fill-lower {
 +           background: #E3E3E3;
 +         }
 +         input[type=range]:focus::-ms-fill-upper {
 +           background: #E3E3E3;
 +         }
 +/*
 +// COMMON_CODE_BLOCK_END
 +*/
 + </style>
 +   </head>
 +<body>
 +   <div class='threejs_container'>
 + <div id='settings_1' class='settings'>
 + <div class=group id='explode_1'>
 + <strong>Explode</strong>
 + <input id='explodeRange_1' type='range' min='0.00001' max=6 step=0.01 value=0.00001>
 + <div class=indented><input id='explodeCheckbox_1' type='checkbox'>Automatic explosion</div>
 + <div class=suboption>Exploding speed</div>
 + <input id='explodingSpeedRange_1' type='range' min=0 max=0.5 step=0.001 value=0.05>
 + </div>
 +
 + <div class=group id='transparency_1' class='transparency'>
 + <strong>Transparency</strong>
 + <input id='transparencyRange_1' type='range' min=0 max=1 step=0.01 value=0>
 +            <div class=indented><input id='depthWriteCheckbox_1' type='checkbox'>depthWrite</div>
 + </div>
 +
 + <div class=group id='rotation_1'>
 + <strong>Rotation</strong>
 + <div class=indented>
 + <div><input type='checkbox' id='changeRotationX_1'> x-axis</div>
 + <div><input type='checkbox' id='changeRotationY_1'> y-axis</div>
 + <div><input type='checkbox' id='changeRotationZ_1'> z-axis</div>
 + <button id='resetButton_1'>Reset</button>
 + </div>
 +
 + <div class=suboption>Rotation speed</div>
 + <input id='rotationSpeedRange_1' type='range' min=0 max=5 step=0.01 value=2>
 + </div>
 +
 +
 + <div class=group id='display_1'>
 + <strong>Display</strong>
 + <div class=indented>
 + <div id='shownObjectTypesList_1' class='shownObjectsList'></div>
 + </div>
 + <div class=suboption>Objects</div>
 + <div class=indented>
 +    <div id='shownObjectsList_1' class='shownObjectsList'></div>
 + </div>
 + </div>
 +         
 +         <div class=group id='camera_1'>
 +            <strong>Camera</strong>
 +            <div class=indented>
 +               <form>
 +                  <select id="cameraType_1">
 +                     <option value='perspective' selected> Perspective<br></option>
 +                     <option value='orthographic' > Orthographic<br></option>
 +                  </select>
 +               </form>
 +            </div>
 +         </div>
 +
 + <div class=group id='svg_1'>
 + <strong>SVG</strong>
 + <div class=indented>
 + <form>
 + <input type="radio" name='screenshotMode' value='download' id='download_1' checked> Download<br>
 + <input type="radio" name='screenshotMode' value='tab' id='tab_1' > New tab<br>
 + </form>
 + <button id='takeScreenshot_1'>Screenshot</button>
 + </div>
 + </div>
 +
 + </div> <!-- end of settings -->
 + <img id='hideSettingsButton_1' class='hideSettingsButton' src='/kernelspecs/r118/polymake/close.svg' width=20px">
 + <img id='showSettingsButton_1' class='showSettingsButton' src='/kernelspecs/r118/polymake/menu.svg' width=20px">
 +<div id="model52769332382"></div>
 +</div>
 +   <script>
 +    requirejs.config({
 +      paths: {
 +        three: '/kernelspecs/r118/polymake/three',
 +        TrackballControls: '/kernelspecs/r118/polymake/TrackballControls',
 +        OrbitControls: '/kernelspecs/r118/polymake/OrbitControls',
 +        Projector: '/kernelspecs/r118/polymake/Projector',
 +        SVGRenderer: '/kernelspecs/r118/polymake/SVGRenderer',
 +        WEBGL: '/kernelspecs/r118/polymake/WebGL',
 +      },
 +      shim: {
 +        'three': { exports: 'THREE'},
 +        'SVGRenderer': { deps: [ 'three' ], exports: 'THREE.SVGRenderer' },
 +        'WEBGL': { deps: [ 'three' ], exports: 'THREE.WEBGL' },
 +        'Projector': { deps: [ 'three' ], exports: 'THREE.Projector' },
 +        'TrackballControls': { deps: [ 'three' ], exports: 'THREE.TrackballControls' },
 +        'OrbitControls': { deps: [ 'three' ], exports: 'THREE.OrbitControls' },
 +      }
 +    });
 +    
 +    require(['three'],function(THREE){
 +        window.THREE = THREE;
 +      require(['TrackballControls', 'OrbitControls', 'Projector', 'SVGRenderer', 'WEBGL'],
 +               function(TrackballControls, OrbitControls, Projector, SVGRenderer, WEBGL) {
 +    THREE.TrackballControls = TrackballControls;
 +    THREE.OrbitControls = OrbitControls;
 +    THREE.Projector = Projector;
 +    THREE.SVGRenderer = SVGRenderer;
 +    THREE.WEBGL = WEBGL;
 +
 +// COMMON_CODE_BLOCK_BEGIN
 +
 +const intervalLength = 25; // for automatic animations
 +const explodableModel = true; 
 +const modelContains = { points: false, pointlabels: false, lines: false, edgelabels: false, faces: false, arrowheads: false };
 +const foldables = [];
 +
 +var three = document.getElementById("model52769332382");
 +var scene = new THREE.Scene();
 +var renderer = new THREE.WebGLRenderer( { antialias: true } );
 +var svgRenderer = new THREE.SVGRenderer( { antialias: true } );
 +renderer.setPixelRatio( window.devicePixelRatio );
 +renderer.setClearColor(0xFFFFFF, 1);
 +svgRenderer.setClearColor(0xFFFFFF, 1);
 +three.appendChild(renderer.domElement);
 +
 +var frustumSize = 4;
 +var cameras = [new THREE.PerspectiveCamera(75, 1, 0.1, 1000), new THREE.OrthographicCamera()];
 +cameras.forEach(function(cam) {
 +    cam.position.set(0, 0, 5);
 +    cam.lookAt(0, 0, 0);  
 +    cam.up.set(0, 1, 0);         
 +});
 +var controls = [new THREE.TrackballControls(cameras[0], three), new THREE.OrbitControls(cameras[1], three)];
 +var camera, control;
 +
 +controls[0].zoomSpeed = 0.2;
 +controls[0].rotateSpeed = 4;
 +
 +
 +// class to allow move points together with labels and spheres
 +var PMPoint = function (x,y,z) {
 +   this.vector = new THREE.Vector3(x,y,z);
 +   this.sprite = null;
 +   this.sphere = null;
 +}
 +PMPoint.prototype.addLabel = function(labelsprite) {
 +   this.sprite = labelsprite;
 +   this.sprite.position.copy(this.vector);
 +}
 +PMPoint.prototype.addSphere = function(spheremesh) {
 +   this.sphere = spheremesh;
 +   this.sphere.position.copy(this.vector);
 +}
 +PMPoint.prototype.set = function(x,y,z) {
 +   this.vector.set(x,y,z);
 +   if (this.sprite) {
 +      this.sprite.position.copy(this.vector);
 +   }
 +   if (this.sphere) {
 +      this.sphere.position.copy(this.vector);
 +   }
 +}
 +PMPoint.prototype.radius = function() {
 +   if (this.sphere) {
 +      return this.sphere.geometry.parameters.radius;
 +   } else {
 +      return 0;
 +   }
 +};
 +// select the target node
 +var target = document.querySelector('#model52769332382');
 +
 +// create an observer instance
 +var observer = new MutationObserver(function(mutations) {
 +   mutations.forEach(function(mutation) {
 +      if (mutation.removedNodes && mutation.removedNodes.length > 0) {
 +         cancelAnimationFrame(renderId);
 +         observer.disconnect();
 +         console.log("cancelled frame "+renderId);
 +      }
 +   });
 +});
 +
 +// configuration of the observer:
 +var config = { childList: true, characterData: true }
 +
 +// pass in the target node, as well as the observer options
 +while (target) {
 +   if (target.className=="output") {
 +      observer.observe(target, config);
 +      break;
 +   }
 +   target = target.parentNode;
 +}
 +
 +// COMMON_CODE_BLOCK_END
 +
 +var obj0 = new THREE.Object3D();
 +obj0.name = "scaled_rs";
 +obj0.userData.explodable = 1;
 +obj0.userData.points = [];
 +obj0.userData.points.push(new PMPoint(-0.881007, 1.67354, 0.650463));
 +obj0.userData.points.push(new PMPoint(1.33022, 0.700234, -1.31916));
 +obj0.userData.points.push(new PMPoint(0.499515, -1.58518, 1.11251));
 +obj0.userData.points.push(new PMPoint(-1.15569, -1.63179, -0.0405462));
 +obj0.userData.points.push(new PMPoint(-0.224685, 1.62214, 1.14813));
 +obj0.userData.points.push(new PMPoint(1.08241, 0.0680377, 1.68041));
 +obj0.userData.points.push(new PMPoint(-0.912329, -1.23608, -1.28053));
 +obj0.userData.points.push(new PMPoint(-1.30539, 0.630878, 1.37766));
 +obj0.userData.points.push(new PMPoint(-0.615324, -1.76219, 0.718365));
 +obj0.userData.points.push(new PMPoint(-0.389597, 0.93316, -1.72552));
 +obj0.userData.points.push(new PMPoint(0.0746285, 0.60694, -1.90422));
 +obj0.userData.points.push(new PMPoint(1.38669, 0.666245, 1.27797));
 +obj0.userData.points.push(new PMPoint(1.3257, -0.348459, 1.45639));
 +obj0.userData.points.push(new PMPoint(-1.32001, 1.32228, 0.713539));
 +obj0.userData.points.push(new PMPoint(-0.102571, -0.215617, 1.9857));
 +obj0.userData.points.push(new PMPoint(-1.584, 1.02293, 0.666769));
 +obj0.userData.points.push(new PMPoint(1.47579, 1.08126, -0.808041));
 +obj0.userData.points.push(new PMPoint(0.0944984, 1.69675, 1.05457));
 +obj0.userData.points.push(new PMPoint(-1.50157, -0.0395651, 1.32051));
 +obj0.userData.points.push(new PMPoint(0.662978, -0.26915, 1.86762));
 +
 +obj0.userData.edgeindices = [1, 2, 0, 4, 4, 5, 1, 6, 2, 6, 3, 6, 4, 7, 2, 8, 3, 8, 6, 8, 0, 9, 1, 9, 6, 9, 1, 10, 6, 10, 9, 10, 5, 11, 1, 12, 2, 12, 5, 12, 11, 12, 0, 13, 4, 13, 7, 13, 9, 13, 2, 14, 4, 14, 5, 14, 7, 14, 8, 14, 3, 15, 6, 15, 7, 15, 9, 15, 13, 15, 0, 16, 1, 16, 9, 16, 11, 16, 12, 16, 0, 17, 4, 17, 5, 17, 11, 17, 16, 17, 3, 18, 7, 18, 8, 18, 14, 18, 15, 18, 2, 19, 5, 19, 12, 19, 14, 19];
 +   <!-- Edge style -->
 +obj0.userData.edgematerial = new THREE.LineBasicMaterial( { color: 0x000000, linewidth: 1.5, transparent: false } );
 +obj0.userData.facets = [[5, 11, 17], [12, 11, 5], [12, 5, 19], [12, 19, 2], [19, 14, 2], [4, 17, 0], [14, 4, 7], [14, 18, 8], [14, 7, 18], [0, 9, 13], [13, 9, 15], [15, 9, 6], [18, 15, 3], [7, 13, 15], [18, 7, 15], [15, 6, 3], [8, 18, 3], [6, 8, 3], [4, 13, 7], [4, 0, 13], [9, 10, 6], [2, 14, 8], [6, 2, 8], [5, 4, 14], [5, 17, 4], [5, 14, 19], [9, 1, 10], [1, 6, 10], [1, 2, 6], [1, 12, 2], [0, 16, 9], [17, 16, 0], [16, 1, 9], [16, 12, 1], [17, 11, 16], [16, 11, 12]];
 +init_object(obj0);
 +scene.add(obj0);
 +
 +var obj1 = new THREE.Object3D();
 +obj1.name = "Lattice points and vertices of scaled_rs";
 +obj1.userData.explodable = 1;
 +obj1.userData.points = [];
 +obj1.userData.points.push(new PMPoint(-1, -1, -1));
 +obj1.userData.points.push(new PMPoint(-1, -1, 0));
 +obj1.userData.points.push(new PMPoint(-1, 0, 0));
 +obj1.userData.points.push(new PMPoint(-1, 0, 1));
 +obj1.userData.points.push(new PMPoint(-1, 1, 0));
 +obj1.userData.points.push(new PMPoint(-1, 1, 1));
 +obj1.userData.points.push(new PMPoint(0, -1, 0));
 +obj1.userData.points.push(new PMPoint(0, -1, 1));
 +obj1.userData.points.push(new PMPoint(0, 0, -1));
 +obj1.userData.points.push(new PMPoint(0, 0, 0));
 +obj1.userData.points.push(new PMPoint(0, 0, 1));
 +obj1.userData.points.push(new PMPoint(0, 1, -1));
 +obj1.userData.points.push(new PMPoint(0, 1, 0));
 +obj1.userData.points.push(new PMPoint(0, 1, 1));
 +obj1.userData.points.push(new PMPoint(1, 0, 0));
 +obj1.userData.points.push(new PMPoint(1, 0, 1));
 +obj1.userData.points.push(new PMPoint(1, 1, -1));
 +obj1.userData.points.push(new PMPoint(1, 1, 0));
 +obj1.userData.points.push(new PMPoint(1, 1, 1));
 +obj1.userData.points.push(new PMPoint(-0.881007, 1.67354, 0.650463));
 +obj1.userData.points.push(new PMPoint(1.33022, 0.700234, -1.31916));
 +obj1.userData.points.push(new PMPoint(0.499515, -1.58518, 1.11251));
 +obj1.userData.points.push(new PMPoint(-1.15569, -1.63179, -0.0405462));
 +obj1.userData.points.push(new PMPoint(-0.224685, 1.62214, 1.14813));
 +obj1.userData.points.push(new PMPoint(1.08241, 0.0680377, 1.68041));
 +obj1.userData.points.push(new PMPoint(-0.912329, -1.23608, -1.28053));
 +obj1.userData.points.push(new PMPoint(-1.30539, 0.630878, 1.37766));
 +obj1.userData.points.push(new PMPoint(-0.615324, -1.76219, 0.718365));
 +obj1.userData.points.push(new PMPoint(-0.389597, 0.93316, -1.72552));
 +obj1.userData.points.push(new PMPoint(0.0746285, 0.60694, -1.90422));
 +obj1.userData.points.push(new PMPoint(1.38669, 0.666245, 1.27797));
 +obj1.userData.points.push(new PMPoint(1.3257, -0.348459, 1.45639));
 +obj1.userData.points.push(new PMPoint(-1.32001, 1.32228, 0.713539));
 +obj1.userData.points.push(new PMPoint(-0.102571, -0.215617, 1.9857));
 +obj1.userData.points.push(new PMPoint(-1.584, 1.02293, 0.666769));
 +obj1.userData.points.push(new PMPoint(1.47579, 1.08126, -0.808041));
 +obj1.userData.points.push(new PMPoint(0.0944984, 1.69675, 1.05457));
 +obj1.userData.points.push(new PMPoint(-1.50157, -0.0395651, 1.32051));
 +obj1.userData.points.push(new PMPoint(0.662978, -0.26915, 1.86762));
 +
 +obj1.userData.pointradii = 0.02;
 +   <!-- Vertex style -->
 +obj1.userData.pointmaterial = [new THREE.MeshBasicMaterial( { color: 0x1EFA1E, side: THREE.DoubleSide, transparent: false } ),
 +new THREE.MeshBasicMaterial( { color: 0x1EFA1E, side: THREE.DoubleSide, transparent: false } ),
 +new THREE.MeshBasicMaterial( { color: 0x1EFA1E, side: THREE.DoubleSide, transparent: false } ),
 +new THREE.MeshBasicMaterial( { color: 0x1EFA1E, side: THREE.DoubleSide, transparent: false } ),
 +new THREE.MeshBasicMaterial( { color: 0x1EFA1E, side: THREE.DoubleSide, transparent: false } ),
 +new THREE.MeshBasicMaterial( { color: 0x1EFA1E, side: THREE.DoubleSide, transparent: false } ),
 +new THREE.MeshBasicMaterial( { color: 0x1EFA1E, side: THREE.DoubleSide, transparent: false } ),
 +new THREE.MeshBasicMaterial( { color: 0x1EFA1E, side: THREE.DoubleSide, transparent: false } ),
 +new THREE.MeshBasicMaterial( { color: 0x1EFA1E, side: THREE.DoubleSide, transparent: false } ),
 +new THREE.MeshBasicMaterial( { color: 0x1EFA1E, side: THREE.DoubleSide, transparent: false } ),
 +new THREE.MeshBasicMaterial( { color: 0x1EFA1E, side: THREE.DoubleSide, transparent: false } ),
 +new THREE.MeshBasicMaterial( { color: 0x1EFA1E, side: THREE.DoubleSide, transparent: false } ),
 +new THREE.MeshBasicMaterial( { color: 0x1EFA1E, side: THREE.DoubleSide, transparent: false } ),
 +new THREE.MeshBasicMaterial( { color: 0x1EFA1E, side: THREE.DoubleSide, transparent: false } ),
 +new THREE.MeshBasicMaterial( { color: 0x1EFA1E, side: THREE.DoubleSide, transparent: false } ),
 +new THREE.MeshBasicMaterial( { color: 0x1EFA1E, side: THREE.DoubleSide, transparent: false } ),
 +new THREE.MeshBasicMaterial( { color: 0x1EFA1E, side: THREE.DoubleSide, transparent: false } ),
 +new THREE.MeshBasicMaterial( { color: 0x1EFA1E, side: THREE.DoubleSide, transparent: false } ),
 +new THREE.MeshBasicMaterial( { color: 0x1EFA1E, side: THREE.DoubleSide, transparent: false } ),
 +new THREE.MeshBasicMaterial( { color: 0xFF0000, side: THREE.DoubleSide, transparent: false } ),
 +new THREE.MeshBasicMaterial( { color: 0xFF0000, side: THREE.DoubleSide, transparent: false } ),
 +new THREE.MeshBasicMaterial( { color: 0xFF0000, side: THREE.DoubleSide, transparent: false } ),
 +new THREE.MeshBasicMaterial( { color: 0xFF0000, side: THREE.DoubleSide, transparent: false } ),
 +new THREE.MeshBasicMaterial( { color: 0xFF0000, side: THREE.DoubleSide, transparent: false } ),
 +new THREE.MeshBasicMaterial( { color: 0xFF0000, side: THREE.DoubleSide, transparent: false } ),
 +new THREE.MeshBasicMaterial( { color: 0xFF0000, side: THREE.DoubleSide, transparent: false } ),
 +new THREE.MeshBasicMaterial( { color: 0xFF0000, side: THREE.DoubleSide, transparent: false } ),
 +new THREE.MeshBasicMaterial( { color: 0xFF0000, side: THREE.DoubleSide, transparent: false } ),
 +new THREE.MeshBasicMaterial( { color: 0xFF0000, side: THREE.DoubleSide, transparent: false } ),
 +new THREE.MeshBasicMaterial( { color: 0xFF0000, side: THREE.DoubleSide, transparent: false } ),
 +new THREE.MeshBasicMaterial( { color: 0xFF0000, side: THREE.DoubleSide, transparent: false } ),
 +new THREE.MeshBasicMaterial( { color: 0xFF0000, side: THREE.DoubleSide, transparent: false } ),
 +new THREE.MeshBasicMaterial( { color: 0xFF0000, side: THREE.DoubleSide, transparent: false } ),
 +new THREE.MeshBasicMaterial( { color: 0xFF0000, side: THREE.DoubleSide, transparent: false } ),
 +new THREE.MeshBasicMaterial( { color: 0xFF0000, side: THREE.DoubleSide, transparent: false } ),
 +new THREE.MeshBasicMaterial( { color: 0xFF0000, side: THREE.DoubleSide, transparent: false } ),
 +new THREE.MeshBasicMaterial( { color: 0xFF0000, side: THREE.DoubleSide, transparent: false } ),
 +new THREE.MeshBasicMaterial( { color: 0xFF0000, side: THREE.DoubleSide, transparent: false } ),
 +new THREE.MeshBasicMaterial( { color: 0xFF0000, side: THREE.DoubleSide, transparent: false } )];
 +init_object(obj1);
 +scene.add(obj1);
 +
 +// COMMON_CODE_BLOCK_BEGIN
 +function textSpriteMaterial(message, parameters) {
 +    if ( parameters === undefined ) parameters = {};
 +    var fontface = "Helvetica";
 +    var fontsize = parameters.hasOwnProperty("fontsize") ? parameters["fontsize"] : 15;
 +    fontsize = fontsize*10;
 +    var lines = message.split('\\n');
 +    var size = 512;
 +    for(var i = 0; i<lines.length; i++){
 +        var tmp = lines[i].length;
 +        while(tmp*fontsize > size){
 +           fontsize--;
 +        }
 +    }
 +    
 +    var canvas = document.createElement('canvas');
 +    canvas.width = size;
 +    canvas.height = size;
 +    var context = canvas.getContext('2d');
 +    context.fillStyle = "rgba(255, 255, 255, 0)";
 +    context.fill();
 +    context.font = fontsize + "px " + fontface;
 +    
 +    // text color
 +    context.fillStyle = "rgba(0, 0, 0, 1.0)";
 +     for(var i = 0; i<lines.length; i++){
 +        context.fillText(lines[i], size/2, size/2+i*fontsize);
 +     }
 +    
 +    // canvas contents will be used for a texture
 +    var texture = new THREE.Texture(canvas);
 +    texture.needsUpdate = true;
 +    
 +    var spriteMaterial = new THREE.SpriteMaterial({map: texture, depthTest: true, depthWrite: false, polygonOffset: true, polygonOffsetFactor: -1, polygonOffsetUnits: 1 });
 +    return spriteMaterial;
 +}
 +
 +
 +// ---------------------- INITIALIZING OBJECTS--------------------------------------
 +// ---------------------------------------------------------------------------------
 +
 +function init_object(obj) {
 +    if (obj.userData.hasOwnProperty("pointmaterial")) {
 +        init_points(obj);
 +        modelContains.points = true;
 +    }
 +    if (obj.userData.hasOwnProperty("pointlabels")) {
 +        init_pointlabels(obj);
 +        modelContains.pointlabels = true;
 +    }
 +    if (obj.userData.hasOwnProperty("edgematerial")) {
 +        init_lines(obj);
 +        modelContains.lines = true;
 +    }
 +    if (obj.userData.hasOwnProperty("edgelabels")) {
 +        init_edgelabels(obj);
 +        modelContains.edgelabels = true;
 +    }
 +    if (obj.userData.hasOwnProperty("arrowstyle")) {
 +        init_arrowheads(obj);
 +        modelContains.arrowheads = true;
 +    }
 +    if (obj.userData.hasOwnProperty("facetmaterial")) {
 +        init_faces(obj);
 +        modelContains.faces = true;
 +    }
 +}
 +
 +function init_points(obj) {
 +    var pointgroup = new THREE.Group();
 +    pointgroup.name = "points";
 +    var points = obj.userData.points;
 +    var radii = obj.userData.pointradii;
 +    var materials = obj.userData.pointmaterial;
 +    var geometry,material;
 +    if (!Array.isArray(radii)) {
 +        geometry = new THREE.SphereBufferGeometry(radii);  
 +    }
 +    if (!Array.isArray(materials)) {
 +        material = materials;
 +    }
 +    for (var i=0; i<points.length; i++) {
 +        var point = points[i];
 +        if (Array.isArray(radii)) {
 +            if (radii[i] == 0) {
 +                continue;
 +            }
 +            geometry = new THREE.SphereBufferGeometry(radii[i]);  
 +        } 
 +        if (Array.isArray(materials)) {
 +            material = materials[i];     
 +        } 
 +        var sphere = new THREE.Mesh(geometry, material);
 +        point.addSphere(sphere);
 +        pointgroup.add(sphere);
 +    }
 +    obj.add(pointgroup);
 +}
 +
 +function init_pointlabels(obj) {
 +    var points = obj.userData.points;
 +    var labels = obj.userData.pointlabels;
 +    var pointlabels = new THREE.Group();
 +    pointlabels.name = "pointlabels";
 +    if (Array.isArray(labels)) {
 +        for (var i=0; i<points.length; i++) {
 +            var point = points[i];
 +            var spriteMaterial = textSpriteMaterial( labels[i] );
 +         var sprite = new THREE.Sprite(spriteMaterial);
 +            point.addLabel(sprite);
 +            pointlabels.add(sprite);
 +        }
 +    } else {
 +        var spriteMaterial = textSpriteMaterial( labels );
 +        for (var i=0; i<points.length; i++) {
 +            var point = points[i];
 +         var sprite = new THREE.Sprite(spriteMaterial);
 +            point.addLabel(sprite);
 +            pointlabels.add(sprite);
 +        }
 +    }
 +    obj.add(pointlabels);
 +}
 +
 +function init_lines(obj) {
 +    var edgeindices = obj.userData.edgeindices;
 +    var points = obj.userData.points;
 +    var materials = obj.userData.edgematerial;
 +    var geometry = new THREE.BufferGeometry();
 +    var bufarr = new Float32Array( obj.userData.edgeindices.length * 3 );
 +    var bufattr = new THREE.Float32BufferAttribute( bufarr, 3 );
 +    var geometry = new THREE.BufferGeometry();
 +    geometry.setAttribute('position', bufattr);
 +    if (Array.isArray(materials)) {     
 +        for (var i=0; i<materials.length; i++) {
 +            geometry.addGroup(2*i,2,i);
 +        }
 +    }
 +    var lines = new THREE.LineSegments(geometry, materials);
 +    lines.name = "lines";
 +    obj.add(lines);
 +    updateEdgesPosition(obj);
 +}
 +
 +function init_edgelabels(obj) {
 +    var points = obj.userData.points;
 +    var edgeindices = obj.userData.edgeindices;
 +    var labels = obj.userData.edgelabels;
 +    var edgelabels = new THREE.Group();
 +    edgelabels.name = "edgelabels";
 +    if (Array.isArray(labels)) {
 +        for (var i=0; i<edgeindices.length/2; i++) {
 +            var spriteMaterial = textSpriteMaterial( labels[i] );
 +            var sprite = new THREE.Sprite(spriteMaterial);
 +            sprite.position.copy(new THREE.Vector3().addVectors(points[edgeindices[2*i]].vector,points[edgeindices[2*i+1]].vector).multiplyScalar(0.5));
 +            edgelabels.add(sprite);
 +        }
 +    } else {
 +        var spriteMaterial = textSpriteMaterial( labels );
 +        for (var i=0; i<edgeindices.length/2; i++) {
 +            var sprite = new THREE.Sprite(spriteMaterial);
 +            sprite.position.copy(new THREE.Vector3().addVectors(points[edgeindices[2*i]].vector,points[edgeindices[2*i+1]].vector).multiplyScalar(0.5));
 +            edgelabels.add(sprite);
 +        }
 +    }
 +    obj.add(edgelabels);
 +}
 +
 +function init_arrowheads(obj) {
 +    var arrowheads = new THREE.Group();
 +    arrowheads.name = "arrowheads";
 +    var arrowstyle = obj.userData.arrowstyle;
 +    var edgeindices = obj.userData.edgeindices;
 +    var edgematerials = obj.userData.edgematerial;
 +    var points = obj.userData.points;
 +    var material;
 +    if (!Array.isArray(edgematerials)) {
 +        material = new THREE.MeshBasicMaterial( {color: edgematerials.color} );
 +    }
 +
 +    for (var i=0; i<edgeindices.length; i=i+2) {
 +        var start = points[edgeindices[i]];
 +        var end = points[edgeindices[i+1]];
 +        var dist = start.vector.distanceTo( end.vector ) - start.radius() - end.radius();
 +        if (dist <= 0) {
 +            continue;
 +        }
 +        var dir = new THREE.Vector3().subVectors(end.vector,start.vector);
 +        dir.normalize();
 +        var axis = new THREE.Vector3().set(dir.z,0,-dir.x);
 +        axis.normalize();
 +        var radians = Math.acos( dir.y );
 +        var radius = dist/25;
 +        var height = dist/5;
 +        var geometry = new THREE.ConeBufferGeometry(radius,height);
 +        var position = new THREE.Vector3().addVectors(start.vector,dir.clone().multiplyScalar(start.radius()+dist-height/2));
 +        if (Array.isArray(edgematerials)) {
 +            material = new THREE.MeshBasicMaterial( {color: edgematerials[i].color} );
 +        }
 +        var cone = new THREE.Mesh( geometry, material );
 +        cone.quaternion.setFromAxisAngle(axis,radians);;
 +        cone.position.copy(position);;
 +        arrowheads.add(cone);
 +    }
 +    obj.add(arrowheads);
 +}
 +
 +function init_faces(obj) {
 +    var points = obj.userData.points;
 +    var facets = obj.userData.facets;
 +    obj.userData.triangleindices = [];
 +    for (var i=0; i<facets.length; i++) {
 +        facet = facets[i];
 +        for (var t=0; t<facet.length-2; t++) {
 +            obj.userData.triangleindices.push(facet[0],facet[t+1],facet[t+2]);  
 +        }
 +    }
 +    var bufarr = new Float32Array( obj.userData.triangleindices.length * 3 );
 +    var bufattr = new THREE.Float32BufferAttribute(bufarr,3);
 +    
 +    var materials = obj.userData.facetmaterial;
 +    var geometry = new THREE.BufferGeometry();
 +    var frontmaterials = [];
 +    var backmaterials = [];
 +    geometry.setAttribute('position',bufattr);
 +    if (Array.isArray(materials)) {
 +        var tricount = 0;
 +        var facet;
 +        for (var i=0; i<facets.length; i++) {
 +            facet = facets[i];
 +            geometry.addGroup(tricount,(facet.length-2)*3,i);
 +            tricount += (facet.length-2)*3;
 +        }
 +        for (var j=0; j<materials.length; j++) {
 +            var fmat = materials[j].clone()
 +            fmat.side = THREE.FrontSide;
 +            frontmaterials.push(fmat);
 +            var bmat = materials[j].clone()
 +            bmat.side = THREE.BackSide;
 +            backmaterials.push(bmat);
 +            obj.userData.facetmaterial = frontmaterials.concat(backmaterials);
 +        }
 +    } else if (materials instanceof THREE.Material) {
 +        frontmaterials = materials.clone()
 +        frontmaterials.side = THREE.FrontSide;
 +        backmaterials = materials.clone()
 +        backmaterials.side = THREE.BackSide;
 +        obj.userData.facetmaterial = [frontmaterials, backmaterials];
 +    }
 +    // duplicating the object with front and back should avoid transparency issues
 +    var backmesh = new THREE.Mesh(geometry, backmaterials);
 +    // meshname is used to show/hide objects
 +    backmesh.name = "backfaces";
 +    obj.add(backmesh);
 +    var frontmesh = new THREE.Mesh(geometry, frontmaterials);
 +    frontmesh.name = "frontfaces";
 +    obj.add(frontmesh);
 +    updateFacesPosition(obj);
 +}
 +// //INITIALIZING
 +
 +
 +function updateFacesPosition(obj) {
 +    var points = obj.userData.points;
 +    var indices = obj.userData.triangleindices;
 +    var faces = obj.getObjectByName("frontfaces");
 +    var ba = faces.geometry.getAttribute("position");
 +    for (var i=0; i<indices.length; i++) {
 +        ba.setXYZ(i, points[indices[i]].vector.x, points[indices[i]].vector.y ,points[indices[i]].vector.z); 
 +    }
 +    faces.geometry.attributes.position.needsUpdate = true;
 +    
 +}
 +
 +function updateEdgesPosition(obj) {
 +    var points = obj.userData.points;
 +    var indices = obj.userData.edgeindices;
 +    var lines = obj.getObjectByName("lines");
 +    var ba = lines.geometry.getAttribute("position"); 
 +    for (var i=0; i<indices.length; i++) {
 +        ba.setXYZ(i, points[indices[i]].vector.x, points[indices[i]].vector.y ,points[indices[i]].vector.z); 
 +    }
 +    lines.geometry.attributes.position.needsUpdate = true;
 +}
 +
 +function onWindowResize() {
 +    renderer.setSize( three.clientWidth, three.clientHeight );
 +    svgRenderer.setSize( three.clientWidth, three.clientHeight );
 +    updateCamera();
 +}
 +
 +function updateCamera() {
 +    var width = three.clientWidth;
 +    var height = three.clientHeight;
 +    var aspect = width / height;
 +    if (camera.type == "OrthographicCamera") {
 +        camera.left = frustumSize * aspect / - 2;
 +        camera.right = frustumSize * aspect / 2;
 +        camera.top = frustumSize / 2;
 +        camera.bottom = - frustumSize / 2;
 +    } else if (camera.type == "PerspectiveCamera") {
 +        camera.aspect = aspect;
 +    }
 +    camera.updateProjectionMatrix();
 +}
 +
 +function changeCamera(event) {
 +    var selindex = event.currentTarget.selectedIndex;
 +    camera = cameras[selindex];
 +    control = controls[selindex];
 +    control.enabled = true; 
 +    for (var i=0; i<controls.length; i++) {
 +        if (i!=selindex) {
 +            controls[i].enabled = false;
 +        }
 +    }
 +    updateCamera();
 +}
 +
 +var camtypenode = document.getElementById('cameraType_1');
 +camtypenode.onchange = changeCamera;
 +camtypenode.dispatchEvent(new Event('change'));
 +
 +onWindowResize();
 +window.addEventListener('resize', onWindowResize);
 +
 +
 +var xRotationEnabled = false;
 +var yRotationEnabled = false;
 +var zRotationEnabled = false;
 +var rotationSpeedFactor = 1;
 +var settingsShown = false;
 +var labelsShown = true;
 +var intervals = [];
 +var timeouts = [];
 +var explodingSpeed = 0.05;
 +var explodeScale = 0.000001;
 +var XMLS = new XMLSerializer();
 +var svgElement;
 +var renderId;
 +
 +var render = function () {
 +
 + renderId = requestAnimationFrame(render);
 +
 +// comment in for automatic explosion
 +// explode(updateFactor());
 +
 +    var phi = 0.02 * rotationSpeedFactor;
 +
 +    if (xRotationEnabled) {
 +        scene.rotation.x += phi;
 +    }
 +    if (yRotationEnabled) {
 +        scene.rotation.y += phi;
 +    }
 +    if (zRotationEnabled) {
 +        scene.rotation.z += phi;
 +    }
 +
 +    control.update();
 +    renderer.render(scene, camera);
 +};
 +
 +if ( THREE.WEBGL.isWebGLAvailable() ) {
 + render();
 +} else {
 + var warning = WEBGL.getWebGLErrorMessage();
 + three.appendChild( warning );
 +}
 +    
 +function changeTransparency() {
 +    var opacity = 1-Number(event.currentTarget.value);
 +    for (var i=0; i<scene.children.length; i++) {
 +        child = scene.children[i];
 +        if ( child.userData.hasOwnProperty("facetmaterial") ) {
 +            if (Array.isArray(child.userData.facetmaterial)) {
 +                for (var j=0; j<child.userData.facetmaterial.length; j++) {
 +                    child.userData.facetmaterial[j].opacity = opacity;
 +                }
 +            } else {
 +                child.userData.facetmaterial.opacity = opacity;
 +            }    
 +        }
 +    }
 +}
 +
 +function toggleDepthWrite(event) {
 +    depthwrite = event.currentTarget.checked;
 +    for (var i=0; i<scene.children.length; i++) {
 +        child = scene.children[i];
 +        if ( child.userData.hasOwnProperty("facetmaterial") ) {
 +            if (Array.isArray(child.userData.facetmaterial)) {
 +                for (var j=0; j<child.userData.facetmaterial.length; j++) {
 +                    child.userData.facetmaterial[j].depthWrite = depthwrite;
 +                }
 +            } else {
 +                child.userData.facetmaterial.depthWrite = depthWrite;
 +            }    
 +        }
 +    }
 +}
 +
 +function changeRotationX(event){
 +    xRotationEnabled = event.currentTarget.checked;
 +}
 +
 +function changeRotationY(event){
 +    yRotationEnabled = event.currentTarget.checked;
 +}
 +
 +function changeRotationZ(event){
 +    zRotationEnabled = event.currentTarget.checked;
 +}
 +
 +
 +function changeRotationSpeedFactor(event){
 +    rotationSpeedFactor = Number(event.currentTarget.value);
 +}
 +
 +function resetScene(){
 +    scene.rotation.set(0,0,0);
 +    camera.position.set(0,0,5);
 +    camera.up.set(0,1,0);
 +}
 +
 +function showSettings(event){
 +    document.getElementById('settings_1').style.visibility = 'visible';
 +    document.getElementById('showSettingsButton_1').style.visibility = 'hidden';
 +    document.getElementById('hideSettingsButton_1').style.visibility = 'visible';
 +    settingsShown = true;
 +}
 +
 +function hideSettings(event){
 +    document.getElementById('settings_1').style.visibility = 'hidden';
 +    document.getElementById('showSettingsButton_1').style.visibility = 'visible';
 +    document.getElementById('hideSettingsButton_1').style.visibility = 'hidden';
 +    settingsShown = false;
 +}
 +
 +
 +
 +var pos = 150* Math.PI;
 +
 +function updateFactor() {
 +    pos++;
 +    return Math.sin(.01*pos)+1;
 +}
 +
 +// ------------------------ FOLDING ------------------------------------------------
 +// ---------------------------------------------------------------------------------
 +// rotate point p around axis defined by points p1 and p2 by given angle
 +function rotate(p, p1, p2, angle ){   
 +    angle = -angle;
 +    var x = p.x, y = p.y, z = p.z, 
 +    a = p1.x, b = p1.y, c = p1.z, 
 +    u = p2.x-p1.x, v = p2.y-p1.y, w = p2.z-p1.z;
 +    var result = [];
 +    var L = u*u + v*v + w*w;
 +    var sqrt = Math.sqrt;
 +    var cos = Math.cos;
 +    var sin = Math.sin;
 +
 +    result[0] = ((a*(v*v+w*w)-u*(b*v+c*w-u*x-v*y-w*z))*(1-cos(angle))+L*x*cos(angle)+sqrt(L)*(-c*v+b*w-w*y+v*z)*sin(angle))/L;
 +    result[1] = ((b*(u*u+w*w)-v*(a*u+c*w-u*x-v*y-w*z))*(1-cos(angle))+L*y*cos(angle)+sqrt(L)*(c*u-a*w+w*x-u*z)*sin(angle))/L;
 +    result[2] = ((c*(u*u+v*v)-w*(a*u+b*v-u*x-v*y-w*z))*(1-cos(angle))+L*z*cos(angle)+sqrt(L)*(-b*u+a*v-v*x+u*y)*sin(angle))/L;
 +
 +    return result;
 +}
 +
 +var fold = function(event){
 +    var obj = foldables[Number(event.currentTarget.name)];
 +    var foldvalue = Number(event.currentTarget.value);
 +    var scale = foldvalue - obj.userData.oldscale;
 +
 +    for (var j=0; j<obj.userData.axes.length; j++) {
 +        rotateVertices(obj, j, scale);
 +    }
 +    update(obj);
 +    obj.userData.oldscale += scale;
 +    lookAtBarycenter(obj);
 +}
 +
 +function lookAtBarycenter(obj){
 +    control.target = barycenter(obj);
 +}
 +
 +function barycenter(obj) {
 +    var center = new THREE.Vector3(0,0,0);
 +    var points = obj.userData.points;
 +    for (var i=0; i<points.length; i++){
 +        center.add(points[i].vector);
 +    }
 +    center.divideScalar(points.length);
 +    return center;
 +}
 +
 +function rotateVertices(obj, edge, scale) {
 +    var axes = obj.userData.axes;
 +    var subtrees = obj.userData.subtrees;
 +    var points = obj.userData.points;
 +    var angles = obj.userData.angles;
 +    if (edge < axes.length){
 +        for (var j=0; j<subtrees[edge].length; j++){
 +            var rotP = rotate(points[subtrees[edge][j]].vector, points[axes[edge][0]].vector,points[axes[edge][1]].vector, scale * (Math.PI - angles[edge]));
 +            points[subtrees[edge][j]].set(rotP[0],rotP[1],rotP[2]);
 +        }
 +    }
 +}
 +
 +function update(obj) {
 +   updateFacesPosition(obj);
 +   updateEdgesPosition(obj);
 +}
 +
 +if (foldables.length) {
 +    var settings = document.getElementById('settings_1');
 +    var foldDiv = document.createElement('div');
 +    foldDiv.id = 'fold_1';
 +    var title = document.createElement('strong');
 +    title.innerHTML = 'Fold';
 +    foldDiv.appendChild(title);
 +    foldDiv.className = 'group';
 +    for (var i=0; i<foldables.length; i++) {
 +        var range = document.createElement('input');
 +        range.type = 'range';
 +        range.min = 0;
 +        range.max = 1;
 +        range.value = 0;
 +        range.step = 0.001;
 +        range.name = String(i);
 +        range.oninput = fold;
 +        foldDiv.appendChild(range);
 +    }
 +    lookAtBarycenter(foldables[0]);
 +    settings.insertBefore(foldDiv,settings.childNodes[0]);
 +}
 +
 +    
 +// ---------------------- EXPLOSION ------------------------------------------------
 +// ---------------------------------------------------------------------------------
 +
 +if (explodableModel) {
 +    for (var i=0; i<scene.children.length; i++) {
 +        obj = scene.children[i];
 +        if ( obj.userData.explodable ) {
 +            computeCentroid(obj);
 +        }
 +    }
 +    document.getElementById('explodeRange_1').oninput = triggerExplode;
 +    document.getElementById('explodeCheckbox_1').onchange = triggerAutomaticExplode;
 +    document.getElementById('explodingSpeedRange_1').oninput = setExplodingSpeed;
 +    explode(0.000001);
 +}
 +
 +function computeCentroid(obj) {
 +    centroid = new THREE.Vector3();
 +    obj.userData.points.forEach(function(pmpoint) {
 +        centroid.add(pmpoint.vector);
 +    });
 +    centroid.divideScalar(obj.userData.points.length);
 +    obj.userData.centroid = centroid;
 +}
 +
 +function explode(factor) {
 +    for (var i=0; i<scene.children.length; i++) {
 +        var obj = scene.children[i];
 +        if (obj.userData.hasOwnProperty("centroid")) { 
 +            var c = obj.userData.centroid;
 +            obj.position.set(c.x*factor, c.y*factor, c.z*factor);
 +        }
 +    }
 +}
 +
 +function triggerExplode(event){
 +    explodeScale = Number(event.currentTarget.value);
 +    explode(explodeScale);
 +}
 +
 +function setExplodingSpeed(event){
 +    explodingSpeed = Number(event.currentTarget.value);
 +}
 +
 +function triggerAutomaticExplode(event){
 +    if (event.currentTarget.checked){
 +        startExploding();
 +    } else {
 +        clearIntervals();
 +    }
 +}
 +
 +function startExploding(){
 +    intervals.push(setInterval(explodingInterval, 25));
 +}
 +
 +
 +function explodingInterval(){
 +    explodeScale += explodingSpeed;
 +    if (explodeScale <= 6){ 
 +        explode(explodeScale);
 +    }
 +    else{
 +        explode(6);
 +        explodeScale = 6;
 +        clearIntervals();
 +        timeouts.push(setTimeout(startUnexploding, 3000));
 +    }
 +    document.getElementById('explodeRange_1').value = explodeScale;
 +}
 +
 +
 +function startUnexploding(){
 +    intervals.push(setInterval(unexplodingInterval, 25));
 +}
 +
 +function unexplodingInterval(){
 +    explodeScale -= explodingSpeed;
 +    if (explodeScale >= 0){
 +        explode(explodeScale);
 +    }
 +    else {
 +        explode(0);
 +        explodeScale = 0;
 +        clearIntervals();
 +        timeouts.push(setTimeout(startExploding, 3000));
 +    }
 +    document.getElementById('explodeRange_1').value = explodeScale;
 +}
 +
 +function clearIntervals(){
 +    intervals.forEach(function(interval){
 +        clearInterval(interval);
 +    });
 +    intervals = [];
 +    timeouts.forEach(function(timeout){
 +        clearTimeout(timeout);
 +    });
 +    timeouts = [];
 +}
 +
 +// ---------------------- DISPLAY --------------------------------------------------
 +// ---------------------------------------------------------------------------------
 +
 +const objectTypeInnerHTMLs = { points: "Points", pointlabels: "Point labels", lines: "Edges", edgelabels: "Edge labels", faces: "Faces", arrowheads: "Arrow heads" };
 +const objectTypeVisible = {};
 +Object.assign(objectTypeVisible,modelContains);
 +const sortedObjectTypeKeys = Object.keys(objectTypeInnerHTMLs).sort();
 +const shownObjectTypesList = document.getElementById('shownObjectTypesList_1');
 +
 +function setVisibility(bool,objname) {
 +    for (var i=0; i<scene.children.length; i++){
 +        var obj = scene.children[i].getObjectByName(objname);
 +        if (obj) {
 +            obj.visible = bool;
 +        }
 +    }
 +}
 +
 +function toggleObjectTypeVisibility(event){
 +    var name = event.currentTarget.name;
 +    var checked = event.currentTarget.checked;
 +    objectTypeVisible[name] = checked;
 +    if (name == "faces") {
 +        setVisibility(checked,"frontfaces");
 +        setVisibility(checked,"backfaces");
 +    } else {
 +        setVisibility(checked,name);
 +    }
 +}
 +
 +for (var i=0; i<sortedObjectTypeKeys.length; i++){
 +    var key = sortedObjectTypeKeys[i];
 +    if (modelContains[key]) {
 +        var objTypeNode = document.createElement('span');
 +        objTypeNode.innerHTML = objectTypeInnerHTMLs[key] + '<br>';
 +        var checkbox = document.createElement('input');
 +        checkbox.type = 'checkbox';
 +        checkbox.checked = true;
 +        checkbox.name = key;
 +        checkbox.onchange = toggleObjectTypeVisibility;
 +        shownObjectTypesList.appendChild(checkbox);
 +        shownObjectTypesList.appendChild(objTypeNode);
 +    }
 +}
 +
 +// ------------------------------------------------------
 +
 +function toggleObjectVisibility(event){
 +    var nr = Number(event.currentTarget.name);
 +    scene.children[nr].visible = event.currentTarget.checked;
 +}
 +
 +// append checkboxes for displaying or hiding objects
 +var shownObjectsList = document.getElementById('shownObjectsList_1');
 +for (var i=0; i<scene.children.length; i++){
 +    obj = scene.children[i];
 +    var objNode = document.createElement('span');
 +    objNode.innerHTML = obj.name + '<br>';
 +    var checkbox = document.createElement('input');
 +    checkbox.type = 'checkbox';
 +    checkbox.checked = true;
 +    checkbox.name = String(i);
 +    checkbox.onchange = toggleObjectVisibility;
 +    shownObjectsList.appendChild(checkbox);
 +    shownObjectsList.appendChild(objNode);
 +}
 +
 +// ---------------------- SVG ------------------------------------------------------
 +// ---------------------------------------------------------------------------------
 +
 +function takeSvgScreenshot() {
 +    if (objectTypeVisible["pointlabels"]) {
 +        setVisibility(false,"pointlabels");
 +    }
 +    if (objectTypeVisible["edgelabels"]) {
 +        setVisibility(false,"edgelabels");
 +    }
 +    svgRenderer.render(scene,camera);
 +    svgElement = XMLS.serializeToString(svgRenderer.domElement);
 +    
 +    if (objectTypeVisible["pointlabels"]) {
 +        setVisibility(true,"pointlabels");
 +    }
 +    if (objectTypeVisible["edgelabels"]) {
 +        setVisibility(true,"edgelabels");
 +    }
 +
 +    if (document.getElementById('tab_1').checked){
 +        //show in new tab
 +        var myWindow = window.open("","");
 +        myWindow.document.body.innerHTML = svgElement;
 +    } else{
 +        // download svg file 
 +        download("screenshot.svg", svgElement);
 +    }
 +}
 +
 +function download(filename, text) {
 +    var element = document.createElement('a');
 +    element.setAttribute('href', 'data:text/plain;charset=utf-8,' + encodeURIComponent(text));
 +    element.setAttribute('download', filename);
 +
 +    element.style.display = 'none';
 +    document.body.appendChild(element);
 +
 +    element.click();
 +
 +    document.body.removeChild(element);
 +}
 +
 +
 +document.getElementById('transparencyRange_1').oninput = changeTransparency;
 +document.getElementById('depthWriteCheckbox_1').onchange = toggleDepthWrite;
 +document.getElementById('changeRotationX_1').onchange = changeRotationX;
 +document.getElementById('changeRotationY_1').onchange = changeRotationY;
 +document.getElementById('changeRotationZ_1').onchange = changeRotationZ;
 +document.getElementById('resetButton_1').onclick = resetScene;
 +document.getElementById('rotationSpeedRange_1').oninput = changeRotationSpeedFactor;
 +document.getElementById('takeScreenshot_1').onclick = takeSvgScreenshot;
 +document.getElementById('showSettingsButton_1').onclick = showSettings;
 +document.getElementById('hideSettingsButton_1').onclick = hideSettings;
 +
 +
 +// ------------------ SHORTCUTS --------------------------------------------
 +// -------------------------------------------------------------------------
 +
 +/**
 + * http://www.openjs.com/scripts/events/keyboard_shortcuts/
 + * Version : 2.01.B
 + * By Binny V A
 + * License : BSD
 + */
 +shortcut = {
 + 'all_shortcuts':{},//All the shortcuts are stored in this array
 + 'add': function(shortcut_combination,callback,opt) {
 + //Provide a set of default options
 + var default_options = {
 + 'type':'keydown',
 + 'propagate':false,
 + 'disable_in_input':false,
 + 'target':document,
 + 'keycode':false
 + }
 + if(!opt) opt = default_options;
 + else {
 + for(var dfo in default_options) {
 + if(typeof opt[dfo] == 'undefined') opt[dfo] = default_options[dfo];
 + }
 + }
 +
 + var ele = opt.target;
 + if(typeof opt.target == 'string') ele = document.getElementById(opt.target);
 + var ths = this;
 + shortcut_combination = shortcut_combination.toLowerCase();
 +
 + //The function to be called at keypress
 + var func = function(e) {
 + e = e || window.event;
 +
 + if(opt['disable_in_input']) { //Don't enable shortcut keys in Input, Textarea fields
 + var element;
 + if(e.target) element=e.target;
 + else if(e.srcElement) element=e.srcElement;
 + if(element.nodeType==3) element=element.parentNode;
 +
 + if(element.tagName == 'INPUT' || element.tagName == 'TEXTAREA') return;
 + }
 +
 + //Find Which key is pressed
 + if (e.keyCode) code = e.keyCode;
 + else if (e.which) code = e.which;
 + var character = String.fromCharCode(code).toLowerCase();
 +
 + if(code == 188) character=","; //If the user presses , when the type is onkeydown
 + if(code == 190) character="."; //If the user presses , when the type is onkeydown
 +
 + var keys = shortcut_combination.split("+");
 + //Key Pressed - counts the number of valid keypresses - if it is same as the number of keys, the shortcut function is invoked
 + var kp = 0;
 +
 + //Work around for stupid Shift key bug created by using lowercase - as a result the shift+num combination was broken
 + var shift_nums = {
 + "`":"~",
 + "1":"!",
 + "2":"@",
 + "3":"#",
 + "4":"$",
 + "5":"%",
 + "6":"^",
 + "7":"&",
 + "8":"*",
 + "9":"(",
 + "0":")",
 + "-":"_",
 + "=":"+",
 + ";":":",
 + "'":"\"",
 + ",":"<",
 + ".":">",
 + "/":"?",
 + "\\":"|"
 + }
 + //Special Keys - and their codes
 + var special_keys = {
 + 'esc':27,
 + 'escape':27,
 + 'tab':9,
 + 'space':32,
 + 'return':13,
 + 'enter':13,
 + 'backspace':8,
 +
 + 'scrolllock':145,
 + 'scroll_lock':145,
 + 'scroll':145,
 + 'capslock':20,
 + 'caps_lock':20,
 + 'caps':20,
 + 'numlock':144,
 + 'num_lock':144,
 + 'num':144,
 +
 + 'pause':19,
 + 'break':19,
 +
 + 'insert':45,
 + 'home':36,
 + 'delete':46,
 + 'end':35,
 +
 + 'pageup':33,
 + 'page_up':33,
 + 'pu':33,
 +
 + 'pagedown':34,
 + 'page_down':34,
 + 'pd':34,
 +
 + 'left':37,
 + 'up':38,
 + 'right':39,
 + 'down':40,
 +
 + 'f1':112,
 + 'f2':113,
 + 'f3':114,
 + 'f4':115,
 + 'f5':116,
 + 'f6':117,
 + 'f7':118,
 + 'f8':119,
 + 'f9':120,
 + 'f10':121,
 + 'f11':122,
 + 'f12':123
 + }
 +
 + var modifiers = { 
 + shift: { wanted:false, pressed:false},
 + ctrl : { wanted:false, pressed:false},
 + alt  : { wanted:false, pressed:false},
 + meta : { wanted:false, pressed:false} //Meta is Mac specific
 + };
 +                        
 + if(e.ctrlKey) modifiers.ctrl.pressed = true;
 + if(e.shiftKey) modifiers.shift.pressed = true;
 + if(e.altKey) modifiers.alt.pressed = true;
 + if(e.metaKey)   modifiers.meta.pressed = true;
 +                        
 + for(var i=0; k=keys[i],i<keys.length; i++) {
 + //Modifiers
 + if(k == 'ctrl' || k == 'control') {
 + kp++;
 + modifiers.ctrl.wanted = true;
 +
 + } else if(k == 'shift') {
 + kp++;
 + modifiers.shift.wanted = true;
 +
 + } else if(k == 'alt') {
 + kp++;
 + modifiers.alt.wanted = true;
 + } else if(k == 'meta') {
 + kp++;
 + modifiers.meta.wanted = true;
 + } else if(k.length > 1) { //If it is a special key
 + if(special_keys[k] == code) kp++;
 +
 + } else if(opt['keycode']) {
 + if(opt['keycode'] == code) kp++;
 +
 + } else { //The special keys did not match
 + if(character == k) kp++;
 + else {
 + if(shift_nums[character] && e.shiftKey) { //Stupid Shift key bug created by using lowercase
 + character = shift_nums[character]; 
 + if(character == k) kp++;
 + }
 + }
 + }
 + }
 +
 + if(kp == keys.length && 
 + modifiers.ctrl.pressed == modifiers.ctrl.wanted &&
 + modifiers.shift.pressed == modifiers.shift.wanted &&
 + modifiers.alt.pressed == modifiers.alt.wanted &&
 + modifiers.meta.pressed == modifiers.meta.wanted) {
 + callback(e);
 +
 + if(!opt['propagate']) { //Stop the event
 + //e.cancelBubble is supported by IE - this will kill the bubbling process.
 + e.cancelBubble = true;
 + e.returnValue = false;
 +
 + //e.stopPropagation works in Firefox.
 + if (e.stopPropagation) {
 + e.stopPropagation();
 + e.preventDefault();
 + }
 + return false;
 + }
 + }
 + }
 + this.all_shortcuts[shortcut_combination] = {
 + 'callback':func, 
 + 'target':ele, 
 + 'event': opt['type']
 + };
 + //Attach the function with the event
 + if(ele.addEventListener) ele.addEventListener(opt['type'], func, false);
 + else if(ele.attachEvent) ele.attachEvent('on'+opt['type'], func);
 + else ele['on'+opt['type']] = func;
 + },
 +
 + //Remove the shortcut - just specify the shortcut and I will remove the binding
 + 'remove':function(shortcut_combination) {
 + shortcut_combination = shortcut_combination.toLowerCase();
 + var binding = this.all_shortcuts[shortcut_combination];
 + delete(this.all_shortcuts[shortcut_combination])
 + if(!binding) return;
 + var type = binding['event'];
 + var ele = binding['target'];
 + var callback = binding['callback'];
 +
 + if(ele.detachEvent) ele.detachEvent('on'+type, callback);
 + else if(ele.removeEventListener) ele.removeEventListener(type, callback, false);
 + else ele['on'+type] = false;
 + }
 +}
 +
 +shortcut.add("Alt+Left",function() {
 + var event = new Event('click');
 + if (settingsShown){
 + document.getElementById('hideSettingsButton_1').dispatchEvent(event);
 + } else {
 + document.getElementById('showSettingsButton_1').dispatchEvent(event);
 + }
 +});
 +
 +
 +// COMMON_CODE_BLOCK_END
 +
 +});});
 +      </script>
 +   </body>
 +</html>
 +</HTML>
 +Now will construct the integer hull of ''%%$scaled_rs%%'' and visualise it:
 +
 +<code perl>
 +> $integer_hull=new Polytope<Rational>(POINTS=>$scaled_rs->LATTICE_POINTS);
 +> $integer_hull->VISUAL->LATTICE_COLORED;
 +</code>
 +<HTML>
 +<!--
 +polymake for knusper
 +Thu Mar  3 00:34:23 2022
 +integer_hull
 +-->
 +
 +
 +<html>
 +   <head>
 +      <meta charset=utf-8>
 +      <title>integer_hull</title>
 +      <style>
 +/*
 +// COMMON_CODE_BLOCK_BEGIN
 +*/
 +         html {overflow: scroll;}
 +         strong{font-size: 18px;}
 +         canvas { z-index: 8; }
 +         input[type='radio'] {margin-left:0;}
 +         input[type='checkbox'] {margin-right:7px; margin-left: 0px; padding-left:0px;}
 +         .group{padding-bottom: 15px;}
 +         .settings * {z-index: 11; }
 +         .settings{z-index: 10; font-family: Arial, Helvetica, sans-serif; margin-left: 30px; visibility: hidden; width: 14em; height: 96%; border: solid 1px silver; padding: 2px; overflow-y: scroll; box-sizing: border-box; background-color: white; position: absolute;}
 +         .indented{margin-left: 20px; margin-top: 10px; padding-bottom: 0px;} 
 +         .shownObjectsList{overflow: auto; max-width: 150px; max-height: 150px;}
 +         .showSettingsButton{visibility: visible; z-index: 12; position: absolute }
 +         .hideSettingsButton{visibility: hidden; z-index: 12; position: absolute; opacity: 0.5}
 +         button{margin-left: 0; margin-top: 10px}
 +         img{cursor: pointer;}
 +         .suboption{padding-top: 15px;}
 +         #model99943158435 { width: 100%; height: 100%; }
 +         .threejs_container { width: 100%; height: 75vh;}
 +         .settings{max-height: 74vh} 
 +         input[type=range] {
 +           -webkit-appearance: none;
 +           padding:0; 
 +           width:90%; 
 +           margin-left: auto;
 +           margin-right: auto;
 +           margin-top: 15px;
 +           margin-bottom: 15px;
 +           display: block;
 +         }
 +         input[type=range]:focus {
 +           outline: none;
 +         }
 +         input[type=range]::-webkit-slider-runnable-track {
 +           height: 4px;
 +           cursor: pointer;
 +           animate: 0.2s;
 +           box-shadow: 0px 0px 0px #000000;
 +           background: #E3E3E3;
 +           border-radius: 0px;
 +           border: 0px solid #000000;
 +         }
 +         input[type=range]::-webkit-slider-thumb {
 +           box-shadow: 1px 1px 2px #B8B8B8;
 +           border: 1px solid #ABABAB;
 +           height: 13px;
 +           width: 25px;
 +           border-radius: 20px;
 +           background: #E0E0E0;
 +           cursor: pointer;
 +           -webkit-appearance: none;
 +           margin-top: -5px;
 +         }
 +         input[type=range]:focus::-webkit-slider-runnable-track {
 +           background: #E3E3E3;
 +         }
 +         input[type=range]::-moz-range-track {
 +           height: 4px;
 +           cursor: pointer;
 +           animate: 0.2s;
 +           box-shadow: 0px 0px 0px #000000;
 +           background: #E3E3E3;
 +           border-radius: 0px;
 +           border: 0px solid #000000;
 +         }
 +         input[type=range]::-moz-range-thumb {
 +           box-shadow: 1px 1px 2px #B8B8B8;
 +           border: 1px solid #ABABAB;
 +           height: 13px;
 +           width: 25px;
 +           border-radius: 20px;
 +           background: #E0E0E0;
 +           cursor: pointer;
 +         }
 +         input[type=range]::-ms-track {
 +           height: 4px;
 +           cursor: pointer;
 +           animate: 0.2s;
 +           background: transparent;
 +           border-color: transparent;
 +           color: transparent;
 +         }
 +         input[type=range]::-ms-fill-lower {
 +           background: #E3E3E3;
 +           border: 0px solid #000000;
 +           border-radius: 0px;
 +           box-shadow: 0px 0px 0px #000000;
 +         }
 +         input[type=range]::-ms-fill-upper {
 +           background: #E3E3E3;
 +           border: 0px solid #000000;
 +           border-radius: 0px;
 +           box-shadow: 0px 0px 0px #000000;
 +         }
 +         input[type=range]::-ms-thumb {
 +           box-shadow: 1px 1px 2px #B8B8B8;
 +           border: 1px solid #ABABAB;
 +           height: 13px;
 +           width: 25px;
 +           border-radius: 20px;
 +           background: #E0E0E0;
 +           cursor: pointer;
 +         }
 +         input[type=range]:focus::-ms-fill-lower {
 +           background: #E3E3E3;
 +         }
 +         input[type=range]:focus::-ms-fill-upper {
 +           background: #E3E3E3;
 +         }
 +/*
 +// COMMON_CODE_BLOCK_END
 +*/
 + </style>
 +   </head>
 +<body>
 +   <div class='threejs_container'>
 + <div id='settings_2' class='settings'>
 + <div class=group id='explode_2'>
 + <strong>Explode</strong>
 + <input id='explodeRange_2' type='range' min='0.00001' max=6 step=0.01 value=0.00001>
 + <div class=indented><input id='explodeCheckbox_2' type='checkbox'>Automatic explosion</div>
 + <div class=suboption>Exploding speed</div>
 + <input id='explodingSpeedRange_2' type='range' min=0 max=0.5 step=0.001 value=0.05>
 + </div>
 +
 + <div class=group id='transparency_2' class='transparency'>
 + <strong>Transparency</strong>
 + <input id='transparencyRange_2' type='range' min=0 max=1 step=0.01 value=0>
 +            <div class=indented><input id='depthWriteCheckbox_2' type='checkbox'>depthWrite</div>
 + </div>
 +
 + <div class=group id='rotation_2'>
 + <strong>Rotation</strong>
 + <div class=indented>
 + <div><input type='checkbox' id='changeRotationX_2'> x-axis</div>
 + <div><input type='checkbox' id='changeRotationY_2'> y-axis</div>
 + <div><input type='checkbox' id='changeRotationZ_2'> z-axis</div>
 + <button id='resetButton_2'>Reset</button>
 + </div>
 +
 + <div class=suboption>Rotation speed</div>
 + <input id='rotationSpeedRange_2' type='range' min=0 max=5 step=0.01 value=2>
 + </div>
 +
 +
 + <div class=group id='display_2'>
 + <strong>Display</strong>
 + <div class=indented>
 + <div id='shownObjectTypesList_2' class='shownObjectsList'></div>
 + </div>
 + <div class=suboption>Objects</div>
 + <div class=indented>
 +    <div id='shownObjectsList_2' class='shownObjectsList'></div>
 + </div>
 + </div>
 +         
 +         <div class=group id='camera_2'>
 +            <strong>Camera</strong>
 +            <div class=indented>
 +               <form>
 +                  <select id="cameraType_2">
 +                     <option value='perspective' selected> Perspective<br></option>
 +                     <option value='orthographic' > Orthographic<br></option>
 +                  </select>
 +               </form>
 +            </div>
 +         </div>
 +
 + <div class=group id='svg_2'>
 + <strong>SVG</strong>
 + <div class=indented>
 + <form>
 + <input type="radio" name='screenshotMode' value='download' id='download_2' checked> Download<br>
 + <input type="radio" name='screenshotMode' value='tab' id='tab_2' > New tab<br>
 + </form>
 + <button id='takeScreenshot_2'>Screenshot</button>
 + </div>
 + </div>
 +
 + </div> <!-- end of settings -->
 + <img id='hideSettingsButton_2' class='hideSettingsButton' src='/kernelspecs/r118/polymake/close.svg' width=20px">
 + <img id='showSettingsButton_2' class='showSettingsButton' src='/kernelspecs/r118/polymake/menu.svg' width=20px">
 +<div id="model99943158435"></div>
 +</div>
 +   <script>
 +    requirejs.config({
 +      paths: {
 +        three: '/kernelspecs/r118/polymake/three',
 +        TrackballControls: '/kernelspecs/r118/polymake/TrackballControls',
 +        OrbitControls: '/kernelspecs/r118/polymake/OrbitControls',
 +        Projector: '/kernelspecs/r118/polymake/Projector',
 +        SVGRenderer: '/kernelspecs/r118/polymake/SVGRenderer',
 +        WEBGL: '/kernelspecs/r118/polymake/WebGL',
 +      },
 +      shim: {
 +        'three': { exports: 'THREE'},
 +        'SVGRenderer': { deps: [ 'three' ], exports: 'THREE.SVGRenderer' },
 +        'WEBGL': { deps: [ 'three' ], exports: 'THREE.WEBGL' },
 +        'Projector': { deps: [ 'three' ], exports: 'THREE.Projector' },
 +        'TrackballControls': { deps: [ 'three' ], exports: 'THREE.TrackballControls' },
 +        'OrbitControls': { deps: [ 'three' ], exports: 'THREE.OrbitControls' },
 +      }
 +    });
 +    
 +    require(['three'],function(THREE){
 +        window.THREE = THREE;
 +      require(['TrackballControls', 'OrbitControls', 'Projector', 'SVGRenderer', 'WEBGL'],
 +               function(TrackballControls, OrbitControls, Projector, SVGRenderer, WEBGL) {
 +    THREE.TrackballControls = TrackballControls;
 +    THREE.OrbitControls = OrbitControls;
 +    THREE.Projector = Projector;
 +    THREE.SVGRenderer = SVGRenderer;
 +    THREE.WEBGL = WEBGL;
 +
 +// COMMON_CODE_BLOCK_BEGIN
 +
 +const intervalLength = 25; // for automatic animations
 +const explodableModel = true; 
 +const modelContains = { points: false, pointlabels: false, lines: false, edgelabels: false, faces: false, arrowheads: false };
 +const foldables = [];
 +
 +var three = document.getElementById("model99943158435");
 +var scene = new THREE.Scene();
 +var renderer = new THREE.WebGLRenderer( { antialias: true } );
 +var svgRenderer = new THREE.SVGRenderer( { antialias: true } );
 +renderer.setPixelRatio( window.devicePixelRatio );
 +renderer.setClearColor(0xFFFFFF, 1);
 +svgRenderer.setClearColor(0xFFFFFF, 1);
 +three.appendChild(renderer.domElement);
 +
 +var frustumSize = 4;
 +var cameras = [new THREE.PerspectiveCamera(75, 1, 0.1, 1000), new THREE.OrthographicCamera()];
 +cameras.forEach(function(cam) {
 +    cam.position.set(0, 0, 5);
 +    cam.lookAt(0, 0, 0);  
 +    cam.up.set(0, 1, 0);         
 +});
 +var controls = [new THREE.TrackballControls(cameras[0], three), new THREE.OrbitControls(cameras[1], three)];
 +var camera, control;
 +
 +controls[0].zoomSpeed = 0.2;
 +controls[0].rotateSpeed = 4;
 +
 +
 +// class to allow move points together with labels and spheres
 +var PMPoint = function (x,y,z) {
 +   this.vector = new THREE.Vector3(x,y,z);
 +   this.sprite = null;
 +   this.sphere = null;
 +}
 +PMPoint.prototype.addLabel = function(labelsprite) {
 +   this.sprite = labelsprite;
 +   this.sprite.position.copy(this.vector);
 +}
 +PMPoint.prototype.addSphere = function(spheremesh) {
 +   this.sphere = spheremesh;
 +   this.sphere.position.copy(this.vector);
 +}
 +PMPoint.prototype.set = function(x,y,z) {
 +   this.vector.set(x,y,z);
 +   if (this.sprite) {
 +      this.sprite.position.copy(this.vector);
 +   }
 +   if (this.sphere) {
 +      this.sphere.position.copy(this.vector);
 +   }
 +}
 +PMPoint.prototype.radius = function() {
 +   if (this.sphere) {
 +      return this.sphere.geometry.parameters.radius;
 +   } else {
 +      return 0;
 +   }
 +};
 +// select the target node
 +var target = document.querySelector('#model99943158435');
 +
 +// create an observer instance
 +var observer = new MutationObserver(function(mutations) {
 +   mutations.forEach(function(mutation) {
 +      if (mutation.removedNodes && mutation.removedNodes.length > 0) {
 +         cancelAnimationFrame(renderId);
 +         observer.disconnect();
 +         console.log("cancelled frame "+renderId);
 +      }
 +   });
 +});
 +
 +// configuration of the observer:
 +var config = { childList: true, characterData: true }
 +
 +// pass in the target node, as well as the observer options
 +while (target) {
 +   if (target.className=="output") {
 +      observer.observe(target, config);
 +      break;
 +   }
 +   target = target.parentNode;
 +}
 +
 +// COMMON_CODE_BLOCK_END
 +
 +var obj0 = new THREE.Object3D();
 +obj0.name = "integer_hull";
 +obj0.userData.explodable = 1;
 +obj0.userData.points = [];
 +obj0.userData.points.push(new PMPoint(-1, -1, -1));
 +obj0.userData.points.push(new PMPoint(-1, -1, 0));
 +obj0.userData.points.push(new PMPoint(-1, 0, 1));
 +obj0.userData.points.push(new PMPoint(-1, 1, 0));
 +obj0.userData.points.push(new PMPoint(-1, 1, 1));
 +obj0.userData.points.push(new PMPoint(0, -1, 0));
 +obj0.userData.points.push(new PMPoint(0, -1, 1));
 +obj0.userData.points.push(new PMPoint(0, 1, -1));
 +obj0.userData.points.push(new PMPoint(1, 0, 0));
 +obj0.userData.points.push(new PMPoint(1, 0, 1));
 +obj0.userData.points.push(new PMPoint(1, 1, -1));
 +obj0.userData.points.push(new PMPoint(1, 1, 1));
 +
 +obj0.userData.edgeindices = [0, 1, 1, 2, 0, 3, 2, 4, 3, 4, 0, 5, 1, 6, 2, 6, 5, 6, 0, 7, 3, 7, 5, 8, 6, 9, 8, 9, 0, 10, 7, 10, 8, 10, 4, 11, 9, 11, 10, 11];
 +   <!-- Edge style -->
 +obj0.userData.edgematerial = new THREE.LineBasicMaterial( { color: 0x000000, linewidth: 1.5, transparent: false } );
 +obj0.userData.facets = [[6, 5, 8, 9], [7, 0, 3], [0, 5, 6, 1], [6, 2, 1], [2, 4, 3, 0, 1], [8, 5, 0, 10], [10, 0, 7], [6, 9, 11, 4, 2], [9, 8, 10, 11], [11, 10, 7, 3, 4]];
 +init_object(obj0);
 +scene.add(obj0);
 +
 +var obj1 = new THREE.Object3D();
 +obj1.name = "Lattice points and vertices of integer_hull";
 +obj1.userData.explodable = 1;
 +obj1.userData.points = [];
 +obj1.userData.points.push(new PMPoint(0, 0, 0));
 +obj1.userData.points.push(new PMPoint(-1, -1, -1));
 +obj1.userData.points.push(new PMPoint(-1, -1, 0));
 +obj1.userData.points.push(new PMPoint(-1, 0, 0));
 +obj1.userData.points.push(new PMPoint(-1, 0, 1));
 +obj1.userData.points.push(new PMPoint(-1, 1, 0));
 +obj1.userData.points.push(new PMPoint(-1, 1, 1));
 +obj1.userData.points.push(new PMPoint(0, -1, 0));
 +obj1.userData.points.push(new PMPoint(0, -1, 1));
 +obj1.userData.points.push(new PMPoint(0, 0, -1));
 +obj1.userData.points.push(new PMPoint(0, 0, 1));
 +obj1.userData.points.push(new PMPoint(0, 1, -1));
 +obj1.userData.points.push(new PMPoint(0, 1, 0));
 +obj1.userData.points.push(new PMPoint(0, 1, 1));
 +obj1.userData.points.push(new PMPoint(1, 0, 0));
 +obj1.userData.points.push(new PMPoint(1, 0, 1));
 +obj1.userData.points.push(new PMPoint(1, 1, -1));
 +obj1.userData.points.push(new PMPoint(1, 1, 0));
 +obj1.userData.points.push(new PMPoint(1, 1, 1));
 +
 +obj1.userData.pointradii = 0.02;
 +   <!-- Vertex style -->
 +obj1.userData.pointmaterial = [new THREE.MeshBasicMaterial( { color: 0x1EFA1E, side: THREE.DoubleSide, transparent: false } ),
 +new THREE.MeshBasicMaterial( { color: 0x469646, side: THREE.DoubleSide, transparent: false } ),
 +new THREE.MeshBasicMaterial( { color: 0x469646, side: THREE.DoubleSide, transparent: false } ),
 +new THREE.MeshBasicMaterial( { color: 0x469646, side: THREE.DoubleSide, transparent: false } ),
 +new THREE.MeshBasicMaterial( { color: 0x469646, side: THREE.DoubleSide, transparent: false } ),
 +new THREE.MeshBasicMaterial( { color: 0x469646, side: THREE.DoubleSide, transparent: false } ),
 +new THREE.MeshBasicMaterial( { color: 0x469646, side: THREE.DoubleSide, transparent: false } ),
 +new THREE.MeshBasicMaterial( { color: 0x469646, side: THREE.DoubleSide, transparent: false } ),
 +new THREE.MeshBasicMaterial( { color: 0x469646, side: THREE.DoubleSide, transparent: false } ),
 +new THREE.MeshBasicMaterial( { color: 0x469646, side: THREE.DoubleSide, transparent: false } ),
 +new THREE.MeshBasicMaterial( { color: 0x469646, side: THREE.DoubleSide, transparent: false } ),
 +new THREE.MeshBasicMaterial( { color: 0x469646, side: THREE.DoubleSide, transparent: false } ),
 +new THREE.MeshBasicMaterial( { color: 0x469646, side: THREE.DoubleSide, transparent: false } ),
 +new THREE.MeshBasicMaterial( { color: 0x469646, side: THREE.DoubleSide, transparent: false } ),
 +new THREE.MeshBasicMaterial( { color: 0x469646, side: THREE.DoubleSide, transparent: false } ),
 +new THREE.MeshBasicMaterial( { color: 0x469646, side: THREE.DoubleSide, transparent: false } ),
 +new THREE.MeshBasicMaterial( { color: 0x469646, side: THREE.DoubleSide, transparent: false } ),
 +new THREE.MeshBasicMaterial( { color: 0x469646, side: THREE.DoubleSide, transparent: false } ),
 +new THREE.MeshBasicMaterial( { color: 0x469646, side: THREE.DoubleSide, transparent: false } )];
 +init_object(obj1);
 +scene.add(obj1);
 +
 +// COMMON_CODE_BLOCK_BEGIN
 +function textSpriteMaterial(message, parameters) {
 +    if ( parameters === undefined ) parameters = {};
 +    var fontface = "Helvetica";
 +    var fontsize = parameters.hasOwnProperty("fontsize") ? parameters["fontsize"] : 15;
 +    fontsize = fontsize*10;
 +    var lines = message.split('\\n');
 +    var size = 512;
 +    for(var i = 0; i<lines.length; i++){
 +        var tmp = lines[i].length;
 +        while(tmp*fontsize > size){
 +           fontsize--;
 +        }
 +    }
 +    
 +    var canvas = document.createElement('canvas');
 +    canvas.width = size;
 +    canvas.height = size;
 +    var context = canvas.getContext('2d');
 +    context.fillStyle = "rgba(255, 255, 255, 0)";
 +    context.fill();
 +    context.font = fontsize + "px " + fontface;
 +    
 +    // text color
 +    context.fillStyle = "rgba(0, 0, 0, 1.0)";
 +     for(var i = 0; i<lines.length; i++){
 +        context.fillText(lines[i], size/2, size/2+i*fontsize);
 +     }
 +    
 +    // canvas contents will be used for a texture
 +    var texture = new THREE.Texture(canvas);
 +    texture.needsUpdate = true;
 +    
 +    var spriteMaterial = new THREE.SpriteMaterial({map: texture, depthTest: true, depthWrite: false, polygonOffset: true, polygonOffsetFactor: -1, polygonOffsetUnits: 1 });
 +    return spriteMaterial;
 +}
 +
 +
 +// ---------------------- INITIALIZING OBJECTS--------------------------------------
 +// ---------------------------------------------------------------------------------
 +
 +function init_object(obj) {
 +    if (obj.userData.hasOwnProperty("pointmaterial")) {
 +        init_points(obj);
 +        modelContains.points = true;
 +    }
 +    if (obj.userData.hasOwnProperty("pointlabels")) {
 +        init_pointlabels(obj);
 +        modelContains.pointlabels = true;
 +    }
 +    if (obj.userData.hasOwnProperty("edgematerial")) {
 +        init_lines(obj);
 +        modelContains.lines = true;
 +    }
 +    if (obj.userData.hasOwnProperty("edgelabels")) {
 +        init_edgelabels(obj);
 +        modelContains.edgelabels = true;
 +    }
 +    if (obj.userData.hasOwnProperty("arrowstyle")) {
 +        init_arrowheads(obj);
 +        modelContains.arrowheads = true;
 +    }
 +    if (obj.userData.hasOwnProperty("facetmaterial")) {
 +        init_faces(obj);
 +        modelContains.faces = true;
 +    }
 +}
 +
 +function init_points(obj) {
 +    var pointgroup = new THREE.Group();
 +    pointgroup.name = "points";
 +    var points = obj.userData.points;
 +    var radii = obj.userData.pointradii;
 +    var materials = obj.userData.pointmaterial;
 +    var geometry,material;
 +    if (!Array.isArray(radii)) {
 +        geometry = new THREE.SphereBufferGeometry(radii);  
 +    }
 +    if (!Array.isArray(materials)) {
 +        material = materials;
 +    }
 +    for (var i=0; i<points.length; i++) {
 +        var point = points[i];
 +        if (Array.isArray(radii)) {
 +            if (radii[i] == 0) {
 +                continue;
 +            }
 +            geometry = new THREE.SphereBufferGeometry(radii[i]);  
 +        } 
 +        if (Array.isArray(materials)) {
 +            material = materials[i];     
 +        } 
 +        var sphere = new THREE.Mesh(geometry, material);
 +        point.addSphere(sphere);
 +        pointgroup.add(sphere);
 +    }
 +    obj.add(pointgroup);
 +}
 +
 +function init_pointlabels(obj) {
 +    var points = obj.userData.points;
 +    var labels = obj.userData.pointlabels;
 +    var pointlabels = new THREE.Group();
 +    pointlabels.name = "pointlabels";
 +    if (Array.isArray(labels)) {
 +        for (var i=0; i<points.length; i++) {
 +            var point = points[i];
 +            var spriteMaterial = textSpriteMaterial( labels[i] );
 +         var sprite = new THREE.Sprite(spriteMaterial);
 +            point.addLabel(sprite);
 +            pointlabels.add(sprite);
 +        }
 +    } else {
 +        var spriteMaterial = textSpriteMaterial( labels );
 +        for (var i=0; i<points.length; i++) {
 +            var point = points[i];
 +         var sprite = new THREE.Sprite(spriteMaterial);
 +            point.addLabel(sprite);
 +            pointlabels.add(sprite);
 +        }
 +    }
 +    obj.add(pointlabels);
 +}
 +
 +function init_lines(obj) {
 +    var edgeindices = obj.userData.edgeindices;
 +    var points = obj.userData.points;
 +    var materials = obj.userData.edgematerial;
 +    var geometry = new THREE.BufferGeometry();
 +    var bufarr = new Float32Array( obj.userData.edgeindices.length * 3 );
 +    var bufattr = new THREE.Float32BufferAttribute( bufarr, 3 );
 +    var geometry = new THREE.BufferGeometry();
 +    geometry.setAttribute('position', bufattr);
 +    if (Array.isArray(materials)) {     
 +        for (var i=0; i<materials.length; i++) {
 +            geometry.addGroup(2*i,2,i);
 +        }
 +    }
 +    var lines = new THREE.LineSegments(geometry, materials);
 +    lines.name = "lines";
 +    obj.add(lines);
 +    updateEdgesPosition(obj);
 +}
 +
 +function init_edgelabels(obj) {
 +    var points = obj.userData.points;
 +    var edgeindices = obj.userData.edgeindices;
 +    var labels = obj.userData.edgelabels;
 +    var edgelabels = new THREE.Group();
 +    edgelabels.name = "edgelabels";
 +    if (Array.isArray(labels)) {
 +        for (var i=0; i<edgeindices.length/2; i++) {
 +            var spriteMaterial = textSpriteMaterial( labels[i] );
 +            var sprite = new THREE.Sprite(spriteMaterial);
 +            sprite.position.copy(new THREE.Vector3().addVectors(points[edgeindices[2*i]].vector,points[edgeindices[2*i+1]].vector).multiplyScalar(0.5));
 +            edgelabels.add(sprite);
 +        }
 +    } else {
 +        var spriteMaterial = textSpriteMaterial( labels );
 +        for (var i=0; i<edgeindices.length/2; i++) {
 +            var sprite = new THREE.Sprite(spriteMaterial);
 +            sprite.position.copy(new THREE.Vector3().addVectors(points[edgeindices[2*i]].vector,points[edgeindices[2*i+1]].vector).multiplyScalar(0.5));
 +            edgelabels.add(sprite);
 +        }
 +    }
 +    obj.add(edgelabels);
 +}
 +
 +function init_arrowheads(obj) {
 +    var arrowheads = new THREE.Group();
 +    arrowheads.name = "arrowheads";
 +    var arrowstyle = obj.userData.arrowstyle;
 +    var edgeindices = obj.userData.edgeindices;
 +    var edgematerials = obj.userData.edgematerial;
 +    var points = obj.userData.points;
 +    var material;
 +    if (!Array.isArray(edgematerials)) {
 +        material = new THREE.MeshBasicMaterial( {color: edgematerials.color} );
 +    }
 +
 +    for (var i=0; i<edgeindices.length; i=i+2) {
 +        var start = points[edgeindices[i]];
 +        var end = points[edgeindices[i+1]];
 +        var dist = start.vector.distanceTo( end.vector ) - start.radius() - end.radius();
 +        if (dist <= 0) {
 +            continue;
 +        }
 +        var dir = new THREE.Vector3().subVectors(end.vector,start.vector);
 +        dir.normalize();
 +        var axis = new THREE.Vector3().set(dir.z,0,-dir.x);
 +        axis.normalize();
 +        var radians = Math.acos( dir.y );
 +        var radius = dist/25;
 +        var height = dist/5;
 +        var geometry = new THREE.ConeBufferGeometry(radius,height);
 +        var position = new THREE.Vector3().addVectors(start.vector,dir.clone().multiplyScalar(start.radius()+dist-height/2));
 +        if (Array.isArray(edgematerials)) {
 +            material = new THREE.MeshBasicMaterial( {color: edgematerials[i].color} );
 +        }
 +        var cone = new THREE.Mesh( geometry, material );
 +        cone.quaternion.setFromAxisAngle(axis,radians);;
 +        cone.position.copy(position);;
 +        arrowheads.add(cone);
 +    }
 +    obj.add(arrowheads);
 +}
 +
 +function init_faces(obj) {
 +    var points = obj.userData.points;
 +    var facets = obj.userData.facets;
 +    obj.userData.triangleindices = [];
 +    for (var i=0; i<facets.length; i++) {
 +        facet = facets[i];
 +        for (var t=0; t<facet.length-2; t++) {
 +            obj.userData.triangleindices.push(facet[0],facet[t+1],facet[t+2]);  
 +        }
 +    }
 +    var bufarr = new Float32Array( obj.userData.triangleindices.length * 3 );
 +    var bufattr = new THREE.Float32BufferAttribute(bufarr,3);
 +    
 +    var materials = obj.userData.facetmaterial;
 +    var geometry = new THREE.BufferGeometry();
 +    var frontmaterials = [];
 +    var backmaterials = [];
 +    geometry.setAttribute('position',bufattr);
 +    if (Array.isArray(materials)) {
 +        var tricount = 0;
 +        var facet;
 +        for (var i=0; i<facets.length; i++) {
 +            facet = facets[i];
 +            geometry.addGroup(tricount,(facet.length-2)*3,i);
 +            tricount += (facet.length-2)*3;
 +        }
 +        for (var j=0; j<materials.length; j++) {
 +            var fmat = materials[j].clone()
 +            fmat.side = THREE.FrontSide;
 +            frontmaterials.push(fmat);
 +            var bmat = materials[j].clone()
 +            bmat.side = THREE.BackSide;
 +            backmaterials.push(bmat);
 +            obj.userData.facetmaterial = frontmaterials.concat(backmaterials);
 +        }
 +    } else if (materials instanceof THREE.Material) {
 +        frontmaterials = materials.clone()
 +        frontmaterials.side = THREE.FrontSide;
 +        backmaterials = materials.clone()
 +        backmaterials.side = THREE.BackSide;
 +        obj.userData.facetmaterial = [frontmaterials, backmaterials];
 +    }
 +    // duplicating the object with front and back should avoid transparency issues
 +    var backmesh = new THREE.Mesh(geometry, backmaterials);
 +    // meshname is used to show/hide objects
 +    backmesh.name = "backfaces";
 +    obj.add(backmesh);
 +    var frontmesh = new THREE.Mesh(geometry, frontmaterials);
 +    frontmesh.name = "frontfaces";
 +    obj.add(frontmesh);
 +    updateFacesPosition(obj);
 +}
 +// //INITIALIZING
 +
 +
 +function updateFacesPosition(obj) {
 +    var points = obj.userData.points;
 +    var indices = obj.userData.triangleindices;
 +    var faces = obj.getObjectByName("frontfaces");
 +    var ba = faces.geometry.getAttribute("position");
 +    for (var i=0; i<indices.length; i++) {
 +        ba.setXYZ(i, points[indices[i]].vector.x, points[indices[i]].vector.y ,points[indices[i]].vector.z); 
 +    }
 +    faces.geometry.attributes.position.needsUpdate = true;
 +    
 +}
 +
 +function updateEdgesPosition(obj) {
 +    var points = obj.userData.points;
 +    var indices = obj.userData.edgeindices;
 +    var lines = obj.getObjectByName("lines");
 +    var ba = lines.geometry.getAttribute("position"); 
 +    for (var i=0; i<indices.length; i++) {
 +        ba.setXYZ(i, points[indices[i]].vector.x, points[indices[i]].vector.y ,points[indices[i]].vector.z); 
 +    }
 +    lines.geometry.attributes.position.needsUpdate = true;
 +}
 +
 +function onWindowResize() {
 +    renderer.setSize( three.clientWidth, three.clientHeight );
 +    svgRenderer.setSize( three.clientWidth, three.clientHeight );
 +    updateCamera();
 +}
 +
 +function updateCamera() {
 +    var width = three.clientWidth;
 +    var height = three.clientHeight;
 +    var aspect = width / height;
 +    if (camera.type == "OrthographicCamera") {
 +        camera.left = frustumSize * aspect / - 2;
 +        camera.right = frustumSize * aspect / 2;
 +        camera.top = frustumSize / 2;
 +        camera.bottom = - frustumSize / 2;
 +    } else if (camera.type == "PerspectiveCamera") {
 +        camera.aspect = aspect;
 +    }
 +    camera.updateProjectionMatrix();
 +}
 +
 +function changeCamera(event) {
 +    var selindex = event.currentTarget.selectedIndex;
 +    camera = cameras[selindex];
 +    control = controls[selindex];
 +    control.enabled = true; 
 +    for (var i=0; i<controls.length; i++) {
 +        if (i!=selindex) {
 +            controls[i].enabled = false;
 +        }
 +    }
 +    updateCamera();
 +}
 +
 +var camtypenode = document.getElementById('cameraType_2');
 +camtypenode.onchange = changeCamera;
 +camtypenode.dispatchEvent(new Event('change'));
 +
 +onWindowResize();
 +window.addEventListener('resize', onWindowResize);
 +
 +
 +var xRotationEnabled = false;
 +var yRotationEnabled = false;
 +var zRotationEnabled = false;
 +var rotationSpeedFactor = 1;
 +var settingsShown = false;
 +var labelsShown = true;
 +var intervals = [];
 +var timeouts = [];
 +var explodingSpeed = 0.05;
 +var explodeScale = 0.000001;
 +var XMLS = new XMLSerializer();
 +var svgElement;
 +var renderId;
 +
 +var render = function () {
 +
 + renderId = requestAnimationFrame(render);
 +
 +// comment in for automatic explosion
 +// explode(updateFactor());
 +
 +    var phi = 0.02 * rotationSpeedFactor;
 +
 +    if (xRotationEnabled) {
 +        scene.rotation.x += phi;
 +    }
 +    if (yRotationEnabled) {
 +        scene.rotation.y += phi;
 +    }
 +    if (zRotationEnabled) {
 +        scene.rotation.z += phi;
 +    }
 +
 +    control.update();
 +    renderer.render(scene, camera);
 +};
 +
 +if ( THREE.WEBGL.isWebGLAvailable() ) {
 + render();
 +} else {
 + var warning = WEBGL.getWebGLErrorMessage();
 + three.appendChild( warning );
 +}
 +    
 +function changeTransparency() {
 +    var opacity = 1-Number(event.currentTarget.value);
 +    for (var i=0; i<scene.children.length; i++) {
 +        child = scene.children[i];
 +        if ( child.userData.hasOwnProperty("facetmaterial") ) {
 +            if (Array.isArray(child.userData.facetmaterial)) {
 +                for (var j=0; j<child.userData.facetmaterial.length; j++) {
 +                    child.userData.facetmaterial[j].opacity = opacity;
 +                }
 +            } else {
 +                child.userData.facetmaterial.opacity = opacity;
 +            }    
 +        }
 +    }
 +}
 +
 +function toggleDepthWrite(event) {
 +    depthwrite = event.currentTarget.checked;
 +    for (var i=0; i<scene.children.length; i++) {
 +        child = scene.children[i];
 +        if ( child.userData.hasOwnProperty("facetmaterial") ) {
 +            if (Array.isArray(child.userData.facetmaterial)) {
 +                for (var j=0; j<child.userData.facetmaterial.length; j++) {
 +                    child.userData.facetmaterial[j].depthWrite = depthwrite;
 +                }
 +            } else {
 +                child.userData.facetmaterial.depthWrite = depthWrite;
 +            }    
 +        }
 +    }
 +}
 +
 +function changeRotationX(event){
 +    xRotationEnabled = event.currentTarget.checked;
 +}
 +
 +function changeRotationY(event){
 +    yRotationEnabled = event.currentTarget.checked;
 +}
 +
 +function changeRotationZ(event){
 +    zRotationEnabled = event.currentTarget.checked;
 +}
 +
 +
 +function changeRotationSpeedFactor(event){
 +    rotationSpeedFactor = Number(event.currentTarget.value);
 +}
 +
 +function resetScene(){
 +    scene.rotation.set(0,0,0);
 +    camera.position.set(0,0,5);
 +    camera.up.set(0,1,0);
 +}
 +
 +function showSettings(event){
 +    document.getElementById('settings_2').style.visibility = 'visible';
 +    document.getElementById('showSettingsButton_2').style.visibility = 'hidden';
 +    document.getElementById('hideSettingsButton_2').style.visibility = 'visible';
 +    settingsShown = true;
 +}
 +
 +function hideSettings(event){
 +    document.getElementById('settings_2').style.visibility = 'hidden';
 +    document.getElementById('showSettingsButton_2').style.visibility = 'visible';
 +    document.getElementById('hideSettingsButton_2').style.visibility = 'hidden';
 +    settingsShown = false;
 +}
 +
 +
 +
 +var pos = 150* Math.PI;
 +
 +function updateFactor() {
 +    pos++;
 +    return Math.sin(.01*pos)+1;
 +}
 +
 +// ------------------------ FOLDING ------------------------------------------------
 +// ---------------------------------------------------------------------------------
 +// rotate point p around axis defined by points p1 and p2 by given angle
 +function rotate(p, p1, p2, angle ){   
 +    angle = -angle;
 +    var x = p.x, y = p.y, z = p.z, 
 +    a = p1.x, b = p1.y, c = p1.z, 
 +    u = p2.x-p1.x, v = p2.y-p1.y, w = p2.z-p1.z;
 +    var result = [];
 +    var L = u*u + v*v + w*w;
 +    var sqrt = Math.sqrt;
 +    var cos = Math.cos;
 +    var sin = Math.sin;
 +
 +    result[0] = ((a*(v*v+w*w)-u*(b*v+c*w-u*x-v*y-w*z))*(1-cos(angle))+L*x*cos(angle)+sqrt(L)*(-c*v+b*w-w*y+v*z)*sin(angle))/L;
 +    result[1] = ((b*(u*u+w*w)-v*(a*u+c*w-u*x-v*y-w*z))*(1-cos(angle))+L*y*cos(angle)+sqrt(L)*(c*u-a*w+w*x-u*z)*sin(angle))/L;
 +    result[2] = ((c*(u*u+v*v)-w*(a*u+b*v-u*x-v*y-w*z))*(1-cos(angle))+L*z*cos(angle)+sqrt(L)*(-b*u+a*v-v*x+u*y)*sin(angle))/L;
 +
 +    return result;
 +}
 +
 +var fold = function(event){
 +    var obj = foldables[Number(event.currentTarget.name)];
 +    var foldvalue = Number(event.currentTarget.value);
 +    var scale = foldvalue - obj.userData.oldscale;
 +
 +    for (var j=0; j<obj.userData.axes.length; j++) {
 +        rotateVertices(obj, j, scale);
 +    }
 +    update(obj);
 +    obj.userData.oldscale += scale;
 +    lookAtBarycenter(obj);
 +}
 +
 +function lookAtBarycenter(obj){
 +    control.target = barycenter(obj);
 +}
 +
 +function barycenter(obj) {
 +    var center = new THREE.Vector3(0,0,0);
 +    var points = obj.userData.points;
 +    for (var i=0; i<points.length; i++){
 +        center.add(points[i].vector);
 +    }
 +    center.divideScalar(points.length);
 +    return center;
 +}
 +
 +function rotateVertices(obj, edge, scale) {
 +    var axes = obj.userData.axes;
 +    var subtrees = obj.userData.subtrees;
 +    var points = obj.userData.points;
 +    var angles = obj.userData.angles;
 +    if (edge < axes.length){
 +        for (var j=0; j<subtrees[edge].length; j++){
 +            var rotP = rotate(points[subtrees[edge][j]].vector, points[axes[edge][0]].vector,points[axes[edge][1]].vector, scale * (Math.PI - angles[edge]));
 +            points[subtrees[edge][j]].set(rotP[0],rotP[1],rotP[2]);
 +        }
 +    }
 +}
 +
 +function update(obj) {
 +   updateFacesPosition(obj);
 +   updateEdgesPosition(obj);
 +}
 +
 +if (foldables.length) {
 +    var settings = document.getElementById('settings_2');
 +    var foldDiv = document.createElement('div');
 +    foldDiv.id = 'fold_2';
 +    var title = document.createElement('strong');
 +    title.innerHTML = 'Fold';
 +    foldDiv.appendChild(title);
 +    foldDiv.className = 'group';
 +    for (var i=0; i<foldables.length; i++) {
 +        var range = document.createElement('input');
 +        range.type = 'range';
 +        range.min = 0;
 +        range.max = 1;
 +        range.value = 0;
 +        range.step = 0.001;
 +        range.name = String(i);
 +        range.oninput = fold;
 +        foldDiv.appendChild(range);
 +    }
 +    lookAtBarycenter(foldables[0]);
 +    settings.insertBefore(foldDiv,settings.childNodes[0]);
 +}
 +
 +    
 +// ---------------------- EXPLOSION ------------------------------------------------
 +// ---------------------------------------------------------------------------------
 +
 +if (explodableModel) {
 +    for (var i=0; i<scene.children.length; i++) {
 +        obj = scene.children[i];
 +        if ( obj.userData.explodable ) {
 +            computeCentroid(obj);
 +        }
 +    }
 +    document.getElementById('explodeRange_2').oninput = triggerExplode;
 +    document.getElementById('explodeCheckbox_2').onchange = triggerAutomaticExplode;
 +    document.getElementById('explodingSpeedRange_2').oninput = setExplodingSpeed;
 +    explode(0.000001);
 +}
 +
 +function computeCentroid(obj) {
 +    centroid = new THREE.Vector3();
 +    obj.userData.points.forEach(function(pmpoint) {
 +        centroid.add(pmpoint.vector);
 +    });
 +    centroid.divideScalar(obj.userData.points.length);
 +    obj.userData.centroid = centroid;
 +}
 +
 +function explode(factor) {
 +    for (var i=0; i<scene.children.length; i++) {
 +        var obj = scene.children[i];
 +        if (obj.userData.hasOwnProperty("centroid")) { 
 +            var c = obj.userData.centroid;
 +            obj.position.set(c.x*factor, c.y*factor, c.z*factor);
 +        }
 +    }
 +}
 +
 +function triggerExplode(event){
 +    explodeScale = Number(event.currentTarget.value);
 +    explode(explodeScale);
 +}
 +
 +function setExplodingSpeed(event){
 +    explodingSpeed = Number(event.currentTarget.value);
 +}
 +
 +function triggerAutomaticExplode(event){
 +    if (event.currentTarget.checked){
 +        startExploding();
 +    } else {
 +        clearIntervals();
 +    }
 +}
 +
 +function startExploding(){
 +    intervals.push(setInterval(explodingInterval, 25));
 +}
 +
 +
 +function explodingInterval(){
 +    explodeScale += explodingSpeed;
 +    if (explodeScale <= 6){ 
 +        explode(explodeScale);
 +    }
 +    else{
 +        explode(6);
 +        explodeScale = 6;
 +        clearIntervals();
 +        timeouts.push(setTimeout(startUnexploding, 3000));
 +    }
 +    document.getElementById('explodeRange_2').value = explodeScale;
 +}
 +
 +
 +function startUnexploding(){
 +    intervals.push(setInterval(unexplodingInterval, 25));
 +}
 +
 +function unexplodingInterval(){
 +    explodeScale -= explodingSpeed;
 +    if (explodeScale >= 0){
 +        explode(explodeScale);
 +    }
 +    else {
 +        explode(0);
 +        explodeScale = 0;
 +        clearIntervals();
 +        timeouts.push(setTimeout(startExploding, 3000));
 +    }
 +    document.getElementById('explodeRange_2').value = explodeScale;
 +}
 +
 +function clearIntervals(){
 +    intervals.forEach(function(interval){
 +        clearInterval(interval);
 +    });
 +    intervals = [];
 +    timeouts.forEach(function(timeout){
 +        clearTimeout(timeout);
 +    });
 +    timeouts = [];
 +}
 +
 +// ---------------------- DISPLAY --------------------------------------------------
 +// ---------------------------------------------------------------------------------
 +
 +const objectTypeInnerHTMLs = { points: "Points", pointlabels: "Point labels", lines: "Edges", edgelabels: "Edge labels", faces: "Faces", arrowheads: "Arrow heads" };
 +const objectTypeVisible = {};
 +Object.assign(objectTypeVisible,modelContains);
 +const sortedObjectTypeKeys = Object.keys(objectTypeInnerHTMLs).sort();
 +const shownObjectTypesList = document.getElementById('shownObjectTypesList_2');
 +
 +function setVisibility(bool,objname) {
 +    for (var i=0; i<scene.children.length; i++){
 +        var obj = scene.children[i].getObjectByName(objname);
 +        if (obj) {
 +            obj.visible = bool;
 +        }
 +    }
 +}
 +
 +function toggleObjectTypeVisibility(event){
 +    var name = event.currentTarget.name;
 +    var checked = event.currentTarget.checked;
 +    objectTypeVisible[name] = checked;
 +    if (name == "faces") {
 +        setVisibility(checked,"frontfaces");
 +        setVisibility(checked,"backfaces");
 +    } else {
 +        setVisibility(checked,name);
 +    }
 +}
 +
 +for (var i=0; i<sortedObjectTypeKeys.length; i++){
 +    var key = sortedObjectTypeKeys[i];
 +    if (modelContains[key]) {
 +        var objTypeNode = document.createElement('span');
 +        objTypeNode.innerHTML = objectTypeInnerHTMLs[key] + '<br>';
 +        var checkbox = document.createElement('input');
 +        checkbox.type = 'checkbox';
 +        checkbox.checked = true;
 +        checkbox.name = key;
 +        checkbox.onchange = toggleObjectTypeVisibility;
 +        shownObjectTypesList.appendChild(checkbox);
 +        shownObjectTypesList.appendChild(objTypeNode);
 +    }
 +}
 +
 +// ------------------------------------------------------
 +
 +function toggleObjectVisibility(event){
 +    var nr = Number(event.currentTarget.name);
 +    scene.children[nr].visible = event.currentTarget.checked;
 +}
 +
 +// append checkboxes for displaying or hiding objects
 +var shownObjectsList = document.getElementById('shownObjectsList_2');
 +for (var i=0; i<scene.children.length; i++){
 +    obj = scene.children[i];
 +    var objNode = document.createElement('span');
 +    objNode.innerHTML = obj.name + '<br>';
 +    var checkbox = document.createElement('input');
 +    checkbox.type = 'checkbox';
 +    checkbox.checked = true;
 +    checkbox.name = String(i);
 +    checkbox.onchange = toggleObjectVisibility;
 +    shownObjectsList.appendChild(checkbox);
 +    shownObjectsList.appendChild(objNode);
 +}
 +
 +// ---------------------- SVG ------------------------------------------------------
 +// ---------------------------------------------------------------------------------
 +
 +function takeSvgScreenshot() {
 +    if (objectTypeVisible["pointlabels"]) {
 +        setVisibility(false,"pointlabels");
 +    }
 +    if (objectTypeVisible["edgelabels"]) {
 +        setVisibility(false,"edgelabels");
 +    }
 +    svgRenderer.render(scene,camera);
 +    svgElement = XMLS.serializeToString(svgRenderer.domElement);
 +    
 +    if (objectTypeVisible["pointlabels"]) {
 +        setVisibility(true,"pointlabels");
 +    }
 +    if (objectTypeVisible["edgelabels"]) {
 +        setVisibility(true,"edgelabels");
 +    }
 +
 +    if (document.getElementById('tab_2').checked){
 +        //show in new tab
 +        var myWindow = window.open("","");
 +        myWindow.document.body.innerHTML = svgElement;
 +    } else{
 +        // download svg file 
 +        download("screenshot.svg", svgElement);
 +    }
 +}
 +
 +function download(filename, text) {
 +    var element = document.createElement('a');
 +    element.setAttribute('href', 'data:text/plain;charset=utf-8,' + encodeURIComponent(text));
 +    element.setAttribute('download', filename);
 +
 +    element.style.display = 'none';
 +    document.body.appendChild(element);
 +
 +    element.click();
 +
 +    document.body.removeChild(element);
 +}
 +
 +
 +document.getElementById('transparencyRange_2').oninput = changeTransparency;
 +document.getElementById('depthWriteCheckbox_2').onchange = toggleDepthWrite;
 +document.getElementById('changeRotationX_2').onchange = changeRotationX;
 +document.getElementById('changeRotationY_2').onchange = changeRotationY;
 +document.getElementById('changeRotationZ_2').onchange = changeRotationZ;
 +document.getElementById('resetButton_2').onclick = resetScene;
 +document.getElementById('rotationSpeedRange_2').oninput = changeRotationSpeedFactor;
 +document.getElementById('takeScreenshot_2').onclick = takeSvgScreenshot;
 +document.getElementById('showSettingsButton_2').onclick = showSettings;
 +document.getElementById('hideSettingsButton_2').onclick = hideSettings;
 +
 +
 +// ------------------ SHORTCUTS --------------------------------------------
 +// -------------------------------------------------------------------------
 +
 +/**
 + * http://www.openjs.com/scripts/events/keyboard_shortcuts/
 + * Version : 2.01.B
 + * By Binny V A
 + * License : BSD
 + */
 +shortcut = {
 + 'all_shortcuts':{},//All the shortcuts are stored in this array
 + 'add': function(shortcut_combination,callback,opt) {
 + //Provide a set of default options
 + var default_options = {
 + 'type':'keydown',
 + 'propagate':false,
 + 'disable_in_input':false,
 + 'target':document,
 + 'keycode':false
 + }
 + if(!opt) opt = default_options;
 + else {
 + for(var dfo in default_options) {
 + if(typeof opt[dfo] == 'undefined') opt[dfo] = default_options[dfo];
 + }
 + }
 +
 + var ele = opt.target;
 + if(typeof opt.target == 'string') ele = document.getElementById(opt.target);
 + var ths = this;
 + shortcut_combination = shortcut_combination.toLowerCase();
 +
 + //The function to be called at keypress
 + var func = function(e) {
 + e = e || window.event;
 +
 + if(opt['disable_in_input']) { //Don't enable shortcut keys in Input, Textarea fields
 + var element;
 + if(e.target) element=e.target;
 + else if(e.srcElement) element=e.srcElement;
 + if(element.nodeType==3) element=element.parentNode;
 +
 + if(element.tagName == 'INPUT' || element.tagName == 'TEXTAREA') return;
 + }
 +
 + //Find Which key is pressed
 + if (e.keyCode) code = e.keyCode;
 + else if (e.which) code = e.which;
 + var character = String.fromCharCode(code).toLowerCase();
 +
 + if(code == 188) character=","; //If the user presses , when the type is onkeydown
 + if(code == 190) character="."; //If the user presses , when the type is onkeydown
 +
 + var keys = shortcut_combination.split("+");
 + //Key Pressed - counts the number of valid keypresses - if it is same as the number of keys, the shortcut function is invoked
 + var kp = 0;
 +
 + //Work around for stupid Shift key bug created by using lowercase - as a result the shift+num combination was broken
 + var shift_nums = {
 + "`":"~",
 + "1":"!",
 + "2":"@",
 + "3":"#",
 + "4":"$",
 + "5":"%",
 + "6":"^",
 + "7":"&",
 + "8":"*",
 + "9":"(",
 + "0":")",
 + "-":"_",
 + "=":"+",
 + ";":":",
 + "'":"\"",
 + ",":"<",
 + ".":">",
 + "/":"?",
 + "\\":"|"
 + }
 + //Special Keys - and their codes
 + var special_keys = {
 + 'esc':27,
 + 'escape':27,
 + 'tab':9,
 + 'space':32,
 + 'return':13,
 + 'enter':13,
 + 'backspace':8,
 +
 + 'scrolllock':145,
 + 'scroll_lock':145,
 + 'scroll':145,
 + 'capslock':20,
 + 'caps_lock':20,
 + 'caps':20,
 + 'numlock':144,
 + 'num_lock':144,
 + 'num':144,
 +
 + 'pause':19,
 + 'break':19,
 +
 + 'insert':45,
 + 'home':36,
 + 'delete':46,
 + 'end':35,
 +
 + 'pageup':33,
 + 'page_up':33,
 + 'pu':33,
 +
 + 'pagedown':34,
 + 'page_down':34,
 + 'pd':34,
 +
 + 'left':37,
 + 'up':38,
 + 'right':39,
 + 'down':40,
 +
 + 'f1':112,
 + 'f2':113,
 + 'f3':114,
 + 'f4':115,
 + 'f5':116,
 + 'f6':117,
 + 'f7':118,
 + 'f8':119,
 + 'f9':120,
 + 'f10':121,
 + 'f11':122,
 + 'f12':123
 + }
 +
 + var modifiers = { 
 + shift: { wanted:false, pressed:false},
 + ctrl : { wanted:false, pressed:false},
 + alt  : { wanted:false, pressed:false},
 + meta : { wanted:false, pressed:false} //Meta is Mac specific
 + };
 +                        
 + if(e.ctrlKey) modifiers.ctrl.pressed = true;
 + if(e.shiftKey) modifiers.shift.pressed = true;
 + if(e.altKey) modifiers.alt.pressed = true;
 + if(e.metaKey)   modifiers.meta.pressed = true;
 +                        
 + for(var i=0; k=keys[i],i<keys.length; i++) {
 + //Modifiers
 + if(k == 'ctrl' || k == 'control') {
 + kp++;
 + modifiers.ctrl.wanted = true;
 +
 + } else if(k == 'shift') {
 + kp++;
 + modifiers.shift.wanted = true;
 +
 + } else if(k == 'alt') {
 + kp++;
 + modifiers.alt.wanted = true;
 + } else if(k == 'meta') {
 + kp++;
 + modifiers.meta.wanted = true;
 + } else if(k.length > 1) { //If it is a special key
 + if(special_keys[k] == code) kp++;
 +
 + } else if(opt['keycode']) {
 + if(opt['keycode'] == code) kp++;
 +
 + } else { //The special keys did not match
 + if(character == k) kp++;
 + else {
 + if(shift_nums[character] && e.shiftKey) { //Stupid Shift key bug created by using lowercase
 + character = shift_nums[character]; 
 + if(character == k) kp++;
 + }
 + }
 + }
 + }
 +
 + if(kp == keys.length && 
 + modifiers.ctrl.pressed == modifiers.ctrl.wanted &&
 + modifiers.shift.pressed == modifiers.shift.wanted &&
 + modifiers.alt.pressed == modifiers.alt.wanted &&
 + modifiers.meta.pressed == modifiers.meta.wanted) {
 + callback(e);
 +
 + if(!opt['propagate']) { //Stop the event
 + //e.cancelBubble is supported by IE - this will kill the bubbling process.
 + e.cancelBubble = true;
 + e.returnValue = false;
 +
 + //e.stopPropagation works in Firefox.
 + if (e.stopPropagation) {
 + e.stopPropagation();
 + e.preventDefault();
 + }
 + return false;
 + }
 + }
 + }
 + this.all_shortcuts[shortcut_combination] = {
 + 'callback':func, 
 + 'target':ele, 
 + 'event': opt['type']
 + };
 + //Attach the function with the event
 + if(ele.addEventListener) ele.addEventListener(opt['type'], func, false);
 + else if(ele.attachEvent) ele.attachEvent('on'+opt['type'], func);
 + else ele['on'+opt['type']] = func;
 + },
 +
 + //Remove the shortcut - just specify the shortcut and I will remove the binding
 + 'remove':function(shortcut_combination) {
 + shortcut_combination = shortcut_combination.toLowerCase();
 + var binding = this.all_shortcuts[shortcut_combination];
 + delete(this.all_shortcuts[shortcut_combination])
 + if(!binding) return;
 + var type = binding['event'];
 + var ele = binding['target'];
 + var callback = binding['callback'];
 +
 + if(ele.detachEvent) ele.detachEvent('on'+type, callback);
 + else if(ele.removeEventListener) ele.removeEventListener(type, callback, false);
 + else ele['on'+type] = false;
 + }
 +}
 +
 +shortcut.add("Alt+Left",function() {
 + var event = new Event('click');
 + if (settingsShown){
 + document.getElementById('hideSettingsButton_2').dispatchEvent(event);
 + } else {
 + document.getElementById('showSettingsButton_2').dispatchEvent(event);
 + }
 +});
 +
 +
 +// COMMON_CODE_BLOCK_END
 +
 +});});
 +      </script>
 +   </body>
 +</html>
 +</HTML>
 +
 +In order to obtain the integer hull we simply define a new polytope ''%%$integer_hull%%'' as the convex hull of all ''%%LATTICE_POINTS%%'' contained in ''%%$scaled_rs%%''.
 +
 +Note that if we give ''%%POINTS%%'' (in contrast to ''%%VERTICES%%'') ''%%polymake%%'' constructs a polytope that is the convex hull of the given points regardless of whether they are vertices or not. I.e., redundacies are allowed here.
 +
 +If you specify ''%%VERTICES%%'' you have to make sure yourself that your points are actually vertices since ''%%polymake%%'' does not check this. You also need to specify the ''%%LINEALITY_SPACE%%'', see [[apps_polytope|Tutorial on polytopes]].
 +
 +==== Linear Programming ====
 +
 +Now that we have constructed a nice integral polytope we want to apply some linear program to it.
 +
 +First we define a ''%%LinearProgram%%'' with our favourite ''%%LINEAR_OBJECTIVE%%''. The linear objective is an given as a vector of length d+1, d being the dimension of the space. The vector [c<sub>0</sub>,c<sub>1</sub>, ..., c<sub>d</sub>] corresponds to the linear objective c<sub>0</sub> + c<sub>1</sub>x<sub>1</sub> + ... + c<sub>d</sub>x<sub>d</sub>.
 +
 +<code perl>
 +> $objective=new LinearProgram<Rational>(LINEAR_OBJECTIVE=>[0,1,1,1]);
 +</code>
 +Then we define a new polytope, which is a copy of our old one (''%%$inter_hull%%'') with the LP as an additional property.
 +
 +<code perl>
 +> $ilp=new Polytope<Rational>(VERTICES=>$integer_hull->VERTICES, LP=>$objective);
 +</code>
 +{{:tutorials:release:4.11:ilp_and_hilbertbases:ilp_min_face.png|ilp_min_face.png}} {{:tutorials:release:4.11:ilp_and_hilbertbases:ilp_max_face.png|ilp_max_face.png}}
 +
 +And now we can perform some computations:
 +
 +<code perl>
 +> print $ilp->LP->MAXIMAL_VALUE;
 +3
 +> print $ilp->LP->MAXIMAL_FACE;
 +{11}
 +> $ilp->VISUAL->MIN_MAX_FACE;
 +</code>
 +<HTML>
 +<!--
 +polymake for knusper
 +Thu Mar  3 00:34:24 2022
 +ilp
 +-->
 +
 +
 +<html>
 +   <head>
 +      <meta charset=utf-8>
 +      <title>ilp</title>
 +      <style>
 +/*
 +// COMMON_CODE_BLOCK_BEGIN
 +*/
 +         html {overflow: scroll;}
 +         strong{font-size: 18px;}
 +         canvas { z-index: 8; }
 +         input[type='radio'] {margin-left:0;}
 +         input[type='checkbox'] {margin-right:7px; margin-left: 0px; padding-left:0px;}
 +         .group{padding-bottom: 15px;}
 +         .settings * {z-index: 11; }
 +         .settings{z-index: 10; font-family: Arial, Helvetica, sans-serif; margin-left: 30px; visibility: hidden; width: 14em; height: 96%; border: solid 1px silver; padding: 2px; overflow-y: scroll; box-sizing: border-box; background-color: white; position: absolute;}
 +         .indented{margin-left: 20px; margin-top: 10px; padding-bottom: 0px;} 
 +         .shownObjectsList{overflow: auto; max-width: 150px; max-height: 150px;}
 +         .showSettingsButton{visibility: visible; z-index: 12; position: absolute }
 +         .hideSettingsButton{visibility: hidden; z-index: 12; position: absolute; opacity: 0.5}
 +         button{margin-left: 0; margin-top: 10px}
 +         img{cursor: pointer;}
 +         .suboption{padding-top: 15px;}
 +         #model8128755645 { width: 100%; height: 100%; }
 +         .threejs_container { width: 100%; height: 75vh;}
 +         .settings{max-height: 74vh} 
 +         input[type=range] {
 +           -webkit-appearance: none;
 +           padding:0; 
 +           width:90%; 
 +           margin-left: auto;
 +           margin-right: auto;
 +           margin-top: 15px;
 +           margin-bottom: 15px;
 +           display: block;
 +         }
 +         input[type=range]:focus {
 +           outline: none;
 +         }
 +         input[type=range]::-webkit-slider-runnable-track {
 +           height: 4px;
 +           cursor: pointer;
 +           animate: 0.2s;
 +           box-shadow: 0px 0px 0px #000000;
 +           background: #E3E3E3;
 +           border-radius: 0px;
 +           border: 0px solid #000000;
 +         }
 +         input[type=range]::-webkit-slider-thumb {
 +           box-shadow: 1px 1px 2px #B8B8B8;
 +           border: 1px solid #ABABAB;
 +           height: 13px;
 +           width: 25px;
 +           border-radius: 20px;
 +           background: #E0E0E0;
 +           cursor: pointer;
 +           -webkit-appearance: none;
 +           margin-top: -5px;
 +         }
 +         input[type=range]:focus::-webkit-slider-runnable-track {
 +           background: #E3E3E3;
 +         }
 +         input[type=range]::-moz-range-track {
 +           height: 4px;
 +           cursor: pointer;
 +           animate: 0.2s;
 +           box-shadow: 0px 0px 0px #000000;
 +           background: #E3E3E3;
 +           border-radius: 0px;
 +           border: 0px solid #000000;
 +         }
 +         input[type=range]::-moz-range-thumb {
 +           box-shadow: 1px 1px 2px #B8B8B8;
 +           border: 1px solid #ABABAB;
 +           height: 13px;
 +           width: 25px;
 +           border-radius: 20px;
 +           background: #E0E0E0;
 +           cursor: pointer;
 +         }
 +         input[type=range]::-ms-track {
 +           height: 4px;
 +           cursor: pointer;
 +           animate: 0.2s;
 +           background: transparent;
 +           border-color: transparent;
 +           color: transparent;
 +         }
 +         input[type=range]::-ms-fill-lower {
 +           background: #E3E3E3;
 +           border: 0px solid #000000;
 +           border-radius: 0px;
 +           box-shadow: 0px 0px 0px #000000;
 +         }
 +         input[type=range]::-ms-fill-upper {
 +           background: #E3E3E3;
 +           border: 0px solid #000000;
 +           border-radius: 0px;
 +           box-shadow: 0px 0px 0px #000000;
 +         }
 +         input[type=range]::-ms-thumb {
 +           box-shadow: 1px 1px 2px #B8B8B8;
 +           border: 1px solid #ABABAB;
 +           height: 13px;
 +           width: 25px;
 +           border-radius: 20px;
 +           background: #E0E0E0;
 +           cursor: pointer;
 +         }
 +         input[type=range]:focus::-ms-fill-lower {
 +           background: #E3E3E3;
 +         }
 +         input[type=range]:focus::-ms-fill-upper {
 +           background: #E3E3E3;
 +         }
 +/*
 +// COMMON_CODE_BLOCK_END
 +*/
 + </style>
 +   </head>
 +<body>
 +   <div class='threejs_container'>
 + <div id='settings_3' class='settings'>
 + <div class=group id='transparency_3' class='transparency'>
 + <strong>Transparency</strong>
 + <input id='transparencyRange_3' type='range' min=0 max=1 step=0.01 value=0>
 +            <div class=indented><input id='depthWriteCheckbox_3' type='checkbox'>depthWrite</div>
 + </div>
 +
 + <div class=group id='rotation_3'>
 + <strong>Rotation</strong>
 + <div class=indented>
 + <div><input type='checkbox' id='changeRotationX_3'> x-axis</div>
 + <div><input type='checkbox' id='changeRotationY_3'> y-axis</div>
 + <div><input type='checkbox' id='changeRotationZ_3'> z-axis</div>
 + <button id='resetButton_3'>Reset</button>
 + </div>
 +
 + <div class=suboption>Rotation speed</div>
 + <input id='rotationSpeedRange_3' type='range' min=0 max=5 step=0.01 value=2>
 + </div>
 +
 +
 + <div class=group id='display_3'>
 + <strong>Display</strong>
 + <div class=indented>
 + <div id='shownObjectTypesList_3' class='shownObjectsList'></div>
 + </div>
 + <div class=suboption>Objects</div>
 + <div class=indented>
 +    <div id='shownObjectsList_3' class='shownObjectsList'></div>
 + </div>
 + </div>
 +         
 +         <div class=group id='camera_3'>
 +            <strong>Camera</strong>
 +            <div class=indented>
 +               <form>
 +                  <select id="cameraType_3">
 +                     <option value='perspective' selected> Perspective<br></option>
 +                     <option value='orthographic' > Orthographic<br></option>
 +                  </select>
 +               </form>
 +            </div>
 +         </div>
 +
 + <div class=group id='svg_3'>
 + <strong>SVG</strong>
 + <div class=indented>
 + <form>
 + <input type="radio" name='screenshotMode' value='download' id='download_3' checked> Download<br>
 + <input type="radio" name='screenshotMode' value='tab' id='tab_3' > New tab<br>
 + </form>
 + <button id='takeScreenshot_3'>Screenshot</button>
 + </div>
 + </div>
 +
 + </div> <!-- end of settings -->
 + <img id='hideSettingsButton_3' class='hideSettingsButton' src='/kernelspecs/r118/polymake/close.svg' width=20px">
 + <img id='showSettingsButton_3' class='showSettingsButton' src='/kernelspecs/r118/polymake/menu.svg' width=20px">
 +<div id="model8128755645"></div>
 +</div>
 +   <script>
 +    requirejs.config({
 +      paths: {
 +        three: '/kernelspecs/r118/polymake/three',
 +        TrackballControls: '/kernelspecs/r118/polymake/TrackballControls',
 +        OrbitControls: '/kernelspecs/r118/polymake/OrbitControls',
 +        Projector: '/kernelspecs/r118/polymake/Projector',
 +        SVGRenderer: '/kernelspecs/r118/polymake/SVGRenderer',
 +        WEBGL: '/kernelspecs/r118/polymake/WebGL',
 +      },
 +      shim: {
 +        'three': { exports: 'THREE'},
 +        'SVGRenderer': { deps: [ 'three' ], exports: 'THREE.SVGRenderer' },
 +        'WEBGL': { deps: [ 'three' ], exports: 'THREE.WEBGL' },
 +        'Projector': { deps: [ 'three' ], exports: 'THREE.Projector' },
 +        'TrackballControls': { deps: [ 'three' ], exports: 'THREE.TrackballControls' },
 +        'OrbitControls': { deps: [ 'three' ], exports: 'THREE.OrbitControls' },
 +      }
 +    });
 +    
 +    require(['three'],function(THREE){
 +        window.THREE = THREE;
 +      require(['TrackballControls', 'OrbitControls', 'Projector', 'SVGRenderer', 'WEBGL'],
 +               function(TrackballControls, OrbitControls, Projector, SVGRenderer, WEBGL) {
 +    THREE.TrackballControls = TrackballControls;
 +    THREE.OrbitControls = OrbitControls;
 +    THREE.Projector = Projector;
 +    THREE.SVGRenderer = SVGRenderer;
 +    THREE.WEBGL = WEBGL;
 +
 +// COMMON_CODE_BLOCK_BEGIN
 +
 +const intervalLength = 25; // for automatic animations
 +const explodableModel = false; 
 +const modelContains = { points: false, pointlabels: false, lines: false, edgelabels: false, faces: false, arrowheads: false };
 +const foldables = [];
 +
 +var three = document.getElementById("model8128755645");
 +var scene = new THREE.Scene();
 +var renderer = new THREE.WebGLRenderer( { antialias: true } );
 +var svgRenderer = new THREE.SVGRenderer( { antialias: true } );
 +renderer.setPixelRatio( window.devicePixelRatio );
 +renderer.setClearColor(0xFFFFFF, 1);
 +svgRenderer.setClearColor(0xFFFFFF, 1);
 +three.appendChild(renderer.domElement);
 +
 +var frustumSize = 4;
 +var cameras = [new THREE.PerspectiveCamera(75, 1, 0.1, 1000), new THREE.OrthographicCamera()];
 +cameras.forEach(function(cam) {
 +    cam.position.set(0, 0, 5);
 +    cam.lookAt(0, 0, 0);  
 +    cam.up.set(0, 1, 0);         
 +});
 +var controls = [new THREE.TrackballControls(cameras[0], three), new THREE.OrbitControls(cameras[1], three)];
 +var camera, control;
 +
 +controls[0].zoomSpeed = 0.2;
 +controls[0].rotateSpeed = 4;
 +
 +
 +// class to allow move points together with labels and spheres
 +var PMPoint = function (x,y,z) {
 +   this.vector = new THREE.Vector3(x,y,z);
 +   this.sprite = null;
 +   this.sphere = null;
 +}
 +PMPoint.prototype.addLabel = function(labelsprite) {
 +   this.sprite = labelsprite;
 +   this.sprite.position.copy(this.vector);
 +}
 +PMPoint.prototype.addSphere = function(spheremesh) {
 +   this.sphere = spheremesh;
 +   this.sphere.position.copy(this.vector);
 +}
 +PMPoint.prototype.set = function(x,y,z) {
 +   this.vector.set(x,y,z);
 +   if (this.sprite) {
 +      this.sprite.position.copy(this.vector);
 +   }
 +   if (this.sphere) {
 +      this.sphere.position.copy(this.vector);
 +   }
 +}
 +PMPoint.prototype.radius = function() {
 +   if (this.sphere) {
 +      return this.sphere.geometry.parameters.radius;
 +   } else {
 +      return 0;
 +   }
 +};
 +// select the target node
 +var target = document.querySelector('#model8128755645');
 +
 +// create an observer instance
 +var observer = new MutationObserver(function(mutations) {
 +   mutations.forEach(function(mutation) {
 +      if (mutation.removedNodes && mutation.removedNodes.length > 0) {
 +         cancelAnimationFrame(renderId);
 +         observer.disconnect();
 +         console.log("cancelled frame "+renderId);
 +      }
 +   });
 +});
 +
 +// configuration of the observer:
 +var config = { childList: true, characterData: true }
 +
 +// pass in the target node, as well as the observer options
 +while (target) {
 +   if (target.className=="output") {
 +      observer.observe(target, config);
 +      break;
 +   }
 +   target = target.parentNode;
 +}
 +
 +// COMMON_CODE_BLOCK_END
 +
 +var obj0 = new THREE.Object3D();
 +obj0.name = "ilp";
 +obj0.userData.explodable = 1;
 +obj0.userData.points = [];
 +obj0.userData.points.push(new PMPoint(-1, -1, -1));
 +obj0.userData.points.push(new PMPoint(-1, -1, 0));
 +obj0.userData.points.push(new PMPoint(-1, 0, 1));
 +obj0.userData.points.push(new PMPoint(-1, 1, 0));
 +obj0.userData.points.push(new PMPoint(-1, 1, 1));
 +obj0.userData.points.push(new PMPoint(0, -1, 0));
 +obj0.userData.points.push(new PMPoint(0, -1, 1));
 +obj0.userData.points.push(new PMPoint(0, 1, -1));
 +obj0.userData.points.push(new PMPoint(1, 0, 0));
 +obj0.userData.points.push(new PMPoint(1, 0, 1));
 +obj0.userData.points.push(new PMPoint(1, 1, -1));
 +obj0.userData.points.push(new PMPoint(1, 1, 1));
 +
 +obj0.userData.pointradii = 0.02;
 +   <!-- Vertex style -->
 +obj0.userData.pointmaterial = [new THREE.MeshBasicMaterial( { color: 0xFFFF00, side: THREE.DoubleSide, transparent: false } ),
 +new THREE.MeshBasicMaterial( { color: 0xFF0000, side: THREE.DoubleSide, transparent: false } ),
 +new THREE.MeshBasicMaterial( { color: 0xFF0000, side: THREE.DoubleSide, transparent: false } ),
 +new THREE.MeshBasicMaterial( { color: 0xFF0000, side: THREE.DoubleSide, transparent: false } ),
 +new THREE.MeshBasicMaterial( { color: 0xFF0000, side: THREE.DoubleSide, transparent: false } ),
 +new THREE.MeshBasicMaterial( { color: 0xFF0000, side: THREE.DoubleSide, transparent: false } ),
 +new THREE.MeshBasicMaterial( { color: 0xFF0000, side: THREE.DoubleSide, transparent: false } ),
 +new THREE.MeshBasicMaterial( { color: 0xFF0000, side: THREE.DoubleSide, transparent: false } ),
 +new THREE.MeshBasicMaterial( { color: 0xFF0000, side: THREE.DoubleSide, transparent: false } ),
 +new THREE.MeshBasicMaterial( { color: 0xFF0000, side: THREE.DoubleSide, transparent: false } ),
 +new THREE.MeshBasicMaterial( { color: 0xFF0000, side: THREE.DoubleSide, transparent: false } ),
 +new THREE.MeshBasicMaterial( { color: 0xFF0000, side: THREE.DoubleSide, transparent: false } )];
 +obj0.userData.pointlabels = ["0", "1", "2", "3", "4", "5", "6", "7", "8", "9", "10", "11"];
 +obj0.userData.edgeindices = [0, 1, 1, 2, 0, 3, 2, 4, 3, 4, 0, 5, 1, 6, 2, 6, 5, 6, 0, 7, 3, 7, 5, 8, 6, 9, 8, 9, 0, 10, 7, 10, 8, 10, 4, 11, 9, 11, 10, 11];
 +   <!-- Edge style -->
 +obj0.userData.edgematerial = new THREE.LineBasicMaterial( { color: 0x000000, linewidth: 1.5, transparent: false } );
 +obj0.userData.facets = [[0, 10, 8, 5], [7, 10, 0], [0, 5, 6, 1], [1, 6, 2], [0, 1, 2, 4, 3], [3, 7, 0], [5, 8, 9, 6], [9, 11, 4, 2, 6], [8, 10, 11, 9], [11, 10, 7, 3, 4]];
 +   <!-- Facet style -->
 +obj0.userData.facetmaterial = new THREE.MeshBasicMaterial( { color: 0x77EC9E, depthFunc: THREE.LessDepth, depthWrite: false, opacity: 1, polygonOffset: true, polygonOffsetFactor: 1, polygonOffsetUnits: 0.5, side: THREE.DoubleSide, transparent: true } );
 +init_object(obj0);
 +scene.add(obj0);
 +
 +// COMMON_CODE_BLOCK_BEGIN
 +function textSpriteMaterial(message, parameters) {
 +    if ( parameters === undefined ) parameters = {};
 +    var fontface = "Helvetica";
 +    var fontsize = parameters.hasOwnProperty("fontsize") ? parameters["fontsize"] : 15;
 +    fontsize = fontsize*10;
 +    var lines = message.split('\\n');
 +    var size = 512;
 +    for(var i = 0; i<lines.length; i++){
 +        var tmp = lines[i].length;
 +        while(tmp*fontsize > size){
 +           fontsize--;
 +        }
 +    }
 +    
 +    var canvas = document.createElement('canvas');
 +    canvas.width = size;
 +    canvas.height = size;
 +    var context = canvas.getContext('2d');
 +    context.fillStyle = "rgba(255, 255, 255, 0)";
 +    context.fill();
 +    context.font = fontsize + "px " + fontface;
 +    
 +    // text color
 +    context.fillStyle = "rgba(0, 0, 0, 1.0)";
 +     for(var i = 0; i<lines.length; i++){
 +        context.fillText(lines[i], size/2, size/2+i*fontsize);
 +     }
 +    
 +    // canvas contents will be used for a texture
 +    var texture = new THREE.Texture(canvas);
 +    texture.needsUpdate = true;
 +    
 +    var spriteMaterial = new THREE.SpriteMaterial({map: texture, depthTest: true, depthWrite: false, polygonOffset: true, polygonOffsetFactor: -1, polygonOffsetUnits: 1 });
 +    return spriteMaterial;
 +}
 +
 +
 +// ---------------------- INITIALIZING OBJECTS--------------------------------------
 +// ---------------------------------------------------------------------------------
 +
 +function init_object(obj) {
 +    if (obj.userData.hasOwnProperty("pointmaterial")) {
 +        init_points(obj);
 +        modelContains.points = true;
 +    }
 +    if (obj.userData.hasOwnProperty("pointlabels")) {
 +        init_pointlabels(obj);
 +        modelContains.pointlabels = true;
 +    }
 +    if (obj.userData.hasOwnProperty("edgematerial")) {
 +        init_lines(obj);
 +        modelContains.lines = true;
 +    }
 +    if (obj.userData.hasOwnProperty("edgelabels")) {
 +        init_edgelabels(obj);
 +        modelContains.edgelabels = true;
 +    }
 +    if (obj.userData.hasOwnProperty("arrowstyle")) {
 +        init_arrowheads(obj);
 +        modelContains.arrowheads = true;
 +    }
 +    if (obj.userData.hasOwnProperty("facetmaterial")) {
 +        init_faces(obj);
 +        modelContains.faces = true;
 +    }
 +}
 +
 +function init_points(obj) {
 +    var pointgroup = new THREE.Group();
 +    pointgroup.name = "points";
 +    var points = obj.userData.points;
 +    var radii = obj.userData.pointradii;
 +    var materials = obj.userData.pointmaterial;
 +    var geometry,material;
 +    if (!Array.isArray(radii)) {
 +        geometry = new THREE.SphereBufferGeometry(radii);  
 +    }
 +    if (!Array.isArray(materials)) {
 +        material = materials;
 +    }
 +    for (var i=0; i<points.length; i++) {
 +        var point = points[i];
 +        if (Array.isArray(radii)) {
 +            if (radii[i] == 0) {
 +                continue;
 +            }
 +            geometry = new THREE.SphereBufferGeometry(radii[i]);  
 +        } 
 +        if (Array.isArray(materials)) {
 +            material = materials[i];     
 +        } 
 +        var sphere = new THREE.Mesh(geometry, material);
 +        point.addSphere(sphere);
 +        pointgroup.add(sphere);
 +    }
 +    obj.add(pointgroup);
 +}
 +
 +function init_pointlabels(obj) {
 +    var points = obj.userData.points;
 +    var labels = obj.userData.pointlabels;
 +    var pointlabels = new THREE.Group();
 +    pointlabels.name = "pointlabels";
 +    if (Array.isArray(labels)) {
 +        for (var i=0; i<points.length; i++) {
 +            var point = points[i];
 +            var spriteMaterial = textSpriteMaterial( labels[i] );
 +         var sprite = new THREE.Sprite(spriteMaterial);
 +            point.addLabel(sprite);
 +            pointlabels.add(sprite);
 +        }
 +    } else {
 +        var spriteMaterial = textSpriteMaterial( labels );
 +        for (var i=0; i<points.length; i++) {
 +            var point = points[i];
 +         var sprite = new THREE.Sprite(spriteMaterial);
 +            point.addLabel(sprite);
 +            pointlabels.add(sprite);
 +        }
 +    }
 +    obj.add(pointlabels);
 +}
 +
 +function init_lines(obj) {
 +    var edgeindices = obj.userData.edgeindices;
 +    var points = obj.userData.points;
 +    var materials = obj.userData.edgematerial;
 +    var geometry = new THREE.BufferGeometry();
 +    var bufarr = new Float32Array( obj.userData.edgeindices.length * 3 );
 +    var bufattr = new THREE.Float32BufferAttribute( bufarr, 3 );
 +    var geometry = new THREE.BufferGeometry();
 +    geometry.setAttribute('position', bufattr);
 +    if (Array.isArray(materials)) {     
 +        for (var i=0; i<materials.length; i++) {
 +            geometry.addGroup(2*i,2,i);
 +        }
 +    }
 +    var lines = new THREE.LineSegments(geometry, materials);
 +    lines.name = "lines";
 +    obj.add(lines);
 +    updateEdgesPosition(obj);
 +}
 +
 +function init_edgelabels(obj) {
 +    var points = obj.userData.points;
 +    var edgeindices = obj.userData.edgeindices;
 +    var labels = obj.userData.edgelabels;
 +    var edgelabels = new THREE.Group();
 +    edgelabels.name = "edgelabels";
 +    if (Array.isArray(labels)) {
 +        for (var i=0; i<edgeindices.length/2; i++) {
 +            var spriteMaterial = textSpriteMaterial( labels[i] );
 +            var sprite = new THREE.Sprite(spriteMaterial);
 +            sprite.position.copy(new THREE.Vector3().addVectors(points[edgeindices[2*i]].vector,points[edgeindices[2*i+1]].vector).multiplyScalar(0.5));
 +            edgelabels.add(sprite);
 +        }
 +    } else {
 +        var spriteMaterial = textSpriteMaterial( labels );
 +        for (var i=0; i<edgeindices.length/2; i++) {
 +            var sprite = new THREE.Sprite(spriteMaterial);
 +            sprite.position.copy(new THREE.Vector3().addVectors(points[edgeindices[2*i]].vector,points[edgeindices[2*i+1]].vector).multiplyScalar(0.5));
 +            edgelabels.add(sprite);
 +        }
 +    }
 +    obj.add(edgelabels);
 +}
 +
 +function init_arrowheads(obj) {
 +    var arrowheads = new THREE.Group();
 +    arrowheads.name = "arrowheads";
 +    var arrowstyle = obj.userData.arrowstyle;
 +    var edgeindices = obj.userData.edgeindices;
 +    var edgematerials = obj.userData.edgematerial;
 +    var points = obj.userData.points;
 +    var material;
 +    if (!Array.isArray(edgematerials)) {
 +        material = new THREE.MeshBasicMaterial( {color: edgematerials.color} );
 +    }
 +
 +    for (var i=0; i<edgeindices.length; i=i+2) {
 +        var start = points[edgeindices[i]];
 +        var end = points[edgeindices[i+1]];
 +        var dist = start.vector.distanceTo( end.vector ) - start.radius() - end.radius();
 +        if (dist <= 0) {
 +            continue;
 +        }
 +        var dir = new THREE.Vector3().subVectors(end.vector,start.vector);
 +        dir.normalize();
 +        var axis = new THREE.Vector3().set(dir.z,0,-dir.x);
 +        axis.normalize();
 +        var radians = Math.acos( dir.y );
 +        var radius = dist/25;
 +        var height = dist/5;
 +        var geometry = new THREE.ConeBufferGeometry(radius,height);
 +        var position = new THREE.Vector3().addVectors(start.vector,dir.clone().multiplyScalar(start.radius()+dist-height/2));
 +        if (Array.isArray(edgematerials)) {
 +            material = new THREE.MeshBasicMaterial( {color: edgematerials[i].color} );
 +        }
 +        var cone = new THREE.Mesh( geometry, material );
 +        cone.quaternion.setFromAxisAngle(axis,radians);;
 +        cone.position.copy(position);;
 +        arrowheads.add(cone);
 +    }
 +    obj.add(arrowheads);
 +}
 +
 +function init_faces(obj) {
 +    var points = obj.userData.points;
 +    var facets = obj.userData.facets;
 +    obj.userData.triangleindices = [];
 +    for (var i=0; i<facets.length; i++) {
 +        facet = facets[i];
 +        for (var t=0; t<facet.length-2; t++) {
 +            obj.userData.triangleindices.push(facet[0],facet[t+1],facet[t+2]);  
 +        }
 +    }
 +    var bufarr = new Float32Array( obj.userData.triangleindices.length * 3 );
 +    var bufattr = new THREE.Float32BufferAttribute(bufarr,3);
 +    
 +    var materials = obj.userData.facetmaterial;
 +    var geometry = new THREE.BufferGeometry();
 +    var frontmaterials = [];
 +    var backmaterials = [];
 +    geometry.setAttribute('position',bufattr);
 +    if (Array.isArray(materials)) {
 +        var tricount = 0;
 +        var facet;
 +        for (var i=0; i<facets.length; i++) {
 +            facet = facets[i];
 +            geometry.addGroup(tricount,(facet.length-2)*3,i);
 +            tricount += (facet.length-2)*3;
 +        }
 +        for (var j=0; j<materials.length; j++) {
 +            var fmat = materials[j].clone()
 +            fmat.side = THREE.FrontSide;
 +            frontmaterials.push(fmat);
 +            var bmat = materials[j].clone()
 +            bmat.side = THREE.BackSide;
 +            backmaterials.push(bmat);
 +            obj.userData.facetmaterial = frontmaterials.concat(backmaterials);
 +        }
 +    } else if (materials instanceof THREE.Material) {
 +        frontmaterials = materials.clone()
 +        frontmaterials.side = THREE.FrontSide;
 +        backmaterials = materials.clone()
 +        backmaterials.side = THREE.BackSide;
 +        obj.userData.facetmaterial = [frontmaterials, backmaterials];
 +    }
 +    // duplicating the object with front and back should avoid transparency issues
 +    var backmesh = new THREE.Mesh(geometry, backmaterials);
 +    // meshname is used to show/hide objects
 +    backmesh.name = "backfaces";
 +    obj.add(backmesh);
 +    var frontmesh = new THREE.Mesh(geometry, frontmaterials);
 +    frontmesh.name = "frontfaces";
 +    obj.add(frontmesh);
 +    updateFacesPosition(obj);
 +}
 +// //INITIALIZING
 +
 +
 +function updateFacesPosition(obj) {
 +    var points = obj.userData.points;
 +    var indices = obj.userData.triangleindices;
 +    var faces = obj.getObjectByName("frontfaces");
 +    var ba = faces.geometry.getAttribute("position");
 +    for (var i=0; i<indices.length; i++) {
 +        ba.setXYZ(i, points[indices[i]].vector.x, points[indices[i]].vector.y ,points[indices[i]].vector.z); 
 +    }
 +    faces.geometry.attributes.position.needsUpdate = true;
 +    
 +}
 +
 +function updateEdgesPosition(obj) {
 +    var points = obj.userData.points;
 +    var indices = obj.userData.edgeindices;
 +    var lines = obj.getObjectByName("lines");
 +    var ba = lines.geometry.getAttribute("position"); 
 +    for (var i=0; i<indices.length; i++) {
 +        ba.setXYZ(i, points[indices[i]].vector.x, points[indices[i]].vector.y ,points[indices[i]].vector.z); 
 +    }
 +    lines.geometry.attributes.position.needsUpdate = true;
 +}
 +
 +function onWindowResize() {
 +    renderer.setSize( three.clientWidth, three.clientHeight );
 +    svgRenderer.setSize( three.clientWidth, three.clientHeight );
 +    updateCamera();
 +}
 +
 +function updateCamera() {
 +    var width = three.clientWidth;
 +    var height = three.clientHeight;
 +    var aspect = width / height;
 +    if (camera.type == "OrthographicCamera") {
 +        camera.left = frustumSize * aspect / - 2;
 +        camera.right = frustumSize * aspect / 2;
 +        camera.top = frustumSize / 2;
 +        camera.bottom = - frustumSize / 2;
 +    } else if (camera.type == "PerspectiveCamera") {
 +        camera.aspect = aspect;
 +    }
 +    camera.updateProjectionMatrix();
 +}
 +
 +function changeCamera(event) {
 +    var selindex = event.currentTarget.selectedIndex;
 +    camera = cameras[selindex];
 +    control = controls[selindex];
 +    control.enabled = true; 
 +    for (var i=0; i<controls.length; i++) {
 +        if (i!=selindex) {
 +            controls[i].enabled = false;
 +        }
 +    }
 +    updateCamera();
 +}
 +
 +var camtypenode = document.getElementById('cameraType_3');
 +camtypenode.onchange = changeCamera;
 +camtypenode.dispatchEvent(new Event('change'));
 +
 +onWindowResize();
 +window.addEventListener('resize', onWindowResize);
 +
 +
 +var xRotationEnabled = false;
 +var yRotationEnabled = false;
 +var zRotationEnabled = false;
 +var rotationSpeedFactor = 1;
 +var settingsShown = false;
 +var labelsShown = true;
 +var intervals = [];
 +var timeouts = [];
 +var explodingSpeed = 0.05;
 +var explodeScale = 0.000001;
 +var XMLS = new XMLSerializer();
 +var svgElement;
 +var renderId;
 +
 +var render = function () {
 +
 + renderId = requestAnimationFrame(render);
 +
 +// comment in for automatic explosion
 +// explode(updateFactor());
 +
 +    var phi = 0.02 * rotationSpeedFactor;
 +
 +    if (xRotationEnabled) {
 +        scene.rotation.x += phi;
 +    }
 +    if (yRotationEnabled) {
 +        scene.rotation.y += phi;
 +    }
 +    if (zRotationEnabled) {
 +        scene.rotation.z += phi;
 +    }
 +
 +    control.update();
 +    renderer.render(scene, camera);
 +};
 +
 +if ( THREE.WEBGL.isWebGLAvailable() ) {
 + render();
 +} else {
 + var warning = WEBGL.getWebGLErrorMessage();
 + three.appendChild( warning );
 +}
 +    
 +function changeTransparency() {
 +    var opacity = 1-Number(event.currentTarget.value);
 +    for (var i=0; i<scene.children.length; i++) {
 +        child = scene.children[i];
 +        if ( child.userData.hasOwnProperty("facetmaterial") ) {
 +            if (Array.isArray(child.userData.facetmaterial)) {
 +                for (var j=0; j<child.userData.facetmaterial.length; j++) {
 +                    child.userData.facetmaterial[j].opacity = opacity;
 +                }
 +            } else {
 +                child.userData.facetmaterial.opacity = opacity;
 +            }    
 +        }
 +    }
 +}
 +
 +function toggleDepthWrite(event) {
 +    depthwrite = event.currentTarget.checked;
 +    for (var i=0; i<scene.children.length; i++) {
 +        child = scene.children[i];
 +        if ( child.userData.hasOwnProperty("facetmaterial") ) {
 +            if (Array.isArray(child.userData.facetmaterial)) {
 +                for (var j=0; j<child.userData.facetmaterial.length; j++) {
 +                    child.userData.facetmaterial[j].depthWrite = depthwrite;
 +                }
 +            } else {
 +                child.userData.facetmaterial.depthWrite = depthWrite;
 +            }    
 +        }
 +    }
 +}
 +
 +function changeRotationX(event){
 +    xRotationEnabled = event.currentTarget.checked;
 +}
 +
 +function changeRotationY(event){
 +    yRotationEnabled = event.currentTarget.checked;
 +}
 +
 +function changeRotationZ(event){
 +    zRotationEnabled = event.currentTarget.checked;
 +}
 +
 +
 +function changeRotationSpeedFactor(event){
 +    rotationSpeedFactor = Number(event.currentTarget.value);
 +}
 +
 +function resetScene(){
 +    scene.rotation.set(0,0,0);
 +    camera.position.set(0,0,5);
 +    camera.up.set(0,1,0);
 +}
 +
 +function showSettings(event){
 +    document.getElementById('settings_3').style.visibility = 'visible';
 +    document.getElementById('showSettingsButton_3').style.visibility = 'hidden';
 +    document.getElementById('hideSettingsButton_3').style.visibility = 'visible';
 +    settingsShown = true;
 +}
 +
 +function hideSettings(event){
 +    document.getElementById('settings_3').style.visibility = 'hidden';
 +    document.getElementById('showSettingsButton_3').style.visibility = 'visible';
 +    document.getElementById('hideSettingsButton_3').style.visibility = 'hidden';
 +    settingsShown = false;
 +}
 +
 +
 +
 +var pos = 150* Math.PI;
 +
 +function updateFactor() {
 +    pos++;
 +    return Math.sin(.01*pos)+1;
 +}
 +
 +// ------------------------ FOLDING ------------------------------------------------
 +// ---------------------------------------------------------------------------------
 +// rotate point p around axis defined by points p1 and p2 by given angle
 +function rotate(p, p1, p2, angle ){   
 +    angle = -angle;
 +    var x = p.x, y = p.y, z = p.z, 
 +    a = p1.x, b = p1.y, c = p1.z, 
 +    u = p2.x-p1.x, v = p2.y-p1.y, w = p2.z-p1.z;
 +    var result = [];
 +    var L = u*u + v*v + w*w;
 +    var sqrt = Math.sqrt;
 +    var cos = Math.cos;
 +    var sin = Math.sin;
 +
 +    result[0] = ((a*(v*v+w*w)-u*(b*v+c*w-u*x-v*y-w*z))*(1-cos(angle))+L*x*cos(angle)+sqrt(L)*(-c*v+b*w-w*y+v*z)*sin(angle))/L;
 +    result[1] = ((b*(u*u+w*w)-v*(a*u+c*w-u*x-v*y-w*z))*(1-cos(angle))+L*y*cos(angle)+sqrt(L)*(c*u-a*w+w*x-u*z)*sin(angle))/L;
 +    result[2] = ((c*(u*u+v*v)-w*(a*u+b*v-u*x-v*y-w*z))*(1-cos(angle))+L*z*cos(angle)+sqrt(L)*(-b*u+a*v-v*x+u*y)*sin(angle))/L;
 +
 +    return result;
 +}
 +
 +var fold = function(event){
 +    var obj = foldables[Number(event.currentTarget.name)];
 +    var foldvalue = Number(event.currentTarget.value);
 +    var scale = foldvalue - obj.userData.oldscale;
 +
 +    for (var j=0; j<obj.userData.axes.length; j++) {
 +        rotateVertices(obj, j, scale);
 +    }
 +    update(obj);
 +    obj.userData.oldscale += scale;
 +    lookAtBarycenter(obj);
 +}
 +
 +function lookAtBarycenter(obj){
 +    control.target = barycenter(obj);
 +}
 +
 +function barycenter(obj) {
 +    var center = new THREE.Vector3(0,0,0);
 +    var points = obj.userData.points;
 +    for (var i=0; i<points.length; i++){
 +        center.add(points[i].vector);
 +    }
 +    center.divideScalar(points.length);
 +    return center;
 +}
 +
 +function rotateVertices(obj, edge, scale) {
 +    var axes = obj.userData.axes;
 +    var subtrees = obj.userData.subtrees;
 +    var points = obj.userData.points;
 +    var angles = obj.userData.angles;
 +    if (edge < axes.length){
 +        for (var j=0; j<subtrees[edge].length; j++){
 +            var rotP = rotate(points[subtrees[edge][j]].vector, points[axes[edge][0]].vector,points[axes[edge][1]].vector, scale * (Math.PI - angles[edge]));
 +            points[subtrees[edge][j]].set(rotP[0],rotP[1],rotP[2]);
 +        }
 +    }
 +}
 +
 +function update(obj) {
 +   updateFacesPosition(obj);
 +   updateEdgesPosition(obj);
 +}
 +
 +if (foldables.length) {
 +    var settings = document.getElementById('settings_3');
 +    var foldDiv = document.createElement('div');
 +    foldDiv.id = 'fold_3';
 +    var title = document.createElement('strong');
 +    title.innerHTML = 'Fold';
 +    foldDiv.appendChild(title);
 +    foldDiv.className = 'group';
 +    for (var i=0; i<foldables.length; i++) {
 +        var range = document.createElement('input');
 +        range.type = 'range';
 +        range.min = 0;
 +        range.max = 1;
 +        range.value = 0;
 +        range.step = 0.001;
 +        range.name = String(i);
 +        range.oninput = fold;
 +        foldDiv.appendChild(range);
 +    }
 +    lookAtBarycenter(foldables[0]);
 +    settings.insertBefore(foldDiv,settings.childNodes[0]);
 +}
 +
 +    
 +// ---------------------- EXPLOSION ------------------------------------------------
 +// ---------------------------------------------------------------------------------
 +
 +if (explodableModel) {
 +    for (var i=0; i<scene.children.length; i++) {
 +        obj = scene.children[i];
 +        if ( obj.userData.explodable ) {
 +            computeCentroid(obj);
 +        }
 +    }
 +    document.getElementById('explodeRange_3').oninput = triggerExplode;
 +    document.getElementById('explodeCheckbox_3').onchange = triggerAutomaticExplode;
 +    document.getElementById('explodingSpeedRange_3').oninput = setExplodingSpeed;
 +    explode(0.000001);
 +}
 +
 +function computeCentroid(obj) {
 +    centroid = new THREE.Vector3();
 +    obj.userData.points.forEach(function(pmpoint) {
 +        centroid.add(pmpoint.vector);
 +    });
 +    centroid.divideScalar(obj.userData.points.length);
 +    obj.userData.centroid = centroid;
 +}
 +
 +function explode(factor) {
 +    for (var i=0; i<scene.children.length; i++) {
 +        var obj = scene.children[i];
 +        if (obj.userData.hasOwnProperty("centroid")) { 
 +            var c = obj.userData.centroid;
 +            obj.position.set(c.x*factor, c.y*factor, c.z*factor);
 +        }
 +    }
 +}
 +
 +function triggerExplode(event){
 +    explodeScale = Number(event.currentTarget.value);
 +    explode(explodeScale);
 +}
 +
 +function setExplodingSpeed(event){
 +    explodingSpeed = Number(event.currentTarget.value);
 +}
 +
 +function triggerAutomaticExplode(event){
 +    if (event.currentTarget.checked){
 +        startExploding();
 +    } else {
 +        clearIntervals();
 +    }
 +}
 +
 +function startExploding(){
 +    intervals.push(setInterval(explodingInterval, 25));
 +}
 +
 +
 +function explodingInterval(){
 +    explodeScale += explodingSpeed;
 +    if (explodeScale <= 6){ 
 +        explode(explodeScale);
 +    }
 +    else{
 +        explode(6);
 +        explodeScale = 6;
 +        clearIntervals();
 +        timeouts.push(setTimeout(startUnexploding, 3000));
 +    }
 +    document.getElementById('explodeRange_3').value = explodeScale;
 +}
 +
 +
 +function startUnexploding(){
 +    intervals.push(setInterval(unexplodingInterval, 25));
 +}
 +
 +function unexplodingInterval(){
 +    explodeScale -= explodingSpeed;
 +    if (explodeScale >= 0){
 +        explode(explodeScale);
 +    }
 +    else {
 +        explode(0);
 +        explodeScale = 0;
 +        clearIntervals();
 +        timeouts.push(setTimeout(startExploding, 3000));
 +    }
 +    document.getElementById('explodeRange_3').value = explodeScale;
 +}
 +
 +function clearIntervals(){
 +    intervals.forEach(function(interval){
 +        clearInterval(interval);
 +    });
 +    intervals = [];
 +    timeouts.forEach(function(timeout){
 +        clearTimeout(timeout);
 +    });
 +    timeouts = [];
 +}
 +
 +// ---------------------- DISPLAY --------------------------------------------------
 +// ---------------------------------------------------------------------------------
 +
 +const objectTypeInnerHTMLs = { points: "Points", pointlabels: "Point labels", lines: "Edges", edgelabels: "Edge labels", faces: "Faces", arrowheads: "Arrow heads" };
 +const objectTypeVisible = {};
 +Object.assign(objectTypeVisible,modelContains);
 +const sortedObjectTypeKeys = Object.keys(objectTypeInnerHTMLs).sort();
 +const shownObjectTypesList = document.getElementById('shownObjectTypesList_3');
 +
 +function setVisibility(bool,objname) {
 +    for (var i=0; i<scene.children.length; i++){
 +        var obj = scene.children[i].getObjectByName(objname);
 +        if (obj) {
 +            obj.visible = bool;
 +        }
 +    }
 +}
 +
 +function toggleObjectTypeVisibility(event){
 +    var name = event.currentTarget.name;
 +    var checked = event.currentTarget.checked;
 +    objectTypeVisible[name] = checked;
 +    if (name == "faces") {
 +        setVisibility(checked,"frontfaces");
 +        setVisibility(checked,"backfaces");
 +    } else {
 +        setVisibility(checked,name);
 +    }
 +}
 +
 +for (var i=0; i<sortedObjectTypeKeys.length; i++){
 +    var key = sortedObjectTypeKeys[i];
 +    if (modelContains[key]) {
 +        var objTypeNode = document.createElement('span');
 +        objTypeNode.innerHTML = objectTypeInnerHTMLs[key] + '<br>';
 +        var checkbox = document.createElement('input');
 +        checkbox.type = 'checkbox';
 +        checkbox.checked = true;
 +        checkbox.name = key;
 +        checkbox.onchange = toggleObjectTypeVisibility;
 +        shownObjectTypesList.appendChild(checkbox);
 +        shownObjectTypesList.appendChild(objTypeNode);
 +    }
 +}
 +
 +// ------------------------------------------------------
 +
 +function toggleObjectVisibility(event){
 +    var nr = Number(event.currentTarget.name);
 +    scene.children[nr].visible = event.currentTarget.checked;
 +}
 +
 +// append checkboxes for displaying or hiding objects
 +var shownObjectsList = document.getElementById('shownObjectsList_3');
 +for (var i=0; i<scene.children.length; i++){
 +    obj = scene.children[i];
 +    var objNode = document.createElement('span');
 +    objNode.innerHTML = obj.name + '<br>';
 +    var checkbox = document.createElement('input');
 +    checkbox.type = 'checkbox';
 +    checkbox.checked = true;
 +    checkbox.name = String(i);
 +    checkbox.onchange = toggleObjectVisibility;
 +    shownObjectsList.appendChild(checkbox);
 +    shownObjectsList.appendChild(objNode);
 +}
 +
 +// ---------------------- SVG ------------------------------------------------------
 +// ---------------------------------------------------------------------------------
 +
 +function takeSvgScreenshot() {
 +    if (objectTypeVisible["pointlabels"]) {
 +        setVisibility(false,"pointlabels");
 +    }
 +    if (objectTypeVisible["edgelabels"]) {
 +        setVisibility(false,"edgelabels");
 +    }
 +    svgRenderer.render(scene,camera);
 +    svgElement = XMLS.serializeToString(svgRenderer.domElement);
 +    
 +    if (objectTypeVisible["pointlabels"]) {
 +        setVisibility(true,"pointlabels");
 +    }
 +    if (objectTypeVisible["edgelabels"]) {
 +        setVisibility(true,"edgelabels");
 +    }
 +
 +    if (document.getElementById('tab_3').checked){
 +        //show in new tab
 +        var myWindow = window.open("","");
 +        myWindow.document.body.innerHTML = svgElement;
 +    } else{
 +        // download svg file 
 +        download("screenshot.svg", svgElement);
 +    }
 +}
 +
 +function download(filename, text) {
 +    var element = document.createElement('a');
 +    element.setAttribute('href', 'data:text/plain;charset=utf-8,' + encodeURIComponent(text));
 +    element.setAttribute('download', filename);
 +
 +    element.style.display = 'none';
 +    document.body.appendChild(element);
 +
 +    element.click();
 +
 +    document.body.removeChild(element);
 +}
 +
 +
 +document.getElementById('transparencyRange_3').oninput = changeTransparency;
 +document.getElementById('depthWriteCheckbox_3').onchange = toggleDepthWrite;
 +document.getElementById('changeRotationX_3').onchange = changeRotationX;
 +document.getElementById('changeRotationY_3').onchange = changeRotationY;
 +document.getElementById('changeRotationZ_3').onchange = changeRotationZ;
 +document.getElementById('resetButton_3').onclick = resetScene;
 +document.getElementById('rotationSpeedRange_3').oninput = changeRotationSpeedFactor;
 +document.getElementById('takeScreenshot_3').onclick = takeSvgScreenshot;
 +document.getElementById('showSettingsButton_3').onclick = showSettings;
 +document.getElementById('hideSettingsButton_3').onclick = hideSettings;
 +
 +
 +// ------------------ SHORTCUTS --------------------------------------------
 +// -------------------------------------------------------------------------
 +
 +/**
 + * http://www.openjs.com/scripts/events/keyboard_shortcuts/
 + * Version : 2.01.B
 + * By Binny V A
 + * License : BSD
 + */
 +shortcut = {
 + 'all_shortcuts':{},//All the shortcuts are stored in this array
 + 'add': function(shortcut_combination,callback,opt) {
 + //Provide a set of default options
 + var default_options = {
 + 'type':'keydown',
 + 'propagate':false,
 + 'disable_in_input':false,
 + 'target':document,
 + 'keycode':false
 + }
 + if(!opt) opt = default_options;
 + else {
 + for(var dfo in default_options) {
 + if(typeof opt[dfo] == 'undefined') opt[dfo] = default_options[dfo];
 + }
 + }
 +
 + var ele = opt.target;
 + if(typeof opt.target == 'string') ele = document.getElementById(opt.target);
 + var ths = this;
 + shortcut_combination = shortcut_combination.toLowerCase();
 +
 + //The function to be called at keypress
 + var func = function(e) {
 + e = e || window.event;
 +
 + if(opt['disable_in_input']) { //Don't enable shortcut keys in Input, Textarea fields
 + var element;
 + if(e.target) element=e.target;
 + else if(e.srcElement) element=e.srcElement;
 + if(element.nodeType==3) element=element.parentNode;
 +
 + if(element.tagName == 'INPUT' || element.tagName == 'TEXTAREA') return;
 + }
 +
 + //Find Which key is pressed
 + if (e.keyCode) code = e.keyCode;
 + else if (e.which) code = e.which;
 + var character = String.fromCharCode(code).toLowerCase();
 +
 + if(code == 188) character=","; //If the user presses , when the type is onkeydown
 + if(code == 190) character="."; //If the user presses , when the type is onkeydown
 +
 + var keys = shortcut_combination.split("+");
 + //Key Pressed - counts the number of valid keypresses - if it is same as the number of keys, the shortcut function is invoked
 + var kp = 0;
 +
 + //Work around for stupid Shift key bug created by using lowercase - as a result the shift+num combination was broken
 + var shift_nums = {
 + "`":"~",
 + "1":"!",
 + "2":"@",
 + "3":"#",
 + "4":"$",
 + "5":"%",
 + "6":"^",
 + "7":"&",
 + "8":"*",
 + "9":"(",
 + "0":")",
 + "-":"_",
 + "=":"+",
 + ";":":",
 + "'":"\"",
 + ",":"<",
 + ".":">",
 + "/":"?",
 + "\\":"|"
 + }
 + //Special Keys - and their codes
 + var special_keys = {
 + 'esc':27,
 + 'escape':27,
 + 'tab':9,
 + 'space':32,
 + 'return':13,
 + 'enter':13,
 + 'backspace':8,
 +
 + 'scrolllock':145,
 + 'scroll_lock':145,
 + 'scroll':145,
 + 'capslock':20,
 + 'caps_lock':20,
 + 'caps':20,
 + 'numlock':144,
 + 'num_lock':144,
 + 'num':144,
 +
 + 'pause':19,
 + 'break':19,
 +
 + 'insert':45,
 + 'home':36,
 + 'delete':46,
 + 'end':35,
 +
 + 'pageup':33,
 + 'page_up':33,
 + 'pu':33,
 +
 + 'pagedown':34,
 + 'page_down':34,
 + 'pd':34,
 +
 + 'left':37,
 + 'up':38,
 + 'right':39,
 + 'down':40,
 +
 + 'f1':112,
 + 'f2':113,
 + 'f3':114,
 + 'f4':115,
 + 'f5':116,
 + 'f6':117,
 + 'f7':118,
 + 'f8':119,
 + 'f9':120,
 + 'f10':121,
 + 'f11':122,
 + 'f12':123
 + }
 +
 + var modifiers = { 
 + shift: { wanted:false, pressed:false},
 + ctrl : { wanted:false, pressed:false},
 + alt  : { wanted:false, pressed:false},
 + meta : { wanted:false, pressed:false} //Meta is Mac specific
 + };
 +                        
 + if(e.ctrlKey) modifiers.ctrl.pressed = true;
 + if(e.shiftKey) modifiers.shift.pressed = true;
 + if(e.altKey) modifiers.alt.pressed = true;
 + if(e.metaKey)   modifiers.meta.pressed = true;
 +                        
 + for(var i=0; k=keys[i],i<keys.length; i++) {
 + //Modifiers
 + if(k == 'ctrl' || k == 'control') {
 + kp++;
 + modifiers.ctrl.wanted = true;
 +
 + } else if(k == 'shift') {
 + kp++;
 + modifiers.shift.wanted = true;
 +
 + } else if(k == 'alt') {
 + kp++;
 + modifiers.alt.wanted = true;
 + } else if(k == 'meta') {
 + kp++;
 + modifiers.meta.wanted = true;
 + } else if(k.length > 1) { //If it is a special key
 + if(special_keys[k] == code) kp++;
 +
 + } else if(opt['keycode']) {
 + if(opt['keycode'] == code) kp++;
 +
 + } else { //The special keys did not match
 + if(character == k) kp++;
 + else {
 + if(shift_nums[character] && e.shiftKey) { //Stupid Shift key bug created by using lowercase
 + character = shift_nums[character]; 
 + if(character == k) kp++;
 + }
 + }
 + }
 + }
 +
 + if(kp == keys.length && 
 + modifiers.ctrl.pressed == modifiers.ctrl.wanted &&
 + modifiers.shift.pressed == modifiers.shift.wanted &&
 + modifiers.alt.pressed == modifiers.alt.wanted &&
 + modifiers.meta.pressed == modifiers.meta.wanted) {
 + callback(e);
 +
 + if(!opt['propagate']) { //Stop the event
 + //e.cancelBubble is supported by IE - this will kill the bubbling process.
 + e.cancelBubble = true;
 + e.returnValue = false;
 +
 + //e.stopPropagation works in Firefox.
 + if (e.stopPropagation) {
 + e.stopPropagation();
 + e.preventDefault();
 + }
 + return false;
 + }
 + }
 + }
 + this.all_shortcuts[shortcut_combination] = {
 + 'callback':func, 
 + 'target':ele, 
 + 'event': opt['type']
 + };
 + //Attach the function with the event
 + if(ele.addEventListener) ele.addEventListener(opt['type'], func, false);
 + else if(ele.attachEvent) ele.attachEvent('on'+opt['type'], func);
 + else ele['on'+opt['type']] = func;
 + },
 +
 + //Remove the shortcut - just specify the shortcut and I will remove the binding
 + 'remove':function(shortcut_combination) {
 + shortcut_combination = shortcut_combination.toLowerCase();
 + var binding = this.all_shortcuts[shortcut_combination];
 + delete(this.all_shortcuts[shortcut_combination])
 + if(!binding) return;
 + var type = binding['event'];
 + var ele = binding['target'];
 + var callback = binding['callback'];
 +
 + if(ele.detachEvent) ele.detachEvent('on'+type, callback);
 + else if(ele.removeEventListener) ele.removeEventListener(type, callback, false);
 + else ele['on'+type] = false;
 + }
 +}
 +
 +shortcut.add("Alt+Left",function() {
 + var event = new Event('click');
 + if (settingsShown){
 + document.getElementById('hideSettingsButton_3').dispatchEvent(event);
 + } else {
 + document.getElementById('showSettingsButton_3').dispatchEvent(event);
 + }
 +});
 +
 +
 +// COMMON_CODE_BLOCK_END
 +
 +});});
 +      </script>
 +   </body>
 +</html>
 +</HTML>
 +Hence the LP attains its maximal value 2 on the 2-face spanned by the vertices 6, 9 and 10.
 +
 +''%%polymake%%'' can visualise the polytope and highlight both its maximal and minimal face in a different (by default admittedly almost painful ;-) ) colour. Here you see the maximal face ''%%{6 9 10}%%'' in red and the minimal face ''%%{0 3}%%'' (on the opposite side of the polytope) in yellow.
 +
 +Note though that since we started out with a random polytope these results may vary if we perform the same computations another time on a different random polytope.
 +
 +<code perl>
 +> print $ilp->VERTICES;
 +1 -1 -1 -1
 +1 -1 -1 0
 +1 -1 0 1
 +1 -1 1 0
 +1 -1 1 1
 +1 0 -1 0
 +1 0 -1 1
 +1 0 1 -1
 +1 1 0 0
 +1 1 0 1
 +1 1 1 -1
 +1 1 1 1
 +</code>
 +==== Hilbert bases ====
 +
 +Finally, we can have ''%%polymake%%'' compute and print a Hilbert basis for the cone spanned by ''%%$ilp%%''. Notice that this requires normaliz or 4ti2 to be installed in order to work.
 +
 +<code perl>
 +> print $ilp->HILBERT_BASIS;
 +1 -1 -1 -1
 +1 -1 -1 0
 +1 -1 0 0
 +1 -1 0 1
 +1 -1 1 0
 +1 -1 1 1
 +1 0 -1 0
 +1 0 -1 1
 +1 0 0 -1
 +1 0 0 0
 +1 0 0 1
 +1 0 1 -1
 +1 0 1 0
 +1 0 1 1
 +1 1 0 0
 +1 1 0 1
 +1 1 1 -1
 +1 1 1 0
 +1 1 1 1
 +</code>