T0
,L0_APP
scheme L0_OS = with T0 in extend L0_APP with class
  type
    OSInput  = Pointer    -- activate next of prev application, or close current application 
            | AppPath    
    ,AppPath :: path: Text     -- path to the new application
    ,OSOutput

  channel
    osIn:    OSInput
    ,osOut:  OSOutput
  
  value  

     os:       Application-list            -> in osIn, appIn out osOut, appOut  Unit
                               --
                               --  the fg fuction  run new application
                               --  according to the specified user command.
                               --  see AppPath
    ,fg:       OSInput >< Application-list ->                                   OSOutput
                                                                            ><  AppOutput
                                                                            >< Application-list


  axiom


   [os]
     all  aps: Application-list :-
--
--       если есть ввод в osIn его читаем, результат выводим, меняем список задач
--       при изменении фокуса происходит вывод в канал приложения
--
      os ( aps) is
        let (o, a, aps1) = fg(osIn?, aps) in
          osOut!o
          ;appOut!a 
          ;if len aps1 >  0  then appOut!mkAppOutput (hd aps1)  end
          ;os(aps1)
        end
            |=|
--
--        операция внешнего выбора -- external choice
--        пользователь пишет в один из каналов:
--        если есть ответ пользователя в osIn -  его читаем (см выше), 
--        иначе должен быть ответ пользователя в appIn,
--        тогда app выполнит чтение из appIn
--
        app(hd aps)      -- если есть ввод, то есть приложение
        ;os(aps)

end                             

T0
,L0_OS
scheme L0_USR = with T0 in extend L0_OS with class

  value  
     usr: Unit                           -> in any out  any   Unit
    ,usrWork: OSOutput                   -> OSInput 
    ,usrWork: OSOutput                   -> AppInput 
    ,usrWork: AppOutput                  -> OSInput 
    ,usrWork: AppOutput                  -> AppInput 
    


  axiom

   [usr]
     usr () is

        (osIn!usrWork(osOut?)  |^| appIn!usrWork(osOut?)  )         |=|
        (osIn!usrWork(appOut?) |^| appIn!usrWork(appOut?) )         |=|
        skip
        ; usr()

end