##// END OF EJS Templates
Separate get_session_info between HistoryAccessor and HistoryManager...
Separate get_session_info between HistoryAccessor and HistoryManager HistoryAccessor has no concept of the current session, whereas HistoryManager does. HistoryAccessor should therefore always be used with a session number > 0. However, I have added get_last_session_id() to HistoryAccessor to make it easier to work with recent history. Closes gh-5348

File last commit:

r15101:703114ce
r15979:326b5fcd
Show More
tree.less
130 lines | 2.3 KiB | text/x-less | LessCssLexer
/**
* Primary styles
*
* Author: IPython Development Team
*/
@dashboard_tb_pad: 4px;
@dashboard_lr_pad: 7px;
// These are the total heights of the Bootstrap small and mini buttons. These values
// are not less variables so we have to track them statically.
@btn_small_height: 26px;
@btn_mini_height: 22px;
@dark_dashboard_color: darken(@border_color, 30%);
ul#tabs {
margin-bottom: @dashboard_tb_pad;
}
ul#tabs a {
padding-top: @dashboard_tb_pad;
padding-bottom: @dashboard_tb_pad;
}
ul.breadcrumb {
a:focus, a:hover {
text-decoration: none;
}
i.icon-home {
font-size: 16px;
margin-right: 4px;
}
span {
color: @dark_dashboard_color;
}
}
.list_toolbar {
padding: @dashboard_tb_pad 0 @dashboard_tb_pad 0;
}
.list_toolbar [class*="span"] {
min-height: @btn_small_height;
}
.list_header {
font-weight: bold;
}
.list_container {
margin-top: @dashboard_tb_pad;
margin-bottom: 5*@dashboard_tb_pad;
border: 1px solid @border_color;
border-radius: 4px;
}
.list_container > div {
border-bottom: 1px solid @border_color;
&:hover .list-item{
background-color: red;
};
}
.list_container > div:last-child {
border: none;
}
.list_item {
&:hover .list_item {
background-color: #ddd;
};
a {text-decoration: none;}
}
.list_header>div, .list_item>div {
padding-top: @dashboard_tb_pad;
padding-bottom: @dashboard_tb_pad;
padding-left: @dashboard_lr_pad;
padding-right: @dashboard_lr_pad;
height: @btn_mini_height;
line-height: @btn_mini_height;
}
.item_name {
line-height: @btn_mini_height;
height: @btn_small_height;
}
.item_icon {
font-size: 14px;
color: @dark_dashboard_color;
margin-right: @dashboard_lr_pad;
}
.item_buttons {
line-height: 1em;
}
.toolbar_info {
height: @btn_small_height;
line-height: @btn_small_height;
}
input.nbname_input, input.engine_num_input {
// These settings give these inputs a height that matches @btn_mini_height = 22
padding-top: 3px;
padding-bottom: 3px;
height: 14px;
line-height: 14px;
margin: 0px;
}
input.engine_num_input {
width: 60px;
}
.highlight_text {
color: blue;
}
#project_name > .breadcrumb {
padding: 0px;
margin-bottom: 0px;
background-color: transparent;
font-weight: bold;
}