// Our own variables for this page

@cell_selected_background:      darken(@body-bg, 2%);
@cell_background:               darken(@body-bg, 3.2%);
@border_color:                  darken(@cell_selected_background, 31%);
@light_border_color:            darken(@cell_selected_background, 17%);
@border_width:                  1px;
@notebook_font_size:            14px;
@notebook_line_height:          20px;
@code_line_height:              1.21429em;  // changed from 1.231 to get 17px even
@code_padding:                  0.4em;  // 5.6 px
@notebook-shadow:               inset 1px 4px 9px -6px rgba(0,0,0,.25);
@rendered_html_border_color:    black;
@input_prompt_color:            navy;
@output_prompt_color:           darkred;
@output_pre_color:              black;
@notification_widget_bg:        rgba(240, 240, 240, 0.5);