module Editor where import Core_datatype import Kernel import Lookup import Vtslib import X_interface import Goals import Globals -- partain import Tags -- partain import Edlib import Type_defs import Tree editor cmdL initial update quit_check finish = initial NONE NONE NONE NONE NONE /./ ( \ st -> process_cmds cmdL update quit_check st st ) /.>/ finish /./ (\ ( state' , _ ) -> reTurn state' ) process_cmds cmdL update quit_check prev state = update prev state ./. x_get_cmd /./ exp `handle` err_handler where exp "Quit" = reTurn state {- = quit_check state /./ ( \ st -> if st then reTurn state else process_cmds cmdL update quit_check state state ) -} exp cmd = do_cmd cmdL state cmd /./ process_cmds cmdL update quit_check state {- = do_cmd cmdL state cmd /.>/ (x_show_tactics ./. reTurn (error "")) /./ ( \ ( st , _ ) -> process_cmds cmdL update quit_check state st ) -} err_handler s -- XError = x_error s /./ ( \ _ -> process_cmds cmdL update quit_check prev state ) -- clean_x {- err_handler _ = process_cmds cmdL update quit_check prev state /./ x_set_status "Can't execute command" --/./ -- clean_x -} {- Interrupt unimplemented Interrupt => ( x_error xio "Command Interrupt" ; process_cmds cmdL update quit_check xio prev state ) and catchTopCont () = ( System.Unsafe.toplevelcont := callcc (fn k => ( callcc (fn k' => (throw k k')); raise Interrupt))) -} do_cmd cmdL state cmd = case my_assocs cmd cmdL of SOME cmd_fn -> cmd_fn state NONE -> x_error ( "Bad command: " ++ cmd ) /./ ( \ _ -> reTurn state ) my_assocs :: String -> [(String,b)] -> Option b my_assocs key [] = NONE my_assocs key ((key',entry):l') | key == key' = SOME entry | otherwise = my_assocs key l'