equal
deleted
inserted
replaced
1480 val head = |
1480 val head = |
1481 List( |
1481 List( |
1482 HTML.title("Isabelle Build Manager"), |
1482 HTML.title("Isabelle Build Manager"), |
1483 Web_App.More_HTML.icon("data:image/x-icon;base64," + logo.encode_base64.text), |
1483 Web_App.More_HTML.icon("data:image/x-icon;base64," + logo.encode_base64.text), |
1484 HTML.style_file("https://hawkz.github.io/gdcss/gd.css"), |
1484 HTML.style_file("https://hawkz.github.io/gdcss/gd.css"), |
1485 HTML.style("html { background-color: white; }")) |
1485 HTML.style(""" |
|
1486 :root { |
|
1487 --color-secondary: var(--color-tertiary); |
|
1488 --color-secondary-hover: var(--color-tertiary-hover); |
|
1489 } |
|
1490 html { background-color: white; }""")) |
1486 } |
1491 } |
1487 |
1492 |
1488 def init: Unit = server.start() |
1493 def init: Unit = server.start() |
1489 def loop_body(u: Unit): Unit = { |
1494 def loop_body(u: Unit): Unit = { |
1490 if (progress.stopped) server.stop() |
1495 if (progress.stopped) server.stop() |