module X_interface where import Edlib import Type_defs import Vtslib import Core_datatype {- (******************************************************************************) (* This is the definition of the X-interface. *) (******************************************************************************) -} data SubTermData = STData [Int] Int Int [SubTermData] data Form_input = InSingleText String String | InMultiText String String | InToggle String [( String , Bool )] | InRadio String Int [String] | InComment String | InSubterm String SubTermData data Form_output = OutText String | OutToggle [String] | OutRadio String | OutSubterm String --x_program = "/usr/nfs/hilbert/data/elr/nd1/X/src/newed/fe" {- (******************************************************************************) (* Define the escape sequences that control the interaction between SML *) (* and X *) (******************************************************************************) -} esc_seq = '\27' x_quit_esc_seq = "\27\&0" x_enable_esc_seq = "\27\&1" x_cmd_esc_seq = "\27\&2" x_display_esc_seq = "\27\&3" x_inter_arg_esc_seq = "\27\&4" x_end_arg_esc_seq = "\27\&5" x_error_esc_seq = "\27\&6" x_scratch_esc_seq = "\27\&7" x_form_esc_seq = "\27\&8" x_cancel_esc_seq = "\27\&9" x_single_text_esc_seq = "\27\&a" x_multi_text_esc_seq = "\27\&b" x_toggle_esc_seq = "\27\&c" x_radio_esc_seq = "\27\&d" x_comment_esc_seq = "\27\&e" x_multi_arg_esc_seq = "\27\&A" x_set_par_esc_seq = "\27\&B" x_set_nod_esc_seq = "\27\&C" x_set_rw_esc_seq = "\27\&D" x_set_don_esc_seq = "\27\&E" x_set_dis_esc_seq = "\27\&F" x_set_tac_esc_seq = "\27\&G" x_set_arg_esc_seq = "\27\&H" x_set_com_esc_seq = "\27\&I" x_set_sub_esc_seq = "\27\&J" x_set_sta_esc_seq = "\27\&K" x_unset_par_esc_seq = "\27\&L" x_bell_esc_seq = "\27\&M" x_tacs_up_esc_seq = "\27\&N" x_subtrm_esc_seq = "\27\&O" x_set_full_esc_seq = "\27\&P" x_unset_full_esc_seq = "\27\&Q" x_hide_main_esc_seq = "\27\&R" x_show_main_esc_seq = "\27\&T" -- GRIP x_send x_send s ins = (ins, s ) x_send_argL argL = x_send x_multi_arg_esc_seq ... x_send [toEnum (length argL)] ... app ( map x_send_arg argL ) ... x_send x_end_arg_esc_seq x_send_arg arg = x_send arg ... x_send x_inter_arg_esc_seq x_multi_send x_send_fn argL = x_send x_multi_arg_esc_seq ... x_send [toEnum (length argL)] ... app (map (x_multi_send_arg x_send_fn) argL) ... x_send x_end_arg_esc_seq x_multi_send_arg x_send_fn arg = x_send_fn arg ... x_send x_inter_arg_esc_seq x_get_argL = x_get_arg_no /./ x_get_i_args /.>/ x_get_esc_seq /./ (\ ( argL, esc ) -> if esc /= x_end_arg_esc_seq then return_err mesg else reTurn argL ) where mesg = "Bad argument terminator " x_get_i_args :: Int -> Xin -> Xst ( MayBe [String] String ) x_get_i_args 0 = reTurn [] x_get_i_args i = x_get_arg /.:>/ x_get_i_args (i-1) x_get_arg :: Xin -> Xst ( MayBe String String ) x_get_arg ( c : ist , rsps , glno ) | c == esc_seq = if [ c , c' ] == x_inter_arg_esc_seq then reTurn "" ( ist2, rsps , glno ) else return_err mesg ( ist2 , rsps , glno ) | otherwise = x_get_arg ( ist, rsps , glno ) /// (\ str -> reTurn ( c : str )) where mesg = "Bad argument escape" ( c' : ist2 ) = ist x_get_arg ( [] , _ , _ ) = error "stdin empty" x_get_arg_no = x_get_esc_seq /./ exp where exp esc_seq xin | esc_seq == x_multi_arg_esc_seq = reTurn ( fromEnum c ) ( ist , rsps , glno ) | otherwise = return_err "Expected multiple arguments" xin where ( c : ist , rsps , glno ) = case xin of ( [] , _ , _ ) -> error "xin empty" otherwise -> xin x_multi_get_arg x_get_fn = x_get_arg_no /./ x_multi_get_i_args x_get_fn /.>/ x_get_esc_seq /./ (\ ( argL, esc ) -> if esc /= x_end_arg_esc_seq then return_err mesg else reTurn argL ) where mesg = "Bad argument terminator " x_multi_get_i_args :: (Xin -> Xst ( MayBe b c )) -> Int -> Xin -> Xst ( MayBe [b] c ) x_multi_get_i_args x_get_fn 0 = reTurn [] x_multi_get_i_args x_get_fn i = x_get_fn /.:>/ x_multi_get_i_args x_get_fn (i-1) x_get_esc_seq ( a : b : ist , rsps , glno ) = reTurn [ a , b ] ( ist , rsps , glno ) end_x = x_send x_quit_esc_seq x_enable_buttons = x_send x_enable_esc_seq x_get_cmd = x_enable_buttons ./. x_get_esc_seq /.>/ x_get_argL /./ exp where exp ( esc_seq, argL ) | esc_seq /= x_cmd_esc_seq = return_err "Expected command" | otherwise = reTurn ( head argL ) x_display title display xin = ( \ ( xin , _ , xout ) -> ( xin , xout )) ( x_form False [InComment title, InMultiText "" display] xin ) {- = x_send x_display_esc_seq ... x_send_argL [title,display] -} x_error error_mesg = x_send x_error_esc_seq ... x_send_argL [error_mesg] ./. x_get_esc_seq /./ exp where exp esc_seq | esc_seq /= x_cancel_esc_seq = return_err "Expected cancel" | otherwise = reTurn ( error "" ) x_scratch str = x_send x_scratch_esc_seq ... x_send_argL [str] x_form answer infoL = x_send x_form_esc_seq ... x_send_bool answer ... x_multi_send x_send_info infoL ./. if answer then x_get_form else reTurn NONE x_set_parent done summary = x_send x_set_par_esc_seq ... x_send_argL [done,summary] x_unset_parent = x_send x_unset_par_esc_seq x_set_node node = x_send x_set_nod_esc_seq ... x_send_argL [node] x_set_rw rw = x_send x_set_rw_esc_seq ... x_send_argL [rw] x_set_done done = x_send x_set_don_esc_seq ... x_send_argL [done] x_set_goal :: String -> String -> Xio_fn x_set_goal done display -- used to be x_set_display = x_send x_set_dis_esc_seq ... x_send_argL [done,display] x_set_tactic tactic = x_send x_set_tac_esc_seq ... x_send_argL [tactic] x_set_argument arg = x_send x_set_arg_esc_seq ... x_send_argL [arg] x_set_comment comment = x_send x_set_com_esc_seq ... x_send_argL [comment] x_set_subgoals done_summaryL = x_send x_set_sub_esc_seq ... x_send_argL ( foldr flatten [] done_summaryL ) where flatten :: ( String , String ) -> [String] -> [String] flatten (done,summary) args = done : summary : args x_set_status status = x_send x_set_sta_esc_seq ... x_send_argL [status] x_bell = x_send x_bell_esc_seq x_show_tactics = x_send x_tacs_up_esc_seq x_show_window = x_send x_show_main_esc_seq x_hide_window = x_send x_hide_main_esc_seq bst True = "1" bst False = "0" x_send_bool True = x_send "1" x_send_bool False = x_send "0" x_send_info (InSingleText l s) = x_send x_single_text_esc_seq ... x_send_argL [l,s] x_send_info (InMultiText l s) = x_send x_multi_text_esc_seq ... x_send_argL [l,s] x_send_info (InToggle s sL) = x_send x_toggle_esc_seq ... x_send_argL [s] ... x_send_argL ( foldr (\ (x,y) z -> x : bst y : z ) [] sL ) x_send_info (InRadio s i sL) = x_send x_radio_esc_seq ... x_send_argL [s] ... x_send_num i ... x_send_argL sL x_send_info (InComment s) = x_send x_comment_esc_seq ... x_send_argL [s] x_send_info (InSubterm s sdata) = x_send x_subtrm_esc_seq ... x_send_argL [s] ... x_send_subtrm sdata x_send_toggle (s,b) = x_send_bool b ... x_send_arg s x_send_form [] = x_send x_end_arg_esc_seq x_send_form [info] = x_send_info info ... x_send x_end_arg_esc_seq x_send_form (info : infoL) = x_send_info info ... x_send x_inter_arg_esc_seq ... x_send_form infoL x_get_form = x_get_esc_seq /./ exp where exp esc_seq | esc_seq == x_cancel_esc_seq = reTurn NONE | esc_seq == x_form_esc_seq = x_multi_get_arg x_get_info /./ (\ arg -> reTurn ( SOME arg )) | otherwise = return_err " XError Expected form escape" x_get_info = x_get_esc_seq /.>/ x_get_argL /./ exp where exp ( esc_seq, argL ) | esc_seq == x_single_text_esc_seq || esc_seq == x_multi_text_esc_seq = reTurn ( OutText ( head argL )) | esc_seq == x_toggle_esc_seq = reTurn ( OutToggle argL ) | esc_seq == x_radio_esc_seq = reTurn ( OutRadio ( head argL )) | esc_seq == x_subtrm_esc_seq = reTurn ( OutSubterm ( head argL )) | otherwise = return_err " XError Bad form escape sequence" x_send_subtrm (STData iL i j stinfoL) = x_multi_send x_send_num iL ... x_send_num i ... x_send_num j ... x_multi_send x_send_subtrm stinfoL x_send_num i = x_send [ toEnum ((i `div` 256) `mod` 256) , toEnum (i `mod` 256) ] {- x_get_num ( msc : lsc : ist , rsps ) = x_send str ( ist , rsps ) ./. reTurn "" where str = show ( fromEnum msc * 256 + fromEnum lsc ) ++ "\n" -} x_set_full :: [Int] -> String -> String -> Xio_fn x_set_full (i:int) title display = x_send x_set_full_esc_seq ... x_send_argL [show i, title, display] x_unset_full = x_send x_unset_full_esc_seq