From 8a225f0a993863861b9a0684aa363865fa07d7bf Mon Sep 17 00:00:00 2001
From: Maxime Jacquemin <maxime.jacquemin@cea.fr>
Date: Tue, 23 Jul 2024 12:24:22 +0200
Subject: [PATCH] [Ivette] Status bullets styles as CSS
Using CSS for status bullets styles allow to specifies colors based on
the current theme. Also, it's ugly to write the style in the typescript
code.
---
ivette/src/dome/renderer/dark.css | 15 ++++++
ivette/src/dome/renderer/light.css | 15 ++++++
ivette/src/frama-c/kernel/ASTview.tsx | 45 ++----------------
ivette/src/frama-c/kernel/style.css | 67 +++++++++++++++++++++++++--
4 files changed, 96 insertions(+), 46 deletions(-)
diff --git a/ivette/src/dome/renderer/dark.css b/ivette/src/dome/renderer/dark.css
index 21ac1aabece..31e009d27d3 100644
--- a/ivette/src/dome/renderer/dark.css
+++ b/ivette/src/dome/renderer/dark.css
@@ -109,5 +109,20 @@
--codemirror-number: #d3869b;
--codemirror-keyword: #d84954;
--codemirror-def: #94aadd;
+
+ --status-dead : #000000;
+ --status-valid : #499E00;
+ --status-invalid: #FF0000;
+ --status-unknown: #FFE62E;
+ --status-never-tried: #FFFFFF;
+ --status-inconsistent: #FF00FF;
+
+ --status-valid-but-dead: linear-gradient(to right, var(--status-valid) 49%, var(--status-dead) 51%);
+ --status-invalid-but-dead: linear-gradient(to right, var(--status-invalid) 49%, var(--status-dead) 51%);
+ --status-unknown-but-dead: linear-gradient(to right, var(--status-unknown) 49%, var(--status-dead) 51%);
+
+ --status-valid-under-hyp: linear-gradient(to right, var(--status-valid) 49%, var(--status-unknown) 51%);
+ --status-considered-valid: linear-gradient(to right, var(--status-valid) 49%, #73BBBB 51%);
+ --status-invalid-under-hyp: linear-gradient(to right, var(--status-invalid) 49%, var(--status-unknown) 51%);
}
}
diff --git a/ivette/src/dome/renderer/light.css b/ivette/src/dome/renderer/light.css
index e9f6bd28b85..732c57a2427 100644
--- a/ivette/src/dome/renderer/light.css
+++ b/ivette/src/dome/renderer/light.css
@@ -109,5 +109,20 @@
--codemirror-number: #116644;
--codemirror-keyword: #770088;
--codemirror-def: #0000ff;
+
+ --status-dead : #000000;
+ --status-valid : #499E00;
+ --status-invalid: #FF0000;
+ --status-unknown: #FFE62E;
+ --status-never-tried: #FFFFFF;
+ --status-inconsistent: #FF00FF;
+
+ --status-valid-but-dead: linear-gradient(to right, var(--status-valid) 49%, var(--status-dead) 51%);
+ --status-invalid-but-dead: linear-gradient(to right, var(--status-invalid) 49%, var(--status-dead) 51%);
+ --status-unknown-but-dead: linear-gradient(to right, var(--status-unknown) 49%, var(--status-dead) 51%);
+
+ --status-valid-under-hyp: linear-gradient(to right, var(--status-valid) 49%, var(--status-unknown) 51%);
+ --status-considered-valid: linear-gradient(to right, var(--status-valid) 49%, #73BBBB 51%);
+ --status-invalid-under-hyp: linear-gradient(to right, var(--status-invalid) 49%, var(--status-unknown) 51%);
}
}
diff --git a/ivette/src/frama-c/kernel/ASTview.tsx b/ivette/src/frama-c/kernel/ASTview.tsx
index 62dfb6b733e..598da566ec0 100644
--- a/ivette/src/frama-c/kernel/ASTview.tsx
+++ b/ivette/src/frama-c/kernel/ASTview.tsx
@@ -432,31 +432,6 @@ function createPropertiesNodes(): Editor.Aspect<Property[]> {
});
}
-// Bullet colors.
-function getBulletColors(status: States.Tag): [string, string] {
- const yellow = '#FFE62E';
- const red = '#FF0000';
- const blue = '#73bbbb';
- const green = '#499E00';
- const black = '#000000';
- const white = '#FFFFFF';
- const magenta = '#FF00FF';
- switch (status.name) {
- case 'unknown': return [yellow, yellow];
- case 'invalid': return [red, red];
- case 'invalid_under_hyp': return [red, yellow];
- case 'valid': return [green, green];
- case 'valid_under_hyp': return [green, yellow];
- case 'considered_valid': return [green, blue];
- case 'invalid_but_dead': return [red, black];
- case 'valid_but_dead': return [green, black];
- case 'unknown_but_dead': return [yellow, black];
- case 'never_tried': return [white, white];
- case 'inconsistent': return [magenta, magenta];
- default: return [yellow, yellow];
- }
-}
-
// Property bullet gutter marker.
class PropertyBullet extends Editor.GutterMarker {
readonly bullet: HTMLDivElement;
@@ -464,22 +439,10 @@ class PropertyBullet extends Editor.GutterMarker {
constructor(status?: States.Tag) {
super();
this.bullet = document.createElement('div');
- this.bullet.innerHTML = ' ';
- if (status) {
- const [bulletColorLeft, bulletColorRight] = getBulletColors(status);
- this.bullet.style.width = "60%";
- this.bullet.style.aspectRatio = "1 / 1";
- this.bullet.style.textAlign = 'center';
- const bulletGradient =
- bulletColorLeft + ' 49%, ' + bulletColorRight + ' 51%';
- this.bullet.style.background =
- 'linear-gradient(to right, ' + bulletGradient + ')';
- this.bullet.style.borderRadius = '50%';
- this.bullet.style.border = '0.5px solid rgba(0, 0, 0, 0.5)';
- this.bullet.style.marginLeft = '20%';
- this.bullet.style.marginTop = '25%';
- if (status.descr) this.bullet.title = status.descr;
- }
+ this.bullet.classList.add('bullet');
+ if (!status) return;
+ this.bullet.classList.add(status.name);
+ if (status.descr) this.bullet.title = status.descr;
}
}
diff --git a/ivette/src/frama-c/kernel/style.css b/ivette/src/frama-c/kernel/style.css
index db351090b3f..919c90022b7 100644
--- a/ivette/src/frama-c/kernel/style.css
+++ b/ivette/src/frama-c/kernel/style.css
@@ -50,16 +50,73 @@
border-bottom: solid 0.2em var(--non-terminating);
}
-.bullet {
- width: 1.5em;
- background: var(--code-bullet);
-}
-
/* More contrasted color for thinner icons. */
.titlebar-thin-icon {
fill: var(--text);
}
+/* -------------------------------------------------------------------------- */
+/* --- Status Bullets --- */
+/* -------------------------------------------------------------------------- */
+
+.bullet {
+ width: 60%;
+ aspect-ratio: 1 / 1;
+ text-align: center;
+ border-radius: 50%;
+ border: 0.5px solid rgba(0, 0, 0, 0.5);
+ margin-left: 20%;
+ margin-top: 25%;
+}
+
+.bullet.dead {
+ background: var(--status-dead);
+}
+
+.bullet.valid {
+ background: var(--status-valid);
+}
+
+.bullet.invalid {
+ background: var(--status-invalid);
+}
+
+.bullet.unknown {
+ background: var(--status-unknown);
+}
+
+.bullet.never_tried {
+ background: var(--status-never-tried);
+}
+
+.bullet.inconsistent {
+ background: var(--status-inconsistent);
+}
+
+.bullet.valid_but_dead {
+ background: var(--status-valid-but-dead);
+}
+
+.bullet.invalid_but_dead {
+ background: var(--status-invalid-but-dead);
+}
+
+.bullet.unknown_but_dead {
+ background: var(--status-unknown-but-dead);
+}
+
+.bullet.valid_under_hyp {
+ background: var(--status-valid-under-hyp);
+}
+
+.bullet.considered_valid {
+ background: var(--status-considered-valid);
+}
+
+.bullet.invalid_under_hyp {
+ background: var(--status-invalid-under-hyp);
+}
+
/* -------------------------------------------------------------------------- */
/* --- Globals --- */
/* -------------------------------------------------------------------------- */
--
GitLab