Reformat web_config css with prettier

I'm not a fan of how prettier formats code, but this file was a mess
with inconsistent indentation, and the result is okay.

[ci skip]
This commit is contained in:
Fabian Homborg 2020-12-10 16:23:13 +01:00
parent 1d7978d282
commit a4e2a3c049

View file

@ -1,6 +1,7 @@
body { body {
background: linear-gradient(to bottom, #a7cfdf 0%,#23538a 100%); background: linear-gradient(to bottom, #a7cfdf 0%, #23538a 100%);
font-family: "Source Code Pro", "DejaVu Sans Mono", Menlo, "Ubuntu Mono", Consolas, Monaco, "Lucida Console", monospace, fixed; font-family: "Source Code Pro", "DejaVu Sans Mono", Menlo, "Ubuntu Mono", Consolas, Monaco,
"Lucida Console", monospace, fixed;
color: #222; color: #222;
min-height: 100vh; /* at least 1 screen high - to prevent the gradient from running out on a short tab */ min-height: 100vh; /* at least 1 screen high - to prevent the gradient from running out on a short tab */
width: 90%; width: 90%;
@ -12,7 +13,8 @@ body {
} }
code { code {
font-family: "Source Code Pro", "DejaVu Sans Mono", Menlo, "Ubuntu Mono", Consolas, Monaco, "Lucida Console", monospace, fixed; font-family: "Source Code Pro", "DejaVu Sans Mono", Menlo, "Ubuntu Mono", Consolas, Monaco,
"Lucida Console", monospace, fixed;
} }
@media screen and (max-width: 700px) { @media screen and (max-width: 700px) {
@ -37,8 +39,8 @@ code {
} }
.tab { .tab {
display: table-cell; display: table-cell;
border: 1px solid #CCC; border: 1px solid #ccc;
border-right: none; border-right: none;
padding-bottom: 15px; padding-bottom: 15px;
padding-top: 15px; padding-top: 15px;
@ -51,21 +53,21 @@ code {
} }
#tab_parent :first-child { #tab_parent :first-child {
border-top-left-radius: 8px; border-top-left-radius: 8px;
} }
#tab_parent :last-child { #tab_parent :last-child {
border-top-right-radius: 8px; border-top-right-radius: 8px;
} }
.tab_first { .tab_first {
border-top-left-radius: 5px; border-top-left-radius: 5px;
border-bottom-left-radius: 5px; border-bottom-left-radius: 5px;
} }
.tab_last { .tab_last {
border-top-right-radius: 5px; border-top-right-radius: 5px;
border-bottom-right-radius: 5px; border-bottom-right-radius: 5px;
} }
.selected_tab { .selected_tab {
@ -74,14 +76,14 @@ code {
} }
#tab_contents { #tab_contents {
padding-top: 20px; padding-top: 20px;
padding-bottom: 20px; padding-bottom: 20px;
width: 100%; width: 100%;
min-height: 80vh; min-height: 80vh;
background-color: #eeeefa; background-color: #eeeefa;
border-bottom-left-radius: 8px; border-bottom-left-radius: 8px;
border-bottom-right-radius: 8px; border-bottom-right-radius: 8px;
margin-bottom: 20px; margin-bottom: 20px;
} }
.footer { .footer {
@ -90,10 +92,10 @@ code {
} }
.master_detail_table { .master_detail_table {
display: table; display: table;
margin-top: 10px; margin-top: 10px;
margin-left: 12px; margin-left: 12px;
margin-right: 12px; margin-right: 12px;
} }
.master { .master {
@ -108,20 +110,20 @@ code {
.detail { .detail {
display: table-cell; display: table-cell;
border: 1px solid #555; border: 1px solid #555;
background-color: #ffffff; background-color: #ffffff;
padding-top: 30px; padding-top: 30px;
padding-bottom: 20px; padding-bottom: 20px;
padding-left: 30px; padding-left: 30px;
padding-right: 30px; padding-right: 30px;
border-radius: 5; border-radius: 5;
width: 100%; width: 100%;
} }
.detail_function pre { .detail_function pre {
white-space: pre-wrap !important; white-space: pre-wrap !important;
width: 100%; width: 100%;
font-size: 11pt; font-size: 11pt;
} }
/* The colours used for function highlighting are taken from the fish /* The colours used for function highlighting are taken from the fish
@ -129,16 +131,36 @@ code {
* These could be pulled from the current terminal (but the background colour * These could be pulled from the current terminal (but the background colour
* might be different), or dynamically from colorutils.js. * might be different), or dynamically from colorutils.js.
*/ */
.detail_function .fish_color_autosuggestion { color: #555; } .detail_function .fish_color_autosuggestion {
.detail_function .fish_color_command { color: #005fd7; } color: #555;
.detail_function .fish_color_param { color: #00afff; } }
.detail_function .fish_color_redirection { color: #00afff; } .detail_function .fish_color_command {
.detail_function .fish_color_comment { color: #990000; } color: #005fd7;
.detail_function .fish_color_error { color: #ff0000; } }
.detail_function .fish_color_escape { color: #00a6b2; } .detail_function .fish_color_param {
.detail_function .fish_color_operator { color: #00a6b2; } color: #00afff;
.detail_function .fish_color_quote { color: #999900; } }
.detail_function .fish_color_statement_terminator { color: #009900; } .detail_function .fish_color_redirection {
color: #00afff;
}
.detail_function .fish_color_comment {
color: #990000;
}
.detail_function .fish_color_error {
color: #ff0000;
}
.detail_function .fish_color_escape {
color: #00a6b2;
}
.detail_function .fish_color_operator {
color: #00a6b2;
}
.detail_function .fish_color_quote {
color: #999900;
}
.detail_function .fish_color_statement_terminator {
color: #009900;
}
.master_element { .master_element {
cursor: pointer; cursor: pointer;
@ -147,22 +169,22 @@ code {
padding-left: 5px; padding-left: 5px;
padding-right: 22px; padding-right: 22px;
font-size: 12pt; font-size: 12pt;
/* Make our border overlap the detail, even if we're unselected (so it doesn't jump when selected) */ /* Make our border overlap the detail, even if we're unselected (so it doesn't jump when selected) */
position: relative; position: relative;
left: 1px; left: 1px;
border-bottom-style: solid; border-bottom-style: solid;
border-bottom-width: 0px; border-bottom-width: 0px;
} }
.selected_master_elem { .selected_master_elem {
border: 1px solid #555; border: 1px solid #555;
border-right: none; border-right: none;
background-color: #FFFFFF; background-color: #ffffff;
border-top-left-radius: 5; border-top-left-radius: 5;
border-bottom-left-radius: 5; border-bottom-left-radius: 5;
/* Pad one less than .master_element, to accomodate our border. */ /* Pad one less than .master_element, to accomodate our border. */
padding-top: 5px; padding-top: 5px;
padding-bottom: 10px; padding-bottom: 10px;
padding-left: 4px; padding-left: 4px;
@ -183,395 +205,413 @@ code {
border-bottom-style: inherit; border-bottom-style: inherit;
border-bottom-color: inherit; border-bottom-color: inherit;
border-bottom-width: 1px; border-bottom-width: 1px;
display: none; display: none;
} }
.selected_master_elem > .master_element_description { .selected_master_elem > .master_element_description {
display: inline; display: inline;
} }
/* We have a newline between the label and description; hide it initially, but show it when it's selected */ /* We have a newline between the label and description; hide it initially, but show it when it's selected */
.master_element > br { display: none; } .master_element > br {
.selected_master_elem > br { display: inherit; } display: none;
}
.selected_master_elem > br {
display: inherit;
}
/* Set this class to suppress the border bottom on master_element_texts with visible descriptions */ /* Set this class to suppress the border bottom on master_element_texts with visible descriptions */
.master_element_no_border { border-bottom-width: 0 } .master_element_no_border {
border-bottom-width: 0;
}
.colorpicker_term256 { .colorpicker_term256 {
border: solid #444 1px; border: solid #444 1px;
border-collapse: collapse; border-collapse: collapse;
} }
.colorpicker_modifiers { .colorpicker_modifiers {
margin-top: 10px; margin-top: 10px;
display:inline-block; display: inline-block;
margin-left: auto; margin-left: auto;
margin-right: auto; margin-right: auto;
color: #000; color: #000;
font-size: smaller; font-size: smaller;
} }
.colorpicker_modifier_cell { .colorpicker_modifier_cell {
cursor: pointer; cursor: pointer;
display:inline-block; display: inline-block;
text-align: center; text-align: center;
border: groove #333 2px; border: groove #333 2px;
padding: 5px; padding: 5px;
margin-top: 5px; margin-top: 5px;
margin-left: auto; margin-left: auto;
margin-right: auto; margin-right: auto;
} }
.modifier_cell_selected { .modifier_cell_selected {
border-color: #000; border-color: #000;
background-color: #444; background-color: #444;
} }
.data_table { .data_table {
table-layout:fixed; table-layout: fixed;
width: 100%; width: 100%;
padding-left: 10px; padding-left: 10px;
padding-right: 10px; padding-right: 10px;
} }
.data_table_row { .data_table_row {
} }
.data_table_cell { .data_table_cell {
padding-top: 5px; padding-top: 5px;
padding-bottom: 5px; padding-bottom: 5px;
vertical-align: top; vertical-align: top;
overflow:hidden; overflow: hidden;
border-bottom: #444 dotted 1px; border-bottom: #444 dotted 1px;
word-wrap: break-word; word-wrap: break-word;
} }
.raw_binding { .raw_binding {
padding-left: 20px; padding-left: 20px;
font-family: monospace; font-family: monospace;
} }
.history_text { .history_text {
padding-top: 5px; padding-top: 5px;
padding-bottom: 5px; padding-bottom: 5px;
vertical-align: top; vertical-align: top;
overflow:hidden; overflow: hidden;
border-bottom: #444 dotted 1px; border-bottom: #444 dotted 1px;
word-wrap: break-word; word-wrap: break-word;
} }
.history_delete { .history_delete {
width: 20px; width: 20px;
border-bottom: #444 dotted 1px; border-bottom: #444 dotted 1px;
} }
.abbreviation_actions { .abbreviation_actions {
width: 8em; width: 8em;
text-align: right; text-align: right;
border-bottom: #444 dotted 1px; border-bottom: #444 dotted 1px;
} }
.abbreviation_input { .abbreviation_input {
height: 1.5em; height: 1.5em;
font: inherit; font: inherit;
padding: 3px; padding: 3px;
margin: 0; margin: 0;
} }
/* The CSS we apply when a table row is filtered */ /* The CSS we apply when a table row is filtered */
.data_table_row_filtered { .data_table_row_filtered {
display: none; display: none;
} }
.no_overflow { .no_overflow {
text-overflow: ellipsis; text-overflow: ellipsis;
white-space: nowrap; white-space: nowrap;
} }
.colorpicker_target { .colorpicker_target {
margin: 0 0 -50px 0; margin: 0 0 -50px 0;
position: relative; position: relative;
bottom: 47px; bottom: 47px;
float: left; /* for some reason this makes the cells that it overlaps (before adjusting its bottom) clickable in Safari */ float: left; /* for some reason this makes the cells that it overlaps (before adjusting its bottom) clickable in Safari */
} }
.colorpicker_target_tab { .colorpicker_target_tab {
cursor: pointer; cursor: pointer;
color: #555; color: #555;
border: solid 1px #555; border: solid 1px #555;
padding-top: 5px; padding-top: 5px;
padding-bottom: 5px; padding-bottom: 5px;
padding-left: 7px; padding-left: 7px;
padding-right: 7px; padding-right: 7px;
display: inline-block; display: inline-block;
background-color: black; background-color: black;
margin-right: -2px; margin-right: -2px;
min-width: 110px; min-width: 110px;
text-align: center; text-align: center;
} }
.colorpicker_target_selected { .colorpicker_target_selected {
background-color: #181818; /* same as #detail */ background-color: #181818; /* same as #detail */
color: white; color: white;
} }
.colorpicker_term256_row { .colorpicker_term256_row {
padding: 0; padding: 0;
} }
.colorpicker_term256_cell { .colorpicker_term256_cell {
width: 18px; width: 18px;
height: 18px; height: 18px;
border: solid black 1px; border: solid black 1px;
padding: 0; padding: 0;
} }
.colorpicker_term256_selection_indicator { .colorpicker_term256_selection_indicator {
width: 18px; width: 18px;
height: 16px; height: 16px;
margin: -4px; margin: -4px;
border: solid white 4px; border: solid white 4px;
position: relative; position: relative;
z-index: 2; z-index: 2;
} }
.colorpicker_cell_selected { .colorpicker_cell_selected {
width: 12px; width: 12px;
height: 12px; height: 12px;
} }
.colorpicker_text_sample, .colorpicker_text_sample_tight { .colorpicker_text_sample,
font-size: 12pt; .colorpicker_text_sample_tight {
padding: 25px; font-size: 12pt;
margin: 5px 20px 25px 20px; /* top right bottom left */ padding: 25px;
cursor: pointer; margin: 5px 20px 25px 20px; /* top right bottom left */
line-height: 1.8em; cursor: pointer;
border: solid #777 1px; line-height: 1.8em;
position: relative; /* so that our absolutely positioned elements work */ border: solid #777 1px;
position: relative; /* so that our absolutely positioned elements work */
} }
.cs_clickable { .cs_clickable {
border: dotted 1px #777; border: dotted 1px #777;
padding: 4px; padding: 4px;
margin: -5px; margin: -5px;
} }
.cs_editing { .cs_editing {
border: solid 3px #3399FF; border: solid 3px #3399ff;
padding: 4px; padding: 4px;
margin: -7px; margin: -7px;
} }
.colorpicker_text_sample_tight { .colorpicker_text_sample_tight {
font-size: 10pt; font-size: 10pt;
line-height: 1.2em; line-height: 1.2em;
margin: 0px 6px; margin: 0px 6px;
max-width: 220px; max-width: 220px;
padding: 5px; padding: 5px;
white-space:nowrap; white-space: nowrap;
overflow: hidden; overflow: hidden;
text-overflow: clip; text-overflow: clip;
} }
.color_picker_background_cells { .color_picker_background_cells {
position: absolute; position: absolute;
right: 0px; right: 0px;
top: 0px; top: 0px;
} }
.color_picker_background_cells div { .color_picker_background_cells div {
width: 24px; width: 24px;
height: 24px; height: 24px;
border-style: solid; border-style: solid;
border-color: #777; border-color: #777;
border-width: 0 0 1px 1px; /* top right bottom left */ border-width: 0 0 1px 1px; /* top right bottom left */
float: left; float: left;
} }
.color_picker_background_cells span { .color_picker_background_cells span {
float: left; float: left;
font-size: 12pt; font-size: 12pt;
padding-top: 2px; padding-top: 2px;
padding-right: 8px; padding-right: 8px;
cursor: pointer; cursor: pointer;
} }
.color_scheme_choice_label, .prompt_demo_choice_label { .color_scheme_choice_label,
margin-left: 10px; .prompt_demo_choice_label {
margin-bottom: 3px; margin-left: 10px;
cursor: pointer; margin-bottom: 3px;
font-size: 12pt; cursor: pointer;
white-space: normal; font-size: 12pt;
white-space: normal;
} }
.color_scheme_choices_scrollview, .prompt_choices_scrollview { .color_scheme_choices_scrollview,
padding-top: 5px; .prompt_choices_scrollview {
overflow-y: scroll; padding-top: 5px;
max-height: 70vh; /* fill out roughly the rest of the screen once scrolled to the preview */ overflow-y: scroll;
max-height: 70vh; /* fill out roughly the rest of the screen once scrolled to the preview */
} }
.color_scheme_choices_list, .prompt_choices_list { .color_scheme_choices_list,
overflow-y: hidden; /* makes our height account for floats */ .prompt_choices_list {
padding: 0 10px 15px 10px; /* top right bottom left */ overflow-y: hidden; /* makes our height account for floats */
bottom: 0px; padding: 0 10px 15px 10px; /* top right bottom left */
bottom: 0px;
} }
.color_scheme_choice_container { .color_scheme_choice_container {
float: left; float: left;
padding: 5px; padding: 5px;
} }
.fake_cursor { .fake_cursor {
background-color: #999; background-color: #999;
} }
.error_msg { .error_msg {
color: red; color: red;
font-size: 12pt; font-size: 12pt;
margin-left: 24pt; margin-left: 24pt;
margin-top: 5pt; margin-top: 5pt;
margin-bottom: 5pt; margin-bottom: 5pt;
} }
img.delete_icon { img.delete_icon {
width: 20px; width: 20px;
height: 20px; height: 20px;
cursor: pointer; cursor: pointer;
text-decoration: none; text-decoration: none;
border: none; border: none;
} }
#table_filter_container { #table_filter_container {
/* top right bottom left*/ /* top right bottom left*/
padding: 0 10 10 30; padding: 0 10 10 30;
text-align: right; text-align: right;
position: relative; position: relative;
bottom: 10px; bottom: 10px;
} }
.filter_text_box { .filter_text_box {
width: 250px; width: 250px;
padding: 5 10 5 10; padding: 5 10 5 10;
border-radius: 15px; border-radius: 15px;
font-size: 12pt; font-size: 12pt;
font-weight: bold; font-weight: bold;
} }
.prompt_demo, .current_prompt { .prompt_demo,
background-color: #000; .current_prompt {
font-size: 12pt; background-color: #000;
padding: 25px; font-size: 12pt;
margin: 5px 5px 25px 5px; /* top right bottom left */ padding: 25px;
cursor: pointer; margin: 5px 5px 25px 5px; /* top right bottom left */
line-height: 1.8em; cursor: pointer;
border: solid #333 1px; line-height: 1.8em;
position: relative; /* so that our absolutely positioned elements work */ border: solid #333 1px;
white-space: nowrap; position: relative; /* so that our absolutely positioned elements work */
overflow: hidden; white-space: nowrap;
text-overflow: ellipsis; overflow: hidden;
color: #c0c0c0; /* set_color normal, assume white (not brwhite) */ text-overflow: ellipsis;
color: #c0c0c0; /* set_color normal, assume white (not brwhite) */
} }
.prompt_demo { .prompt_demo {
color: #AAA; color: #aaa;
white-space: pre; white-space: pre;
} }
.unbordered { .unbordered {
border: none; border: none;
padding-top: 0; padding-top: 0;
padding-bottom: 0; padding-bottom: 0;
} }
.save_button, .prompt_save_button, .colors_close_button, .customize_theme_button, .generic_button { .save_button,
border-radius: 5px; .prompt_save_button,
border: solid rgba(71,71,71,0.5) 1px; .colors_close_button,
padding: 5px 8px; .customize_theme_button,
font-size: 13pt; .generic_button {
display: inline-block; border-radius: 5px;
margin-top: 12px; border: solid rgba(71, 71, 71, 0.5) 1px;
background-color: rgba(128,128,128,0.4); padding: 5px 8px;
color: #FFF; font-size: 13pt;
cursor: pointer; display: inline-block;
margin-top: 12px;
background-color: rgba(128, 128, 128, 0.4);
color: #fff;
cursor: pointer;
} }
.save_button:hover, .customize_theme_button:hover, .generic_button:hover { .save_button:hover,
border-color: rgba(71,71,71,0.9); .customize_theme_button:hover,
.generic_button:hover {
border-color: rgba(71, 71, 71, 0.9);
} }
.button_highlight { .button_highlight {
background-color: rgba(128,128,128,0.6) background-color: rgba(128, 128, 128, 0.6);
} }
.prompt_save_button { .prompt_save_button {
background-color: #333; background-color: #333;
border: solid #525252 1px; border: solid #525252 1px;
color: #ffffff; color: #ffffff;
margin: 2px 20px 25px; /* top right bottom left */ margin: 2px 20px 25px; /* top right bottom left */
font-size: 12pt; font-size: 12pt;
} }
.prompt_demo_text { .prompt_demo_text {
white-space: pre; white-space: pre;
line-height: 170%; line-height: 170%;
padding: 4px 12px; padding: 4px 12px;
font-size: 14pt; font-size: 14pt;
top: 0px; top: 0px;
bottom: 0px; bottom: 0px;
vertical-align: middle; vertical-align: middle;
display: table-cell; display: table-cell;
height: 72px; /* this is really the min height */ height: 72px; /* this is really the min height */
} }
.prompt_function { .prompt_function {
display: block; display: block;
border: 1px solid #555; border: 1px solid #555;
background-color: #181818; background-color: #181818;
margin: 5px 20px 5px; margin: 5px 20px 5px;
border-radius: 5; border-radius: 5;
} }
.prompt_function_text { .prompt_function_text {
white-space: pre-wrap; white-space: pre-wrap;
padding: 15px 3px; padding: 15px 3px;
width: 100%; width: 100%;
height: 25%; height: 25%;
overflow: auto; overflow: auto;
} }
.external_link_img { .external_link_img {
width: 16px; width: 16px;
height: 16px; height: 16px;
vertical-align: text-top; vertical-align: text-top;
margin-left: 10px; margin-left: 10px;
} }
.paginator { .paginator {
border-spacing: 0; border-spacing: 0;
border-collapse: collapse; border-collapse: collapse;
display: inline; display: inline;
vertical-align: bottom; vertical-align: bottom;
margin-right: 15px; margin-right: 15px;
} }
.paginator td { .paginator td {
border: solid 1px #777; border: solid 1px #777;
padding: 8px; padding: 8px;
} }
.paginator .prev, .paginator .next { .paginator .prev,
font-size: 11pt; .paginator .next {
font-size: 11pt;
} }
.paginator a { .paginator a {
text-decoration: none; text-decoration: none;
text-align: center; text-align: center;
color: #0080AA; color: #0080aa;
font-size: larger; font-size: larger;
} }
.paginator .disabled a { .paginator .disabled a {
color: #BBB; color: #bbb;
background-color: transparent; background-color: transparent;
cursor: default; cursor: default;
} }