1 module X_interface where 2 3 import Edlib 4 5 import Type_defs 6 7 import Vtslib 8 9 import Core_datatype 10 11 {- 12 (******************************************************************************) 13 (* This is the definition of the X-interface. *) 14 (******************************************************************************) 15 -} 16 17 18 data SubTermData = STData [Int] Int Int [SubTermData] 19 20 data Form_input = InSingleText String String | 21 InMultiText String String | 22 InToggle String [( String , Bool )] | 23 InRadio String Int [String] | 24 InComment String | 25 InSubterm String SubTermData 26 27 data Form_output = OutText String | 28 OutToggle [String] | 29 OutRadio String | 30 OutSubterm String 31 32 33 --x_program = "/usr/nfs/hilbert/data/elr/nd1/X/src/newed/fe" 34 35 {- 36 (******************************************************************************) 37 (* Define the escape sequences that control the interaction between SML *) 38 (* and X *) 39 (******************************************************************************) 40 -} 41 42 esc_seq = '\27' 43 x_quit_esc_seq = "\27\&0" 44 x_enable_esc_seq = "\27\&1" 45 x_cmd_esc_seq = "\27\&2" 46 x_display_esc_seq = "\27\&3" 47 x_inter_arg_esc_seq = "\27\&4" 48 x_end_arg_esc_seq = "\27\&5" 49 x_error_esc_seq = "\27\&6" 50 x_scratch_esc_seq = "\27\&7" 51 x_form_esc_seq = "\27\&8" 52 x_cancel_esc_seq = "\27\&9" 53 x_single_text_esc_seq = "\27\&a" 54 x_multi_text_esc_seq = "\27\&b" 55 x_toggle_esc_seq = "\27\&c" 56 x_radio_esc_seq = "\27\&d" 57 x_comment_esc_seq = "\27\&e" 58 x_multi_arg_esc_seq = "\27\&A" 59 x_set_par_esc_seq = "\27\&B" 60 x_set_nod_esc_seq = "\27\&C" 61 x_set_rw_esc_seq = "\27\&D" 62 x_set_don_esc_seq = "\27\&E" 63 x_set_dis_esc_seq = "\27\&F" 64 x_set_tac_esc_seq = "\27\&G" 65 x_set_arg_esc_seq = "\27\&H" 66 x_set_com_esc_seq = "\27\&I" 67 x_set_sub_esc_seq = "\27\&J" 68 x_set_sta_esc_seq = "\27\&K" 69 x_unset_par_esc_seq = "\27\&L" 70 x_bell_esc_seq = "\27\&M" 71 x_tacs_up_esc_seq = "\27\&N" 72 x_subtrm_esc_seq = "\27\&O" 73 x_set_full_esc_seq = "\27\&P" 74 x_unset_full_esc_seq = "\27\&Q" 75 x_hide_main_esc_seq = "\27\&R" 76 x_show_main_esc_seq = "\27\&T" 77 78 79 -- GRIP x_send 80 81 x_send s ins 82 = (ins, s ) 83 84 85 86 87 88 89 90 91 x_send_argL argL 92 = x_send x_multi_arg_esc_seq ... 93 x_send [toEnum (length argL)] ... 94 app ( map x_send_arg argL ) ... 95 x_send x_end_arg_esc_seq 96 97 98 99 x_send_arg arg 100 = x_send arg ... 101 x_send x_inter_arg_esc_seq 102 103 104 x_multi_send x_send_fn argL 105 = x_send x_multi_arg_esc_seq ... 106 x_send [toEnum (length argL)] ... 107 app (map (x_multi_send_arg x_send_fn) argL) ... 108 x_send x_end_arg_esc_seq 109 110 111 112 x_multi_send_arg x_send_fn arg 113 = x_send_fn arg ... 114 x_send x_inter_arg_esc_seq 115 116 117 118 x_get_argL 119 = x_get_arg_no /./ 120 x_get_i_args /.>/ 121 x_get_esc_seq /./ 122 (\ ( argL, esc ) 123 -> if esc /= x_end_arg_esc_seq 124 then return_err mesg 125 else reTurn argL ) 126 where 127 mesg = "Bad argument terminator " 128 129 130 131 132 133 x_get_i_args :: Int -> Xin -> Xst ( MayBe [String] String ) 134 135 x_get_i_args 0 = reTurn [] 136 137 x_get_i_args i = x_get_arg /.:>/ 138 x_get_i_args (i-1) 139 140 141 142 143 x_get_arg :: Xin -> Xst ( MayBe String String ) 144 145 x_get_arg ( c : ist , rsps , glno ) 146 | c == esc_seq = if [ c , c' ] == x_inter_arg_esc_seq 147 then reTurn "" ( ist2, rsps , glno ) 148 else return_err mesg ( ist2 , rsps , glno ) 149 | otherwise = x_get_arg ( ist, rsps , glno ) /// 150 (\ str -> reTurn ( c : str )) 151 where 152 mesg = "Bad argument escape" 153 ( c' : ist2 ) = ist 154 155 x_get_arg ( [] , _ , _ ) = error "stdin empty" 156 157 158 159 x_get_arg_no 160 = x_get_esc_seq /./ exp 161 where 162 exp esc_seq xin 163 | esc_seq == x_multi_arg_esc_seq 164 = reTurn ( fromEnum c ) ( ist , rsps , glno ) 165 | otherwise 166 = return_err "Expected multiple arguments" xin 167 where 168 ( c : ist , rsps , glno ) 169 = case xin of 170 ( [] , _ , _ ) -> error "xin empty" 171 otherwise -> xin 172 173 174 175 x_multi_get_arg x_get_fn 176 = x_get_arg_no /./ 177 x_multi_get_i_args x_get_fn /.>/ 178 x_get_esc_seq /./ 179 (\ ( argL, esc ) 180 -> if esc /= x_end_arg_esc_seq 181 then return_err mesg 182 else reTurn argL ) 183 where 184 mesg = "Bad argument terminator " 185 186 187 188 189 x_multi_get_i_args :: (Xin -> Xst ( MayBe b c )) -> Int -> Xin 190 -> Xst ( MayBe [b] c ) 191 192 x_multi_get_i_args x_get_fn 0 = reTurn [] 193 194 x_multi_get_i_args x_get_fn i 195 = x_get_fn /.:>/ 196 x_multi_get_i_args x_get_fn (i-1) 197 198 199 200 201 x_get_esc_seq ( a : b : ist , rsps , glno ) 202 = reTurn [ a , b ] ( ist , rsps , glno ) 203 204 205 206 end_x = x_send x_quit_esc_seq 207 208 209 210 x_enable_buttons 211 = x_send x_enable_esc_seq 212 213 214 215 x_get_cmd 216 = x_enable_buttons ./. 217 x_get_esc_seq /.>/ 218 x_get_argL /./ 219 exp 220 where 221 exp ( esc_seq, argL ) 222 | esc_seq /= x_cmd_esc_seq 223 = return_err "Expected command" 224 | otherwise = reTurn ( head argL ) 225 226 227 228 229 x_display title display xin 230 = ( \ ( xin , _ , xout ) -> ( xin , xout )) 231 ( x_form False [InComment title, InMultiText "" display] xin ) 232 {- 233 = x_send x_display_esc_seq ... 234 x_send_argL [title,display] 235 -} 236 237 238 239 x_error error_mesg 240 = x_send x_error_esc_seq ... 241 x_send_argL [error_mesg] ./. 242 x_get_esc_seq /./ 243 exp 244 where 245 exp esc_seq 246 | esc_seq /= x_cancel_esc_seq 247 = return_err "Expected cancel" 248 | otherwise = reTurn ( error "" ) 249 250 251 252 x_scratch str 253 = x_send x_scratch_esc_seq ... 254 x_send_argL [str] 255 256 257 258 x_form answer infoL 259 = x_send x_form_esc_seq ... 260 x_send_bool answer ... 261 x_multi_send x_send_info infoL ./. 262 if answer then x_get_form 263 else reTurn NONE 264 265 266 267 x_set_parent done summary 268 = x_send x_set_par_esc_seq ... 269 x_send_argL [done,summary] 270 271 272 273 x_unset_parent = x_send x_unset_par_esc_seq 274 275 276 277 x_set_node node 278 = x_send x_set_nod_esc_seq ... 279 x_send_argL [node] 280 281 282 283 x_set_rw rw 284 = x_send x_set_rw_esc_seq ... 285 x_send_argL [rw] 286 287 288 289 x_set_done done 290 = x_send x_set_don_esc_seq ... 291 x_send_argL [done] 292 293 294 295 x_set_goal :: String -> String -> Xio_fn 296 297 x_set_goal done display -- used to be x_set_display 298 = x_send x_set_dis_esc_seq ... 299 x_send_argL [done,display] 300 301 302 303 x_set_tactic tactic 304 = x_send x_set_tac_esc_seq ... 305 x_send_argL [tactic] 306 307 308 309 x_set_argument arg 310 = x_send x_set_arg_esc_seq ... 311 x_send_argL [arg] 312 313 314 315 x_set_comment comment 316 = x_send x_set_com_esc_seq ... 317 x_send_argL [comment] 318 319 320 321 x_set_subgoals done_summaryL 322 = x_send x_set_sub_esc_seq ... 323 x_send_argL ( foldr flatten [] done_summaryL ) 324 where 325 flatten :: ( String , String ) -> [String] -> [String] 326 flatten (done,summary) args = done : summary : args 327 328 329 330 x_set_status status 331 = x_send x_set_sta_esc_seq ... 332 x_send_argL [status] 333 334 335 336 x_bell = x_send x_bell_esc_seq 337 338 339 340 x_show_tactics = x_send x_tacs_up_esc_seq 341 342 343 x_show_window 344 = x_send x_show_main_esc_seq 345 346 347 x_hide_window 348 = x_send x_hide_main_esc_seq 349 350 351 bst True = "1" 352 353 bst False = "0" 354 355 356 357 x_send_bool True = x_send "1" 358 359 x_send_bool False = x_send "0" 360 361 362 363 x_send_info (InSingleText l s) 364 = x_send x_single_text_esc_seq ... 365 x_send_argL [l,s] 366 367 x_send_info (InMultiText l s) 368 = x_send x_multi_text_esc_seq ... 369 x_send_argL [l,s] 370 371 x_send_info (InToggle s sL) 372 = x_send x_toggle_esc_seq ... 373 x_send_argL [s] ... 374 x_send_argL ( foldr (\ (x,y) z -> x : bst y : z ) [] sL ) 375 376 x_send_info (InRadio s i sL) 377 = x_send x_radio_esc_seq ... 378 x_send_argL [s] ... 379 x_send_num i ... 380 x_send_argL sL 381 382 x_send_info (InComment s) 383 = x_send x_comment_esc_seq ... 384 x_send_argL [s] 385 386 x_send_info (InSubterm s sdata) 387 = x_send x_subtrm_esc_seq ... 388 x_send_argL [s] ... 389 x_send_subtrm sdata 390 391 392 x_send_toggle (s,b) 393 = x_send_bool b ... 394 x_send_arg s 395 396 397 398 x_send_form [] 399 = x_send x_end_arg_esc_seq 400 401 x_send_form [info] 402 = x_send_info info ... 403 x_send x_end_arg_esc_seq 404 405 x_send_form (info : infoL) 406 = x_send_info info ... 407 x_send x_inter_arg_esc_seq ... 408 x_send_form infoL 409 410 411 412 x_get_form 413 = x_get_esc_seq /./ 414 exp 415 where 416 exp esc_seq 417 | esc_seq == x_cancel_esc_seq 418 = reTurn NONE 419 | esc_seq == x_form_esc_seq 420 = x_multi_get_arg x_get_info /./ 421 (\ arg -> reTurn ( SOME arg )) 422 | otherwise 423 = return_err " XError Expected form escape" 424 425 426 427 x_get_info 428 = x_get_esc_seq /.>/ 429 x_get_argL /./ 430 exp 431 where 432 exp ( esc_seq, argL ) 433 | esc_seq == x_single_text_esc_seq || 434 esc_seq == x_multi_text_esc_seq 435 = reTurn ( OutText ( head argL )) 436 | esc_seq == x_toggle_esc_seq 437 = reTurn ( OutToggle argL ) 438 | esc_seq == x_radio_esc_seq 439 = reTurn ( OutRadio ( head argL )) 440 | esc_seq == x_subtrm_esc_seq 441 = reTurn ( OutSubterm ( head argL )) 442 | otherwise 443 = return_err " XError Bad form escape sequence" 444 445 446 447 x_send_subtrm (STData iL i j stinfoL) 448 = x_multi_send x_send_num iL ... 449 x_send_num i ... 450 x_send_num j ... 451 x_multi_send x_send_subtrm stinfoL 452 453 454 455 x_send_num i 456 = x_send [ toEnum ((i `div` 256) `mod` 256) , toEnum (i `mod` 256) ] 457 458 459 {- 460 x_get_num ( msc : lsc : ist , rsps ) 461 = x_send str ( ist , rsps ) ./. 462 reTurn "" 463 where 464 str = show ( fromEnum msc * 256 + fromEnum lsc ) ++ "\n" 465 -} 466 467 468 469 x_set_full :: [Int] -> String -> String -> Xio_fn 470 471 x_set_full (i:int) title display 472 = x_send x_set_full_esc_seq ... 473 x_send_argL [show i, title, display] 474 475 476 477 x_unset_full = x_send x_unset_full_esc_seq