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