From 262fdd3a0a12aeaf0659b37cbeca9eacaeb43ffd Mon Sep 17 00:00:00 2001 From: Steven Hugg Date: Wed, 16 Sep 2026 16:16:07 +0200 Subject: [PATCH] ui: gutter styles moved to css/ui.css --- css/ui.css | 39 +++++++++++++++++++++++++++++++++++++++ src/ide/views/gutter.ts | 35 ++++++----------------------------- 2 files changed, 45 insertions(+), 29 deletions(-) diff --git a/css/ui.css b/css/ui.css index d4d03531..06643b54 100644 --- a/css/ui.css +++ b/css/ui.css @@ -1361,3 +1361,42 @@ div.scripting-cell button.scripting-enabled { margin-top: 0.8em; line-height: 1.4; } +/* CodeMirror gutter markers */ +.gutter-offset-marker { + cursor: pointer; +} +.gutter-offset-marker:hover { + text-decoration: underline; +} +.gutter-breakpoint, +.gutter-breakpoint-placeholder { + cursor: pointer; +} +.gutter-breakpoint-enabled { + color: rgba(255, 0, 0, 1.0); +} +.gutter-breakpoint-disabled { + color: rgba(255, 255, 255, 0.35); +} +.gutter-breakpoint-placeholder { + color: transparent; +} +.gutter-breakpoint-placeholder:hover { + color: rgba(255, 0, 0, 0.5); +} +.gutter-error { + color: #ff6666; + font-weight: bold; + cursor: pointer; +} +.gutter-currentpc { + color: #ff66ee; + cursor: pointer; +} +.gutter-currentpc-placeholder { + color: transparent; + cursor: pointer; +} +.gutter-currentpc-placeholder:hover { + color: #ffee66; +} diff --git a/src/ide/views/gutter.ts b/src/ide/views/gutter.ts index 9b36813f..9f2ec5d6 100644 --- a/src/ide/views/gutter.ts +++ b/src/ide/views/gutter.ts @@ -145,15 +145,9 @@ class OffsetMarker extends GutterMarker { constructor(readonly hex: string) { super(); } toDOM() { const span = document.createElement("span"); + span.className = "gutter-offset-marker"; span.textContent = this.hex; - span.style.cursor = "pointer"; span.title = "Click to run to here"; - span.addEventListener("mouseenter", () => { - span.style.textDecoration = "underline"; - }); - span.addEventListener("mouseleave", () => { - span.style.textDecoration = "none"; - }); return span; } eq(other: OffsetMarker) { return this.hex == other.hex; } @@ -174,15 +168,8 @@ class ClockMarker extends GutterMarker { const BREAKPOINT_PLACEHOLDER_MARKER = new class extends GutterMarker { toDOM() { const span = document.createElement("span"); + span.className = "gutter-breakpoint-placeholder"; span.textContent = "●"; - span.style.color = "transparent"; - span.style.cursor = "pointer"; - span.addEventListener("mouseenter", () => { - span.style.color = "rgba(255, 0, 0, 0.5)"; - }); - span.addEventListener("mouseleave", () => { - span.style.color = "transparent"; - }); return span; } }; @@ -191,9 +178,8 @@ class BreakpointMarker extends GutterMarker { constructor(readonly enabled: boolean) { super(); } toDOM() { const span = document.createElement("span"); + span.className = "gutter-breakpoint " + (this.enabled ? "gutter-breakpoint-enabled" : "gutter-breakpoint-disabled"); span.innerHTML = "●"; - span.style.color = this.enabled ? "rgba(255, 0, 0, 1.0)" : "rgba(255, 255, 255, 0.35)"; - span.style.cursor = "pointer"; span.title = this.enabled ? "Breakpoint (click to remove; manage in Breakpoints window)" : "Disabled breakpoint (click to remove)"; return span; } @@ -208,9 +194,8 @@ class ErrorMarker extends GutterMarker { toDOM() { const span = document.createElement("span"); + span.className = "gutter-error"; span.innerHTML = "ⓧ"; - span.style.color = "red"; - span.style.cursor = "pointer"; span.title = this.msg; return span; } @@ -220,16 +205,9 @@ class ErrorMarker extends GutterMarker { const CURRENT_PC_PLACEHOLDER_MARKER = new class extends GutterMarker { toDOM() { const span = document.createElement("span"); + span.className = "gutter-currentpc-placeholder"; span.textContent = "▶"; - span.style.color = "transparent"; - span.style.cursor = "pointer"; span.title = "Click to run to here"; - span.addEventListener("mouseenter", () => { - span.style.color = "#ffee66"; - }); - span.addEventListener("mouseleave", () => { - span.style.color = "transparent"; - }); return span; } }; @@ -237,9 +215,8 @@ const CURRENT_PC_PLACEHOLDER_MARKER = new class extends GutterMarker { const CURRENT_PC_MARKER = new class extends GutterMarker { toDOM() { const span = document.createElement("span"); + span.className = "gutter-currentpc"; span.innerHTML = "▶"; - span.style.color = "#ff66ee"; - span.style.cursor = "pointer"; span.title = "Current PC"; return span; }