#include "tpl_os_kernel.h"          /* tpl_schedule */
#include "tpl_os_timeobj_kernel.h"  /* tpl_counter_tick */
#include "tpl_machine_interface.h"  /* tpl_switch_context_from_it */

#define OS_START_SEC_CODE
#include "tpl_memmap.h"
%

if exists INTERRUPTSOURCES then
foreach INTERRUPTSOURCES prefixedby interrupt_ do
  let counterFct := emptylist
  foreach COUNTERS prefixedby counter_ do
    if counter_SOURCE == interrupt_NAME then
      let counterFct += counter_NAME
    end if
  end foreach
  foreach counterFct
    before
%
FUNC(void, OS_CODE) tpl_tick_% ! interrupt_NAME %()
{
%
    do
      %  tpl_counter_tick(&% !NAME %_counter_desc);
%
    after %
  
  check_buttons_period++;
  if (check_buttons_period == 10)
  {
    /* Call check_buttons_status() (via interrupts)
     * which will check if buttons are pressed or not.
     */
     *AT91C_AIC_ISCR = (1 << AT91C_PERIPHERAL_ID_IRQ0);
     check_buttons_period = 0;
  }

  if (tpl_kern.need_schedule)
  {
    tpl_schedule_from_running();
    LOCAL_SWITCH_CONTEXT()
  }
}
%
  end foreach
end foreach

end if
%
#define OS_STOP_SEC_CODE
#include "tpl_memmap.h"