resources/src/mediawiki.widgets.datetime/mediawiki.widgets.datetime.definitions.less

   1 /*!
   2  * OOJS-UI defines used by the existing CSS (will make it easier to put this
   3  * widget in OOJS-UI once OOJS-UI is capable of handling it)
   4  */
   5
   6 .oo-ui-box-sizing( @type: border-box ) {
   7         -webkit-box-sizing: @type;
   8         -moz-box-sizing: @type;
   9         box-sizing: @type;
  10 }
  11
  12 .oo-ui-unselectable() {
  13         -webkit-touch-callout: none;
  14         -webkit-user-select: none;
  15         -moz-user-select: none;
  16         -ms-user-select: none;
  17         user-select: none;
  18 }
  19
  20 .oo-ui-inline-spacing( @spacing, @cancelled-spacing: 0 ) {
  21         margin-right: @spacing;
  22         &:last-child {
  23                 margin-right: @cancelled-spacing;
  24         }
  25 }
  26
  27 .oo-ui-transition( @value1, @value2: X, ... ) {
  28         @value: ~`"@{arguments}".replace(/[\[\]]|\,\sX/g, '')`;
  29         -webkit-transition: @value;
  30         -moz-transition: @value;
  31         transition: @value;
  32 }
  33
  34 @indicator-size: unit(12 / 16 / 0.8, em);
  35 @icon-size: unit(24 / 16 / 0.8, em);
  36 @quick-ease: 100ms ease;
  37 @progressive: #347bff;