always show line numbers in source editor

Dependencies

• [2] LIKTH6HM update stale source X-(
• [3] GZ5WULJV switch source side to new screen-line-based render
• [4] J3I6DVMB drop an unused arg
• [5] AOZX2G5F source: no commandline args
• [6] A23MMLJH migrate old settings, attempt #3
• [7] KKMFQDR4 editing source code from within the app
• [8] ISOFHXB2 App.width can no longer take a Text
• [9] W5WCQNMP bugfix: Windows pushing title bar off screen
• [10] S3PNFXTB handle missing cursors in settings
• [11] SDO4DHNU source: load cursor position from settings
• [12] G54H3YG2 get rid of all bifold text
• [13] OI4FPFIN support drawings in the source editor

Change contents

• edit in source_text.lua at line 15
  [3.254]

  [5.87409]
  + App.color(Line_number_color)

  + love.graphics.print(line_index, State.left-Line_number_width*App.width('m')+10,y)
• edit in source_edit.lua at line 10
  [5.152673]

  [5.18034]
  + Line_number_color = {r=0.6, g=0.6, b=0.6}
• replacement in source_edit.lua at line 172
  [5.20316]→[2.302:394](∅→∅)
  − button(State, 'draw', {x=State.left-Margin_left+4, y=y+4, w=12,h=12, color={1,1,0},
  [5.20316]

  [5.20384]
  + button(State, 'draw', {x=4, y=y+4, w=12,h=12, color={1,1,0},
• edit in source.lua at line 4
  [5.165798]

  [5.165798]
  + Line_number_width = 3 -- in ems
• replacement in source.lua at line 129
  [5.169468]→[5.169468:169599](∅→∅)
  − Editor_state = edit.initialize_state(Margin_top, Margin_left, right, settings.font_height, math.floor(settings.font_height*1.3))
  [5.169468]

  [5.169599]
  + Editor_state = edit.initialize_state(Margin_top, Margin_left + Line_number_width*App.width('m'), right, settings.font_height, math.floor(settings.font_height*1.3))
• replacement in source.lua at line 157
  [4.51]→[5.170188:170283](∅→∅),[5.783]→[5.170188:170283](∅→∅),[5.170188]→[5.170188:170283](∅→∅)
  − Editor_state = edit.initialize_state(Margin_top, Margin_left, App.screen.width-Margin_right)
  [4.51]

  [5.115]
  + Editor_state = edit.initialize_state(Margin_top, Margin_left + Line_number_width*App.width('m'), App.screen.width-Margin_right)