+ },
+ makeSrcFile: function(sourceFile)
+ {
+ // this stuff works...
+ return;
+
+
+ name = sourceFile.substring(Options.baseDir.length+1);
+ name = name.replace(/\.\.?[\\\/]/g, "").replace(/[\\\/]/g, "_");
+
+ name = name.replace(/\:/g, "_"); //??
+
+ Options.LOG.inform("Write Source file : " + Options.target+"/symbols/src/" + name);
+ var pretty = imports.PrettyPrint.toPretty(File.read(sourceFile));
+ File.write(Options.target+"/symbols/src/" + name,
+ '<html><head>' +
+ '<title>' + sourceFile + '</title>' +
+ '<link rel="stylesheet" type="text/css" href="../../../highlight-js.css"/>' +
+ '</head><body class="highlightpage">' +
+ pretty +
+ '</body></html>');