ui: gutter styles moved to css/ui.css

This commit is contained in:
Steven Hugg committed 2026-09-16 16:16:07 +02:00
1 parent a69ee89077
commit 262fdd3a0a
2 files changed
+45 -29

No files matched your search

+39
View File
@@ -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;
}
+6 -29
View File
@@ -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;
}