if (fileName.indexOf ("//") < 0) fileName = "file://" + fileName;
return new java.io.BufferedReader ( new java.io.InputStreamReader ( new java.net.URL (fileName).openStream ()));
}, "~S,~B");
+Clazz.defineStatics (c$,
+"TCOFFEE_SCORE", "TCoffeeScore",
+"Phylip_FILE", 1,
+"Phylip_FILE_EXT", "phy",
+"Phylip_FILE_DESC", "PHYLIP",
+"JSON_FILE", 2,
+"JSON_FILE_EXT", "json",
+"JSON_FILE_DESC", "JSON",
+"Html_FILE", 3,
+"Html_FILE_EXT", "html",
+"Html_FILE_DESC", "HTML");
});