1 module Editor where 2 3 import Core_datatype 4 import Kernel 5 import Lookup 6 7 import Vtslib 8 9 import X_interface 10 11 import Goals 12 import Globals -- partain 13 import Tags -- partain 14 15 import Edlib 16 17 import Type_defs 18 19 import Tree 20 21 22 23 24 editor cmdL initial update quit_check finish 25 = initial NONE NONE NONE NONE NONE /./ 26 ( \ st -> process_cmds cmdL update quit_check st st ) /.>/ 27 finish /./ 28 (\ ( state' , _ ) -> reTurn state' ) 29 30 process_cmds cmdL update quit_check prev state 31 = update prev state ./. 32 x_get_cmd /./ 33 exp 34 `handle` 35 err_handler 36 where 37 exp "Quit" 38 = reTurn state 39 {- 40 = quit_check state /./ 41 ( \ st -> if st then reTurn state 42 else process_cmds cmdL update 43 quit_check state state ) 44 -} 45 46 exp cmd 47 = do_cmd cmdL state cmd /./ 48 process_cmds cmdL update quit_check state 49 {- 50 = do_cmd cmdL state cmd /.>/ 51 (x_show_tactics ./. reTurn (error "")) /./ 52 ( \ ( st , _ ) -> process_cmds cmdL update quit_check state st ) 53 -} 54 55 err_handler s -- XError 56 = x_error s /./ 57 ( \ _ -> process_cmds cmdL update quit_check prev state ) 58 -- clean_x 59 60 61 {- 62 err_handler _ 63 = process_cmds cmdL update quit_check prev state /./ 64 x_set_status "Can't execute command" --/./ 65 -- clean_x 66 -} 67 68 {- Interrupt unimplemented 69 70 Interrupt => 71 ( 72 x_error xio "Command Interrupt" ; 73 process_cmds cmdL update quit_check xio prev state 74 ) 75 76 and catchTopCont () = ( 77 System.Unsafe.toplevelcont := 78 callcc (fn k => ( 79 callcc (fn k' => (throw k k')); 80 raise Interrupt))) 81 -} 82 83 84 85 do_cmd cmdL state cmd 86 = case my_assocs cmd cmdL of 87 SOME cmd_fn -> cmd_fn state 88 NONE -> x_error ( "Bad command: " ++ cmd ) /./ 89 ( \ _ -> reTurn state ) 90 91 my_assocs :: String -> [(String,b)] -> Option b 92 93 my_assocs key [] = NONE 94 95 my_assocs key ((key',entry):l') 96 | key == key' = SOME entry 97 | otherwise = my_assocs key l' 98