You can not select more than 25 topics Topics must start with a letter or number, can include dashes ('-') and can be up to 35 characters long.

71 lines
2.1 KiB

  1. function noFormat() {
  2. let elements: Array<string> = [
  3. "remove_comments",
  4. "remove_lines",
  5. "remove_report",
  6. "check_alias",
  7. "sign_align_in",
  8. "sign_align_port",
  9. "sign_align_generic",
  10. "sign_align_function",
  11. "sign_align_procedure",
  12. "sign_align_all",
  13. "new_line_after",
  14. "use_space",
  15. "customise_indentation",
  16. "compress",
  17. "mix_letter",
  18. "cust_eol"
  19. ];
  20. var isDisabled = getHTMLInputElement("no_format").checked;
  21. elements.forEach(element => {
  22. var htmlElement = getHTMLInputElement(element + "_div");
  23. try {
  24. getHTMLInputElement(element).disabled = isDisabled;
  25. }
  26. catch{ }
  27. if (isDisabled) {
  28. htmlElement.className += " disabled";
  29. }
  30. else {
  31. htmlElement.className = htmlElement.className.replace(/\bdisabled\b/g, "");
  32. }
  33. });
  34. let radioButtons = <HTMLCollectionOf<HTMLInputElement>>document.getElementsByTagName("input");
  35. for (let i = 0; i < radioButtons.length; i++) {
  36. if ((<HTMLInputElement>radioButtons[i]).type == "radio") {
  37. (<HTMLInputElement>radioButtons[i]).disabled = isDisabled;
  38. }
  39. }
  40. }
  41. function getHTMLInputElement(id: string): HTMLInputElement {
  42. return <HTMLInputElement>document.getElementById(id);
  43. }
  44. function Compress(input: string) {
  45. input = input.replace(/\r\n/g, '');
  46. input = input.replace(/[\t ]+/g, ' ');
  47. input = input.replace(/[ ]?([&=:\-<>\+|])[ ]?/g, '$1');
  48. return input;
  49. }
  50. function MixLetters(input: string) {
  51. let arr = input.split("");
  52. for (var k = 0; k < arr.length; k++) {
  53. if (arr[k] === arr[k].toUpperCase() && Math.random() > 0.5) {
  54. arr[k] = arr[k].toLowerCase();
  55. } else if (Math.random() > 0.5) {
  56. arr[k] = arr[k].toUpperCase();
  57. }
  58. }
  59. return arr.join("");
  60. }
  61. function wordWrap() {
  62. var d = document.getElementById("result");
  63. if (d.className == "") {
  64. d.className = "wordwrap";
  65. } else {
  66. d.className = "";
  67. }
  68. }