'use strict'; var Typed = {}; Typed.DEVMODE = false; // Note: This demo page must be located in either of the two directories: // demos/typed and docs/. The DEVMODE must be enabled if this page exists in // the first one. Otherwise, it must be disabled. Typed.SCRIPTS_FOR_DEV = [ "../../blockly_uncompressed.js", "../../blocks/lists.js", "../../blocks/typed_blocks.js", "../../blocks/parameters.js", "../../blocks/datatypes.js", "../../generators/typedlang.js", "../../generators/typedlang/blocks.js", "../../msg/js/ja.js", "../../block_of_ocaml/converter.js", "../../block_of_ocaml/utils.js", "../codemirror/lib/codemirror.js", "../codemirror/mode/mllike/mllike.js", "../codemirror/addon/runmode/runmode.js", "eval.js", ]; Typed.SCRIPTS_FOR_PROD = [ "base.js", "blockly_compressed.js", "blocks_compressed.js", "typedlang_compressed.js", "en.js", "ja.js", "converter.js", "block_of_ocaml_utils.js", "eval.js", ]; Typed.BOOT = (function() { var scripts = document.getElementsByTagName('script'); var re = new RegExp('(.+)[\/]typed\.js$'); var dir; for (var i = 0, script; script = scripts[i]; i++) { var match = re.exec(script.src); if (match) { dir = match[1]; } } if (!dir) { alert('Could not detect the directory name.'); return; } var scripts = Typed.DEVMODE ? Typed.SCRIPTS_FOR_DEV : Typed.SCRIPTS_FOR_PROD; for (var i = 0, src; src = scripts[i]; i++) { document.write( '