#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"
%
foreach INTERRUPTSOURCES prefixedby interrupt_ do
  let counterFct := emptylist
  foreach HARDWARECOUNTERS 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 %
  
  if (tpl_kern.need_schedule)
  {
    tpl_schedule_from_running();
    LOCAL_SWITCH_CONTEXT()
  }
}
%
  end foreach
end foreach
%
#define OS_STOP_SEC_CODE
#include "tpl_memmap.h"