// animation
function get_anim_keys() = [
0, // initial
0.1, // resting
0.25, // holodisk free-inserted
0.3, // holodisk click-inserted
0.4, // laser raised
0.5, // start playing
0.7, // stop playing, start lowering laser
0.8, // laser lowered, holodisk removing
0.85, // holodisk click-removed
1 // final, holodisk free-removed
];

function ANIM_START()=0;
function ANIM_RESTING()=0;
function ANIM_INSERTING()=1;
function ANIM_OPENING()=2;
function ANIM_RAISING()=3;
function ANIM_PLAYING()=4;
function ANIM_LOWERING()=5;
function ANIM_CLOSING()=6;
function ANIM_REMOVING()=7;
function ANIM_END()=8;

function anim(key_from, key_to, KEYS=get_anim_keys())
    = max(0, min(($t - KEYS[key_from]) / (KEYS[key_to] - KEYS[key_from]), 1));