base.css 5.7 KB

123456789101112131415161718192021222324252627282930313233343536373839404142434445464748495051525354555657585960616263646566676869707172737475767778798081828384858687888990919293949596979899100101102103104105106107108109110111112113114115116117118119120121122123124125126127128129130131132133134135136137138139140141142143144145146147148149150151152153154155156157158159160161162163164165166167168169170171172173174175176177178179180181182183184185186187188189190191192193194195196197198199200201202203204205206207208209210211212213214215216217218219220221222223224225226227228229230231232233234235236237238239240241242243
  1. /*-----------------------------------------------------------------------------
  2. | Copyright (c) Jupyter Development Team.
  3. | Distributed under the terms of the Modified BSD License.
  4. |----------------------------------------------------------------------------*/
  5. :root {
  6. --jp-private-settingeditor-debug-height: 28px;
  7. --jp-private-settingeditor-key-width: 150px;
  8. --jp-private-settingeditor-legend-height: 16px;
  9. --jp-private-settingeditor-row-height: 16px;
  10. --jp-private-settingeditor-toolbar-height: 28px;
  11. --jp-private-settingeditor-type-width: 75px;
  12. }
  13. #setting-editor {
  14. min-width: 360px;
  15. min-height: 240px;
  16. background-color: var(--jp-layout-color0);
  17. margin-top: -1px;
  18. outline: none;
  19. /* This is needed so that all font sizing of children done in ems is
  20. * relative to this base size */
  21. font-size: var(--jp-ui-font-size1);
  22. }
  23. #setting-editor > .lm-Widget {
  24. position: absolute;
  25. top: 0;
  26. bottom: 0;
  27. left: 0;
  28. right: 0;
  29. }
  30. #setting-editor .lm-SplitPanel-handle {
  31. background-color: var(--jp-border-color2);
  32. }
  33. #setting-editor .jp-SettingEditorInstructions {
  34. text-align: center;
  35. }
  36. #setting-editor .jp-SettingEditorInstructions-icon {
  37. display: inline-block;
  38. height: 78px;
  39. margin: 2px 5px 2px 8px;
  40. width: 60px;
  41. }
  42. #setting-editor .jp-SettingEditorInstructions-title {
  43. color: var(--jp-ui-font-color0);
  44. font-size: 32px;
  45. font-weight: 200;
  46. line-height: 78px;
  47. vertical-align: top;
  48. }
  49. #setting-editor .jp-SettingEditorInstructions-text {
  50. color: var(--jp-ui-font-color0);
  51. font-size: var(--jp-ui-font-size2);
  52. }
  53. #setting-editor .jp-PluginList {
  54. min-width: 175px;
  55. max-width: 275px;
  56. }
  57. #setting-editor .jp-PluginList ul {
  58. background-color: var(--jp-layout-color1);
  59. color: var(--jp-ui-font-color1);
  60. font-size: var(--jp-ui-font-size1);
  61. list-style-type: none;
  62. margin: 0;
  63. padding: 0;
  64. overflow-y: auto;
  65. position: absolute;
  66. top: 0;
  67. bottom: 0;
  68. left: 0;
  69. right: 0;
  70. }
  71. #setting-editor .jp-PluginList li {
  72. display: flex;
  73. flex-direction: row;
  74. border: 1px solid transparent;
  75. overflow: hidden;
  76. padding: 4px 0 4px 4px;
  77. text-overflow: ellipsis;
  78. white-space: nowrap;
  79. }
  80. #setting-editor .jp-PluginList li:hover {
  81. background-color: var(--jp-layout-color2);
  82. border: 1px solid var(--jp-border-color2);
  83. }
  84. #setting-editor .jp-PluginList li.jp-mod-selected {
  85. background-color: var(--jp-brand-color1);
  86. color: white;
  87. border: 1px solid var(--jp-brand-color1);
  88. }
  89. #setting-editor
  90. ul.jp-PluginList
  91. li.jp-mod-selected
  92. span.jp-PluginList-icon.jp-FileIcon {
  93. background-image: var(--jp-icon-file-selected);
  94. }
  95. #setting-editor .jp-PluginList-icon {
  96. display: inline-block;
  97. height: 20px;
  98. width: 20px;
  99. margin-right: 3px;
  100. position: relative;
  101. }
  102. #setting-editor .jp-SettingsRawEditor .jp-Toolbar {
  103. color: var(--jp-ui-font-color0);
  104. font-size: var(--jp-ui-font-size1);
  105. height: var(--jp-private-settingeditor-toolbar-height);
  106. max-height: var(--jp-private-settingeditor-toolbar-height);
  107. }
  108. #setting-editor
  109. .jp-SettingsRawEditor
  110. .jp-Toolbar
  111. .jp-ToolbarButtonComponent-label {
  112. display: none;
  113. }
  114. #setting-editor .jp-SettingsRawEditor .jp-Toolbar-item {
  115. margin-top: 1px;
  116. align-items: center;
  117. }
  118. .jp-ToolbarButtonComponent-label
  119. #setting-editor
  120. .jp-SettingsRawEditor.jp-mod-error
  121. .jp-Toolbar-item.jp-BugIcon::after {
  122. color: red;
  123. content: '\25CF'; /* Unicode circle character (error dot) */
  124. font-size: 7px;
  125. width: 100%;
  126. height: 100%;
  127. position: absolute;
  128. top: 4px;
  129. left: 6px;
  130. }
  131. #setting-editor .jp-SettingsRawEditor .jp-Inspector {
  132. border-top: 2px solid var(--jp-layout-color2);
  133. min-height: var(--jp-private-settingeditor-debug-height);
  134. max-height: var(--jp-private-settingeditor-debug-height);
  135. }
  136. #setting-editor
  137. .jp-SettingsRawEditor
  138. .jp-Inspector.jp-SettingsDebug
  139. .jp-RenderedHTMLCommon {
  140. padding: 2px 5px 2px 0;
  141. width: 100%;
  142. }
  143. #setting-editor
  144. .jp-SettingsRawEditor
  145. .jp-Inspector.jp-SettingsDebug
  146. .jp-RenderedHTMLCommon
  147. p {
  148. text-align: right;
  149. }
  150. #setting-editor .jp-SettingsTableEditor {
  151. border: 1px solid var(--jp-brand-color1);
  152. margin: 0;
  153. padding: 0;
  154. }
  155. #setting-editor .jp-SettingsTableEditor legend {
  156. color: var(--jp-brand-color1);
  157. font-size: 70%;
  158. font-weight: bold;
  159. margin-left: 15px;
  160. height: var(--jp-private-settingeditor-legend-height);
  161. }
  162. #setting-editor .jp-SettingsTableEditor-wrapper {
  163. position: absolute;
  164. top: var(--jp-private-settingeditor-legend-height);
  165. bottom: 0;
  166. overflow-y: auto;
  167. }
  168. #setting-editor .jp-SettingsTableEditor table {
  169. table-layout: fixed;
  170. color: var(--jp-ui-font-color1);
  171. font-size: var(--jp-ui-font-size1);
  172. padding: 2px;
  173. width: calc(100% - 4px);
  174. overflow: hidden;
  175. }
  176. #setting-editor .jp-SettingsTableEditor tr {
  177. color: var(--jp-ui-font-color2);
  178. height: var(--jp-private-settingeditor-row-height);
  179. overflow: hidden;
  180. }
  181. #setting-editor .jp-SettingsTableEditor th {
  182. background-color: var(--jp-layout-color3);
  183. border: 1px solid transparent;
  184. font-weight: bold;
  185. height: var(--jp-private-settingeditor-row-height);
  186. }
  187. #setting-editor .jp-SettingsTableEditor td {
  188. border: 1px solid transparent;
  189. height: var(--jp-private-settingeditor-row-height);
  190. }
  191. #setting-editor .jp-SettingsTableEditor th.jp-SettingsTableEditor-key {
  192. width: var(--jp-private-settingeditor-key-width);
  193. }
  194. #setting-editor .jp-SettingsTableEditor th.jp-SettingsTableEditor-type {
  195. width: var(--jp-private-settingeditor-type-width);
  196. }
  197. #setting-editor .jp-SettingsTableEditor td.jp-SettingsTableEditor-key {
  198. overflow: hidden;
  199. white-space: nowrap;
  200. text-overflow: ellipsis;
  201. }
  202. #setting-editor .jp-SettingsTableEditor td.jp-SettingsTableEditor-value {
  203. overflow: hidden;
  204. white-space: nowrap;
  205. text-overflow: ellipsis;
  206. }
  207. #setting-editor .jp-SettingsTableEditor td.jp-SettingsTableEditor-type {
  208. text-align: right;
  209. }