home *** CD-ROM | disk | FTP | other *** search
/ Liren Large Software Subsidy 16 / 16.iso / w / w055 / 4.ddi / SOURCES.LIF / MOUSE.PEL < prev    next >
Encoding:
Text File  |  1990-09-27  |  16.4 KB  |  757 lines
  1. # $Header:   P:/source/ppee/macros/mouse.pev   1.96   11 Jun 1990 13:00:14   JB  $
  2.  
  3. ##############################################################################
  4. #
  5. #           Sage Software - POLYTRON Division
  6. #             1700 NW 167th Place
  7. #               Beaverton, OR 97006
  8. #
  9. #   Copyright 1990, Sage Software, Inc.
  10. #
  11. #   Permission is hereby granted for licensed users of Sage Professional
  12. #   Editor and PolyAwk to copy and modify this source code for their own
  13. #   personal use.  These derivative works may be distributed only to other
  14. #   licensed Sage Professional Editor and PolyAwk users.  All other usage
  15. #   is prohibited without express written permission from Sage Software.
  16. #
  17. ##############################################################################
  18.  
  19. #### $Workfile:   mouse.pel  $: mouse support
  20.  
  21. global    mouse_selection_type    = NORMAL_SELECTION
  22.  
  23. global    LEFT_BUTTON    = 1
  24. global    RIGHT_BUTTON    = 2
  25. global    BOTH_BUTTONS    = 3
  26. global    MIDDLE_BUTTON    = 4
  27.  
  28. global    LEFT_PRESS    = 0xf000
  29. global    RIGHT_PRESS    = 0xf100
  30. global    MIDDLE_PRESS    = 0xf200
  31. global    LEFT_CLICK    = 0xf600
  32. global    RIGHT_CLICK    = 0xf700
  33. global    MIDDLE_CLICK    = 0xf800
  34.  
  35.     ## augment scan codes in keys.pel
  36. global    SCANCODE_LEFT_PRESS    = 0xf0
  37. global    SCANCODE_RIGHT_PRESS    = 0xf1
  38. global    SCANCODE_LEFT_CLICK    = 0xf6
  39. global    SCANCODE_RIGHT_CLICK    = 0xf7
  40.  
  41. ## assign mouse button events to the usual functions...
  42.     
  43. function assign_mouse_buttons(){                #PUBLIC #VOID
  44.     assign_key( "#61440",  "left_press" )
  45.     assign_key( "#61696",  "right_press" )
  46.     assign_key( "#61952",  "middle_press" )
  47.  
  48.     assign_key( "#62208",  "left_release" )
  49.     assign_key( "#62464",  "right_release" )
  50.     assign_key( "#62720",  "middle_release" )
  51.  
  52.     assign_key( "#62976",  "left_click" )
  53.     assign_key( "#63232",  "right_click" )
  54.     assign_key( "#63488",  "middle_click" )
  55.  
  56.     assign_key( "#63744",  "left_double_click" )
  57.     assign_key( "#64000",  "right_double_click" )
  58.     assign_key( "#64256",  "middle_double_click" )
  59. }
  60.  
  61.  
  62. ## the mouse's position falls into one of the following categories,
  63. #    accurately computed by mouse_position():
  64. #
  65. global MOUSE_IN_BACKGROUND    = 0
  66. global MOUSE_IN_TEXT        = 0x10
  67. global MOUSE_IN_NUMBERS        = 0x20
  68. global MOUSE_N            = 0x01
  69. global MOUSE_E            = 0x02
  70. global MOUSE_S            = 0x04
  71. global MOUSE_W            = 0x08
  72. global MOUSE_IGNORE        = 0x40
  73.  
  74. # composites:
  75.  
  76. global    MOUSE_LEFT        = 0x28    # WEST or IN_NUMBERS
  77. global    MOUSE_LEFTR        = 0x2A    # WEST or IN_NUMBERS or right
  78. #global    MOUSE_LR        = 0x2A    # left or right
  79. global    MOUSE_IN_BORDER        = 0x2F    # anywhere in border
  80. #global    MOUSE_NE        = 0x03  # NE corner
  81. global    MOUSE_SE        = 0x06
  82. global    MOUSE_NW        = 0x09
  83. global    MOUSE_SW        = 0x0C
  84.  
  85. ## The following are set by mouse_position and used by its clients:
  86.  
  87. local    x, y, mw, mouse_pos
  88. local    x0, y0, x1, y1    # these are computed only if MOUSE_IN_BORDER
  89. local    mouse_prev_window
  90. local    mouse_prev_buffer
  91.  
  92. local    highlighted_scroll = 0;    # if set, raise anchor and drop line
  93.                 # selection for every vertical movement
  94.  
  95.  
  96. ## compute qualitatively the current mouse position.
  97. #    ensures that if a window contains the mouse it becomes current
  98. #
  99. global function mouse_position( include_system_win ){
  100.  
  101.     x = mouse_event_x
  102.     y = mouse_event_y
  103.     mouse_prev_window = current_window 
  104.     mouse_prev_buffer = current_buffer 
  105.  
  106.     mw = window_containing( x, y )
  107.  
  108.     if( !mw )
  109.         return mouse_pos = MOUSE_IN_BACKGROUND
  110.  
  111.     current_window = mw
  112.  
  113.      if ( current_window != mw ) {
  114.         # EVENT_NEW_CURNT_WINDOW may have changed the current window
  115.         mouse_pos = MOUSE_IGNORE
  116.  
  117.     } else if( !include_system_win && and( window_flags, WINDOW_SYSTEM )){
  118.         assign_current_window( mouse_prev_window )
  119.         bury_window( mw )
  120.         mouse_pos = MOUSE_IN_BACKGROUND
  121.  
  122.     } else if( window_border_contains( x, y, mw )){
  123.         x0 = window_x0
  124.         y0 = window_y0
  125.         x1 = x0 + window_width - 1
  126.         y1 = y0 + window_height - 1
  127.  
  128.         mouse_pos = 0
  129.  
  130.         if( x == x0 )
  131.             mouse_pos += MOUSE_W
  132.         else if( x == x1 )
  133.             mouse_pos += MOUSE_E
  134.  
  135.         if( y == y0 )
  136.             mouse_pos += MOUSE_N
  137.         else if( y == y1 )
  138.             mouse_pos += MOUSE_S
  139.  
  140.         if( mouse_pos == 0                \
  141.         && linenumber_format                  \
  142.         && x < window_text_x0 )                \
  143.             mouse_pos += MOUSE_IN_NUMBERS
  144.  
  145.         if( !mouse_pos )
  146.             play( "o6g" )
  147.     } else
  148.         mouse_pos = MOUSE_IN_TEXT
  149.  
  150.     return mouse_pos
  151. }
  152.  
  153. ## perform mouse scroll bar action if scroll bars are enabled and the mouse
  154. #    is within a scroll bar
  155.  
  156. function mouse_in_scrollbar(){
  157.  
  158.     if(( and( mouse_pos, MOUSE_E )                 \
  159.         && and( window_flags, WINDOW_SB_RIGHT ))    \
  160.     || ( and( mouse_pos, MOUSE_W )                 \
  161.         && and( window_flags, WINDOW_SB_LEFT ))){
  162.  
  163.         if( y == y0 || y == y1 )
  164.             return 0
  165.  
  166.         if( y == y0 + 1 )                # up arrow
  167.             dynamic_scroll_vertical( -1 )
  168.  
  169.         else if( y == y0 + 2 )                # up diamond
  170.             dynamic_page_up()
  171.  
  172.         else if( y == y1 - 2 )                # down diamond
  173.             dynamic_page_down()
  174.  
  175.         else if( y == y1 - 1 )                # down arrow
  176.             dynamic_scroll_vertical( +1 )
  177.  
  178.         else                        # elevator
  179.             dynamic_elevator()
  180.  
  181.         return 1
  182.     }
  183.  
  184.     if( and( mouse_pos, MOUSE_S )                 \
  185.     && and( window_flags, WINDOW_SB_BELOW )){
  186.  
  187.         if( x == x0 || x == x1 )
  188.             return 0
  189.  
  190.         if( x == x0 + 1 )                # left arrow
  191.             dynamic_scroll_horizontal( -1 )
  192.  
  193.         else if( x == x0 + 2 )            # left diamond
  194.             dynamic_scroll_horizontal( -8 )
  195.  
  196.         else if( x == x1 - 2 )            # right diamond
  197.             dynamic_scroll_horizontal( +8 )
  198.  
  199.         else if( x == x1 - 1 )            # right arrow
  200.             dynamic_scroll_horizontal( +1 )
  201.  
  202.         else                        # elevator
  203.             dynamic_flat_elevator()
  204.  
  205.         return 1
  206.     }
  207.  
  208.     return 0
  209. }
  210.  
  211. ### principal mouse actions
  212.  
  213. ## left button
  214.  
  215. local CTRL_KEY = 4
  216. local ALT_KEY = 8
  217. local SHIFT_KEYS = 3
  218.  
  219. function left_press( include_system_win ){
  220.     local where = mouse_position( include_system_win )
  221.     local seltype
  222.  
  223.     if( where )
  224.         if( and( where, MOUSE_IN_BORDER ))
  225.             left_press_border( where )
  226.         else if ( and( where, MOUSE_IGNORE ))
  227.             return;
  228.         else {
  229.             if( and( keyboard_flags, CTRL_KEY ))
  230.                 move_selection()
  231.  
  232.             else if( and( keyboard_flags, SHIFT_KEYS ))
  233.                 copy_selection()
  234.  
  235.             else {
  236.                 seltype = and( keyboard_flags, ALT_KEY ) \
  237.                     ? COLUMN_SELECTION        \
  238.                     : mouse_selection_type
  239.                 dynamic_selection( seltype, LEFT_BUTTON )
  240.             }
  241.         }
  242.     else if (current_key != LEFT_CLICK)
  243.         mouse_create_window()
  244. }
  245.  
  246. function left_release(){
  247. }
  248.  
  249. function left_click(){
  250.     left_press();
  251. }
  252.  
  253. function left_double_click(){
  254.     left_press()
  255. }
  256.  
  257.  
  258. ## right button
  259.  
  260. function right_press( include_system_win ){
  261.     local where = mouse_position( include_system_win )
  262.  
  263.     if( where )
  264.         if( and( where, MOUSE_IN_BORDER ))
  265.             right_press_border( where )
  266.         else 
  267.             dynamic_selection( COLUMN_SELECTION, RIGHT_BUTTON )
  268.     else
  269.         beep()
  270. }
  271.  
  272. function right_release(){
  273. }
  274.  
  275. function right_click(){
  276.     right_press()
  277. }
  278.  
  279. function right_double_click(){
  280.     right_press()
  281. }
  282.  
  283.  
  284. ## middle button
  285.  
  286. function middle_press( include_system_win ){
  287.     local where = mouse_position( include_system_win )
  288.     local seltype
  289.  
  290.     if( where )
  291.         if( !and( where, MOUSE_IN_BORDER )){
  292.             seltype = and( keyboard_flags, 3 )     \
  293.                 ? COLUMN_SELECTION        \
  294.                 : mouse_selection_type
  295.             dynamic_selection( seltype, LEFT_BUTTON )
  296.         } else if( and( where, MOUSE_LEFT )){    # left margin
  297.             dynamic_selection( LINE_SELECTION, LEFT_BUTTON )
  298.         }
  299. }
  300.  
  301. function middle_release(){
  302.     playback()
  303. }
  304.  
  305. function middle_click(){
  306.     beep()
  307. }
  308.  
  309. function middle_double_click(){
  310.     beep()
  311. }
  312.  
  313.  
  314. ### mouse button helper routines
  315.  
  316. local function left_press_border( where ){
  317.  
  318.     if( where == MOUSE_NW ){        # upper left corner
  319.         smaller_window()
  320.         mouse_display_x = window_x0
  321.         mouse_display_y = window_y0
  322.  
  323.     } else if( and( where, MOUSE_N )){    # title bar
  324.         dynamic_window_move()
  325.  
  326.     } else if( mouse_in_scrollbar()){        # any scroll-bar
  327.         
  328.         # (appropriate action performed by mouse_in_scrollbar())
  329.  
  330.     } else if( where == MOUSE_SE ){        # lower right corner
  331.         dynamic_window_resize()
  332.  
  333.     } else if( where == MOUSE_SW ){        # lower left corner
  334.         play( "o6g" )
  335.  
  336.     } else if( and( where, MOUSE_LEFTR )){    # left or right margin
  337.         dynamic_selection( LINE_SELECTION, LEFT_BUTTON )
  338.  
  339.     } else {                # can't (?) happen
  340.         play( "o6g" )
  341.     }
  342. }
  343.  
  344. local function right_press_border( where ){
  345.  
  346.     if( where == MOUSE_NW ){        # upper left corner
  347.         larger_window()
  348.         mouse_display_x = window_x0
  349.         mouse_display_y = window_y0
  350.  
  351.     } else if( and( where, MOUSE_N )){    # elsewhere in title
  352.         while( and( mouse_buttons, RIGHT_BUTTON )){
  353.             if( mouse_window_deleted())
  354.                 return
  355.         }
  356.         beep()
  357.  
  358.     } else if( and( where, MOUSE_LEFT )){        # left margin
  359.         split_window_horizontal( y - y0 )
  360.         # mouse_display_y --
  361.  
  362.     } else if( and( where, MOUSE_S )){        # bottom margin
  363.         split_window_vertical( x - x0 )
  364.  
  365.     } else {
  366.         play( "o6g" )
  367.     }
  368. }
  369.  
  370. ### mouse library routines
  371.  
  372. local function dynamic_window_move(){
  373.     local xl = window_width,     yl = window_height
  374.     local nx0, ny0
  375.  
  376.     if( !mw || mw != current_window )
  377.         return
  378.  
  379.     while( and( mouse_buttons, LEFT_BUTTON )){
  380.         if( mouse_window_deleted())
  381.             return
  382.         nx0 = x0 + mouse_display_x - x
  383.         ny0 = y0 + mouse_display_y - y
  384.         if( nx0 != window_x0 || ny0 != window_y0 ){
  385.             move_window( nx0, ny0, mw )
  386.             display_update()
  387.         }
  388.     }    
  389. }
  390.  
  391.  
  392. local function dynamic_window_resize(){
  393.     local xl = window_width, yl = window_height
  394.     local nxl, nyl
  395.  
  396.     if( mw && mw == current_window ){
  397.         while( and( mouse_buttons, LEFT_BUTTON )){
  398.             nxl = xl + mouse_display_x - x
  399.             nyl = yl + mouse_display_y - y
  400.             if(( nxl != window_width || nyl != window_height  )        \
  401.             && ( nyl >= WINDOW_MIN_HEIGHT && nxl >= WINDOW_MIN_WIDTH )){
  402.                 frame_window( x0, y0, nxl, nyl, mw )
  403.                 display_update()
  404.             }
  405.         }
  406.     }
  407. }
  408.  
  409.  
  410. global function dynamic_reposition(){
  411.     local first, margin, x0, y0
  412.  
  413.     if( collapsed())
  414.         return
  415.     
  416.     first = window_first
  417.     margin = window_margin
  418.     x0 = window_text_x0
  419.     y0 = window_text_y0
  420.  
  421.     raise_scroll_highlight()
  422.     goto_pos( y - y0 + window_first,     \
  423.           x - x0 + window_margin + 1 )    # x was mouse_display_x
  424.     drop_scroll_highlight()
  425. }
  426.  
  427. global function dynamic_selection( type, button, suppress_marking ){
  428.     local first, margin, x0, y0
  429.     local xx, yy, oldx, oldy
  430.  
  431.     if( collapsed())
  432.         return
  433.     
  434.     first = window_first
  435.     margin = window_margin
  436.     x0 = window_text_x0
  437.     y0 = window_text_y0
  438.  
  439.     raise_scroll_highlight()
  440.     goto_pos( y - y0 + window_first,     \
  441.           x - x0 + window_margin + 1 )    # x was mouse_display_x
  442.     drop_scroll_highlight()
  443.  
  444.     oldx = current_column
  445.     oldy = current_line
  446.  
  447.     raise_anchor()
  448.     if ( !suppress_marking ) {
  449.         drop_anchor( type, create_mark( TEMP_MARK ), 0 )
  450.     }
  451.     display_update()
  452.  
  453.     while( and( mouse_buttons, button )){
  454.         xx = highlighted_scroll ? 1 : mouse_display_x - x0 + window_margin + 1
  455.         yy = mouse_display_y - y0 + window_first
  456.  
  457.         if( xx != current_column || yy != current_line ){
  458.             raise_scroll_highlight()
  459.             goto_pos( yy, xx )
  460.             drop_scroll_highlight()
  461.             display_update()
  462.         }
  463.     }
  464.  
  465.     if( oldx == current_column    \
  466.     &&  oldy == current_line    \
  467.     &&  type != LINE_SELECTION )
  468.         raise_anchor()
  469. }
  470.  
  471.  
  472. local function dynamic_page_up(){
  473.     local smp = scroll_or_pan()
  474.  
  475.     raise_scroll_highlight()
  476.     page_up( smp )
  477.     drop_scroll_highlight()
  478.     pause()
  479.  
  480.     while( and( mouse_buttons, LEFT_BUTTON )){
  481.         raise_scroll_highlight()
  482.         page_up( smp )
  483.         drop_scroll_highlight()
  484.         display_update()
  485.     }
  486. }
  487.  
  488.  
  489. local function dynamic_page_down(){
  490.     local smp = scroll_or_pan()
  491.  
  492.     raise_scroll_highlight()
  493.     page_down( smp )
  494.     drop_scroll_highlight()
  495.     pause()
  496.  
  497.     while( and( mouse_buttons, LEFT_BUTTON )){
  498.         raise_scroll_highlight()
  499.         page_down( smp )
  500.         drop_scroll_highlight()
  501.         display_update()
  502.     }
  503. }
  504.  
  505.  
  506. local function dynamic_scroll_horizontal( dir ){
  507.     local smp = scroll_or_pan()
  508.  
  509.     scroll_horizontal( dir, smp )
  510.     pause()
  511.  
  512.     while( and( mouse_buttons, LEFT_BUTTON )){
  513.         scroll_horizontal( dir, smp )
  514.         display_update()
  515.     }
  516. }
  517.  
  518.  
  519. local function dynamic_scroll_vertical( direction ){
  520.     local smp = scroll_or_pan()
  521.  
  522.     raise_scroll_highlight()
  523.     scroll_vertical( direction, smp )
  524.     drop_scroll_highlight()
  525.     pause()
  526.  
  527.     while( and( mouse_buttons, LEFT_BUTTON )){
  528.         raise_scroll_highlight()
  529.         scroll_vertical( direction, smp )
  530.         drop_scroll_highlight()
  531.         display_update()
  532.     }
  533. }
  534.  
  535.  
  536. #
  537. # delete the current window if left and right mouse buttons
  538. # are depressed, and only if it is a regular window
  539. #
  540. local function mouse_window_deleted(){
  541.     if( (and( mouse_buttons, BOTH_BUTTONS ) == BOTH_BUTTONS )) {
  542.         delete_tiled_window()
  543.         while( and( mouse_buttons, BOTH_BUTTONS ))
  544.             continue
  545.         return 1
  546.     }
  547.     return 0
  548. }
  549.  
  550.  
  551. function mouse_create_window(){    
  552.     local x, y, xl, yl
  553.  
  554.     if ( !and( mouse_buttons, LEFT_BUTTON ))
  555.         return;
  556.  
  557.     x = mouse_event_x
  558.     y = mouse_event_y
  559.  
  560.     message( "SLIDE to opposite corner, then RELEASE" )
  561.  
  562.     while( and( mouse_buttons, LEFT_BUTTON ))
  563.         ;
  564.  
  565.     xl = mouse_display_x - x + 1
  566.     yl = mouse_display_y - y + 1
  567.  
  568.     # normalize so that x0,y0 is the upper left corner:
  569.  
  570.     if( xl < 0 ){
  571.         xl = 2 - xl
  572.         x -= xl - 1
  573.     }
  574.     if( yl < 0 ){
  575.         yl = 2 - yl
  576.         y -= yl - 1
  577.     }
  578.  
  579.     if( xl >= WINDOW_MIN_WIDTH && yl >= WINDOW_MIN_HEIGHT ){
  580.         # create the window:
  581.         
  582.         current_window = create_window( x, y, xl, yl )
  583.         attach_window_buffer( current_window, current_buffer )
  584.         color_current_window()        # maybe change its color
  585.  
  586.         message( "" )
  587.     } else {
  588.         message( "window would be too small" )
  589.     }
  590. }
  591.  
  592. function elevator_position(){
  593.     local pos = ( y1 - y0 - 3 ) * buffer_offset / buffer_size
  594.     # message( " my = %d, y0 = %d, y1 = %d, off = %d, size = %d => %d",     \
  595.     #     mouse_display_y, y0, y1, buffer_offset, buffer_size, pos )
  596.     return pos
  597. }
  598.  
  599. function dynamic_elevator(){
  600.     local yy0 = ( y0 + 3 )
  601.     local yy1 = ( y1 - 3 )
  602.     local whole = yy1 - yy0
  603.     local opart = -1
  604.     local part = y - yy0
  605.     local off
  606.  
  607.     if( whole > 0 ){
  608.         do {
  609.             if( part != opart ){
  610.                 opart = part
  611.                 off = buffer_size * part / whole
  612.                 raise_scroll_highlight()
  613.                 goto_buffer_offset( off )
  614.                 goto_bol()
  615.                 drop_scroll_highlight()
  616.                 skip_whitespace()
  617.                 display_update()
  618.             }
  619.             part = mouse_display_y - yy0
  620.         } while( and( mouse_buttons, LEFT_BUTTON ))
  621.     } else
  622.         beep()        # "can't" happen
  623. }
  624.  
  625.  
  626. function dynamic_flat_elevator(){
  627.     local smp = scroll_or_pan()
  628.     local xx0 = ( x0 + 3 )
  629.     local xx1 = ( x1 - 3 )
  630.     local whole = xx1 - xx0
  631.     local part = x - xx0
  632.     local delta
  633.  
  634.     if( whole > 0 ){
  635.         do {
  636.             delta = ( window_width * part / whole )     \
  637.                 - window_margin
  638.             if( delta ){
  639.                 scroll_horizontal( delta, smp )
  640.                 display_update()
  641.             }
  642.             part = mouse_display_x - xx0
  643.         } while( and( mouse_buttons, LEFT_BUTTON ))
  644.     } else
  645.         beep()        # "can't" happen
  646. }
  647.  
  648.  
  649. local function collapsed(){
  650.     if( and( window_flags, WINDOW_ZOOM ) == WINDOW_COLLAPSED ){
  651.         beep()
  652.         return 1
  653.     }  else
  654.         return 0
  655. }
  656.  
  657.  
  658. # when this function is called, mouse_position() has been called, all 
  659. # related variables have been set, and current_window and current_buffer
  660. # have been updated to the destination versions.
  661.  
  662. local function move_or_copy_selection( copy ){
  663.     local destination_window = current_window
  664.     local source_window = mouse_prev_window
  665.     local type
  666.     local x0,y0
  667.  
  668.     if( collapsed())
  669.         return
  670.  
  671.  
  672.     y0 = y - window_text_y0 + window_first
  673.     x0 = x - window_text_x0 + window_margin + 1
  674.  
  675.     # select source window (also selects source buffer)
  676.  
  677.     assign_current_window( source_window )
  678.  
  679.     # save source region, if any
  680.  
  681.     if(( type = region_type())){
  682.         save_position()
  683.         swap_marks()
  684.         save_position()
  685.         raise_anchor()
  686.     }
  687.  
  688.     # locate new position in destination window (may change buffer)
  689.     # and mark it.
  690.  
  691.     assign_current_window( destination_window )
  692.  
  693.     goto_pos( y0, x0 )
  694.  
  695.     create_mark( TEMP_MARK )
  696.  
  697.     # if there was a marked region, copy or move it to the new pos.
  698.  
  699.     if( type ){
  700.         # restore source selection (removed by dynamic_reposition())
  701.  
  702.         assign_current_window( source_window )
  703.  
  704.         restore_position( 1 )
  705.         drop_anchor( type )
  706.         restore_position( 1 )
  707.  
  708.         # copy or delete to scrap
  709.  
  710.         if( copy ){
  711.             copy_to_scrap()
  712.         } else
  713.             delete_to_scrap()
  714.         raise_anchor()
  715.  
  716.         # insert it in the new location:
  717.  
  718.         assign_current_window( destination_window )
  719.         goto_mark( TEMP_MARK )
  720.         insert_scrap()
  721.     }
  722. }
  723.  
  724. local function move_selection(){
  725.     move_or_copy_selection( 0 )
  726. }
  727.  
  728. local function copy_selection(){
  729.     move_or_copy_selection( 1 )
  730. }
  731.  
  732.  
  733. # local function peep(){
  734. #    play( ">>l16a" )
  735. #}
  736.  
  737. local function pause(){
  738.     display_update()
  739.     play( "_" )
  740. }
  741.  
  742.  
  743. local function raise_scroll_highlight(){
  744.     if (highlighted_scroll)
  745.         raise_anchor();
  746. }
  747.  
  748. local function drop_scroll_highlight(){
  749.     if (highlighted_scroll)
  750.         drop_anchor( LINE_SELECTION );
  751. }
  752.  
  753.  
  754. global function setHighlightedScrolling( mode ){
  755.     highlighted_scroll = 0+mode;
  756. }
  757.