base.css 7.0 KB

123456789101112131415161718192021222324252627282930313233343536373839404142434445464748495051525354555657585960616263646566676869707172737475767778798081828384858687888990919293949596979899100101102103104105106107108109110111112113114115116117118119120121122123124125126127128129130131132133134135136137138139140141142143144145146147148149150151152153154155156157158159160161162163164165166167168169170171172173174175176177178179180181182183184185186187188189190191192193194195196197198199200201202203204205206207208209210211212213214215216217218219220221222223224225226227228229230231232233234235236237238239240241242243244245246247248249250251252253254255256257258259260261262263264265266267268269270271272273274275276277278279280281282283284285286287288289290291292293294295296297298299300301302303304305306307
  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 > .p-Widget {
  24. position: absolute;
  25. top: 0;
  26. bottom: 0;
  27. left: 0;
  28. right: 0;
  29. }
  30. #setting-editor .p-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. background-size: 60px;
  39. width: 60px;
  40. height: 78px;
  41. margin-right: 5px;
  42. }
  43. #setting-editor .jp-SettingEditorInstructions-title {
  44. color: var(--jp-ui-font-color0);
  45. font-size: 32px;
  46. font-weight: 200;
  47. line-height: 78px;
  48. vertical-align: top;
  49. }
  50. #setting-editor .jp-SettingEditorInstructions-text {
  51. color: var(--jp-ui-font-color0);
  52. font-size: var(--jp-ui-font-size2);
  53. }
  54. #setting-editor .jp-PluginList {
  55. min-width: 175px;
  56. max-width: 275px;
  57. }
  58. #setting-editor .jp-PluginList ul {
  59. background-color: var(--jp-layout-color1);
  60. color: var(--jp-ui-font-color1);
  61. font-size: var(--jp-ui-font-size1);
  62. list-style-type: none;
  63. margin: 0;
  64. padding: 0;
  65. overflow-y: auto;
  66. position: absolute;
  67. top: 0;
  68. bottom: 0;
  69. left: 0;
  70. right: 0;
  71. }
  72. #setting-editor .jp-PluginList li {
  73. display: flex;
  74. flex-direction: row;
  75. border: 1px solid transparent;
  76. overflow: hidden;
  77. padding: 4px 0 4px 4px;
  78. text-overflow: ellipsis;
  79. white-space: nowrap;
  80. }
  81. #setting-editor .jp-PluginList li:hover {
  82. background-color: var(--jp-layout-color2);
  83. border: 1px solid var(--jp-border-color2);
  84. }
  85. #setting-editor .jp-PluginList li.jp-mod-selected {
  86. background-color: var(--jp-brand-color1);
  87. color: white;
  88. border: 1px solid var(--jp-brand-color1);
  89. }
  90. #setting-editor
  91. ul.jp-PluginList
  92. li.jp-mod-selected
  93. span.jp-PluginList-icon.jp-FileIcon {
  94. background-image: var(--jp-icon-file-selected);
  95. }
  96. #setting-editor .jp-PluginList-icon {
  97. display: inline-block;
  98. height: 20px;
  99. width: 20px;
  100. margin-right: 3px;
  101. position: relative;
  102. }
  103. #setting-editor .jp-SettingsRawEditor .jp-Toolbar {
  104. color: var(--jp-ui-font-color0);
  105. font-size: var(--jp-ui-font-size1);
  106. height: var(--jp-private-settingeditor-toolbar-height);
  107. max-height: var(--jp-private-settingeditor-toolbar-height);
  108. }
  109. #setting-editor
  110. .jp-SettingsRawEditor
  111. .jp-Toolbar
  112. .jp-ToolbarButtonComponent-label {
  113. display: none;
  114. }
  115. #setting-editor .jp-SettingsRawEditor .jp-Toolbar-item {
  116. margin-top: 1px;
  117. align-items: center;
  118. }
  119. .jp-ToolbarButtonComponent-label
  120. #setting-editor
  121. .jp-SettingsRawEditor.jp-mod-error
  122. .jp-Toolbar-item.jp-BugIcon::after {
  123. color: red;
  124. content: '\25CF'; /* Unicode circle character (error dot) */
  125. font-size: 7px;
  126. width: 100%;
  127. height: 100%;
  128. position: absolute;
  129. top: 4px;
  130. left: 6px;
  131. }
  132. #setting-editor .jp-SettingsRawEditor .jp-Inspector {
  133. border-top: 2px solid var(--jp-layout-color2);
  134. min-height: var(--jp-private-settingeditor-debug-height);
  135. max-height: var(--jp-private-settingeditor-debug-height);
  136. }
  137. #setting-editor
  138. .jp-SettingsRawEditor
  139. .jp-Inspector.jp-SettingsDebug
  140. .jp-RenderedHTMLCommon {
  141. padding: 2px 5px 2px 0;
  142. width: 100%;
  143. }
  144. #setting-editor
  145. .jp-SettingsRawEditor
  146. .jp-Inspector.jp-SettingsDebug
  147. .jp-RenderedHTMLCommon
  148. p {
  149. text-align: right;
  150. }
  151. #setting-editor .jp-SettingsTableEditor {
  152. border: 1px solid var(--jp-brand-color1);
  153. margin: 0;
  154. padding: 0;
  155. }
  156. #setting-editor .jp-SettingsTableEditor legend {
  157. color: var(--jp-brand-color1);
  158. font-size: 70%;
  159. font-weight: bold;
  160. margin-left: 15px;
  161. height: var(--jp-private-settingeditor-legend-height);
  162. }
  163. #setting-editor .jp-SettingsTableEditor-wrapper {
  164. position: absolute;
  165. top: var(--jp-private-settingeditor-legend-height);
  166. bottom: 0;
  167. overflow-y: auto;
  168. }
  169. #setting-editor .jp-SettingsTableEditor table {
  170. table-layout: fixed;
  171. color: var(--jp-ui-font-color1);
  172. font-size: var(--jp-ui-font-size1);
  173. padding: 2px;
  174. width: calc(100% - 4px);
  175. overflow: hidden;
  176. }
  177. #setting-editor .jp-SettingsTableEditor tr {
  178. color: var(--jp-ui-font-color2);
  179. height: var(--jp-private-settingeditor-row-height);
  180. overflow: hidden;
  181. }
  182. #setting-editor .jp-SettingsTableEditor th {
  183. background-color: var(--jp-layout-color3);
  184. border: 1px solid transparent;
  185. font-weight: bold;
  186. height: var(--jp-private-settingeditor-row-height);
  187. }
  188. #setting-editor .jp-SettingsTableEditor td {
  189. border: 1px solid transparent;
  190. height: var(--jp-private-settingeditor-row-height);
  191. }
  192. #setting-editor .jp-SettingsTableEditor th.jp-SettingsTableEditor-key {
  193. width: var(--jp-private-settingeditor-key-width);
  194. }
  195. #setting-editor .jp-SettingsTableEditor th.jp-SettingsTableEditor-type {
  196. width: var(--jp-private-settingeditor-type-width);
  197. }
  198. #setting-editor .jp-SettingsTableEditor td.jp-SettingsTableEditor-key {
  199. overflow: hidden;
  200. white-space: nowrap;
  201. text-overflow: ellipsis;
  202. }
  203. #setting-editor .jp-SettingsTableEditor td.jp-SettingsTableEditor-value {
  204. overflow: hidden;
  205. white-space: nowrap;
  206. text-overflow: ellipsis;
  207. }
  208. #setting-editor .jp-SettingsTableEditor td.jp-SettingsTableEditor-type {
  209. text-align: right;
  210. }
  211. #setting-editor
  212. .jp-PluginList
  213. .jp-mod-selected
  214. .jp-PluginList-icon.jp-FileIcon {
  215. background-image: var(--jp-icon-file-selected);
  216. }
  217. #setting-editor
  218. .jp-PluginList
  219. .jp-mod-selected
  220. .jp-PluginList-icon.jp-TextEditorIcon {
  221. background-image: var(--jp-icon-text-editor-selected);
  222. }
  223. #setting-editor
  224. .jp-PluginList
  225. .jp-mod-selected
  226. .jp-PluginList-icon.jp-NotebookIcon {
  227. background-image: var(--jp-icon-notebook-selected);
  228. }
  229. #setting-editor
  230. .jp-PluginList
  231. .jp-mod-selected
  232. .jp-PluginList-icon.jp-FolderIcon {
  233. background-image: var(--jp-icon-folder-selected);
  234. }
  235. #setting-editor
  236. .jp-PluginList
  237. .jp-mod-selected
  238. .jp-PluginList-icon.jp-CodeConsoleIcon {
  239. background-image: var(--jp-icon-console-selected);
  240. }
  241. #setting-editor
  242. .jp-PluginList
  243. .jp-mod-selected
  244. .jp-PluginList-icon.jp-MarkdownIcon {
  245. background-image: var(--jp-icon-markdown-selected);
  246. }
  247. #setting-editor
  248. .jp-PluginList
  249. .jp-mod-selected
  250. .jp-PluginList-icon.jp-LauncherIcon {
  251. background-image: var(--jp-icon-launcher-selected);
  252. }
  253. #setting-editor
  254. .jp-PluginList
  255. .jp-mod-selected
  256. .jp-PluginList-icon.jp-SettingsIcon {
  257. background-image: var(--jp-icon-settings-selected);
  258. }
  259. #setting-editor
  260. .jp-PluginList
  261. .jp-mod-selected
  262. .jp-PluginList-icon.jp-KeyboardIcon {
  263. background-image: var(--jp-icon-keyboard-selected);
  264. }