-- line-width indicator
Line_width_hover = nil

  -- line-width indicator
  button('line-width', {x=Margin_left+Line_width-4,y=Margin_top-10, w=10,h=10, color={1,1,1},
    icon = icon.line_width,
    onpress1 = function() Line_width_hover = App.getTime() end,
  })

        -- insert new drawing

                     end})

                     end
        })

    end
  end
  -- update Line_width with some hysteresis while the indicator is dragged
  if Line_width_hover then
    if App.getTime() - Line_width_hover > 0.1 then
      Line_width = App.mouse_x() - Margin_left
      Text.redraw_all()
      if App.mouse_down(1) then
        Line_width_hover = App.getTime()
      else
        Line_width_hover = nil
      end

  -- we seem to sometimes get phantom clicks if the mouse moves down into text while adjusting line-width
  if Line_width_hover then
    Selection1 = {}
    return
  end

function icon.line_width(x, y)
  love.graphics.setColor(0.7,0.7,0.7)
  love.graphics.line(x+0,y+0, x+9,y+0)
  love.graphics.line(x+0,y+1, x+9,y+1)
  love.graphics.line(x+0,y+2, x+9,y+2)
  love.graphics.line(x+0,y+3, x+9,y+3)
  love.graphics.line(x+0,y+4, x+9,y+4)
  love.graphics.line(x+0,y+5, x+9,y+5)
  love.graphics.line(x+1,y+6, x+8,y+6)
  love.graphics.line(x+2,y+7, x+7,y+7)
  love.graphics.line(x+3,y+8, x+6,y+8)
  love.graphics.line(x+4,y+9, x+5,y+9)
end