
// 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
@rendered_html_border_color:    black;
@input_prompt_color:            #303F9F;
@output_prompt_color:           #D84315;
@output_pre_color:              black;
@notification_widget_bg:        rgba(240, 240, 240, 0.5);


@selected_border_color:           #42A5F5;
@selected_border_color_light:     #90CAF9;
@soft_select_color:             #E3F2FD;


@edit_mode_border_color:        #66BB6A;
@cell_padding:                  6px;
@cell_border_width:             1px;
