X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2FDEVEL%2Flablgtk%2Flablgtk_20000829-0.1.0%2Fapplications%2Fbrowser%2Fshell.ml;fp=helm%2FDEVEL%2Flablgtk%2Flablgtk_20000829-0.1.0%2Fapplications%2Fbrowser%2Fshell.ml;h=0000000000000000000000000000000000000000;hb=c7514aaa249a96c5fdd39b1123fbdb38d92f20b6;hp=fbe0f92a0ea785552bac60b9eb1d084e80475108;hpb=1c7fb836e2af4f2f3d18afd0396701f2094265ff;p=helm.git diff --git a/helm/DEVEL/lablgtk/lablgtk_20000829-0.1.0/applications/browser/shell.ml b/helm/DEVEL/lablgtk/lablgtk_20000829-0.1.0/applications/browser/shell.ml deleted file mode 100644 index fbe0f92a0..000000000 --- a/helm/DEVEL/lablgtk/lablgtk_20000829-0.1.0/applications/browser/shell.ml +++ /dev/null @@ -1,255 +0,0 @@ -(* $Id$ *) - -open GdkKeysyms -open Printf - -(* Nice history class. May reuse *) - -class ['a] history () = object - val mutable history = ([] : 'a list) - val mutable count = 0 - method empty = history = [] - method add s = count <- 0; history <- s :: history - method previous = - let s = List.nth history count in - count <- (count + 1) mod List.length history; - s - method next = - let l = List.length history in - count <- (l + count - 1) mod l; - List.nth history ((l + count - 1) mod l) -end - -(* The shell class. Now encapsulated *) - -let protect f x = try f x with _ -> () - -class shell ~prog ~args ~env ?packing ?show () = - let (in2,out1) = Unix.pipe () - and (in1,out2) = Unix.pipe () - and (err1,err2) = Unix.pipe () in - let _ = List.iter ~f:Unix.set_nonblock [out1;in1;err1] in -object (self) - val textw = GEdit.text ~editable:true ?packing ?show () - val pid = Unix.create_process_env - ~prog ~args ~env ~stdin:in2 ~stdout:out2 ~stderr:err2 - val out = Unix.out_channel_of_descr out1 - val h = new history () - val mutable alive = true - val mutable reading = false - val mutable input_start = 0 - method text = textw - method alive = alive - method kill () = - textw#set_editable false; - if alive then begin - alive <- false; - protect close_out out; - List.iter ~f:(protect Unix.close) [in1; err1; in2; out2; err2]; - try - Unix.kill ~pid ~signal:Sys.sigkill; - Unix.waitpid pid ~mode:[]; () - with _ -> () - end - method interrupt () = - if alive then try - reading <- false; - Unix.kill ~pid ~signal:Sys.sigint - with Unix.Unix_error _ -> () - method send s = - if alive then try - output_string out s; - flush out - with Sys_error _ -> () - method private read ~fd ~len = - try - let buf = String.create len in - let len = Unix.read fd ~buf ~pos:0 ~len in - if len > 0 then begin - textw#set_position textw#length; - self#insert (String.sub buf ~pos:0 ~len); - input_start <- textw#position; - end; - len - with Unix.Unix_error _ -> 0 - method history (dir : [`next|`previous]) = - if not h#empty then begin - if reading then begin - textw#delete_text ~start:input_start ~stop:textw#position; - end else begin - reading <- true; - input_start <- textw#position - end; - self#insert (if dir = `previous then h#previous else h#next); - end - val mutable lexing = false - method private lex ~start ~stop:e = - if not lexing && start < e then begin - lexing <- true; - Lexical.tag textw ~start ~stop:e; - lexing <- false - end - method insert ?(lex=true) text = - let start = Text.line_start textw in - textw#insert text; - if lex then self#lex ~start ~stop:(Text.line_end textw) - method private keypress c = - if not reading & c > " " then begin - reading <- true; - input_start <- textw#position - end - method private return () = - if reading then reading <- false - else input_start <- textw#position; - textw#set_position (Text.line_end textw); - let s = textw#get_chars ~start:input_start ~stop:textw#position in - h#add s; - self#send s; - self#send "\n" - method private paste () = - if not reading then begin - reading <- true; - input_start <- textw#position; - end - initializer - textw#event#connect#key_press ~callback: - begin fun ev -> - if GdkEvent.Key.keyval ev = _Return && GdkEvent.Key.state ev = [] - then self#return () - else self#keypress (GdkEvent.Key.string ev); - false - end; - textw#connect#after#insert_text ~callback: - begin fun s ~pos -> - if not lexing then - self#lex ~start:(Text.line_start textw ~pos:(pos - String.length s)) - ~stop:(Text.line_end textw ~pos) - end; - textw#connect#after#delete_text ~callback: - begin fun ~start:pos ~stop -> - if not lexing then - self#lex ~start:(Text.line_start textw ~pos) - ~stop:(Text.line_end textw ~pos) - end; - textw#event#connect#button_press ~callback: - begin fun ev -> - if GdkEvent.Button.button ev = 2 then self#paste (); - false - end; - textw#connect#destroy ~callback:self#kill; - GMain.Timeout.add ~ms:100 ~callback: - begin fun () -> - if alive then begin - List.iter [err1;in1] - ~f:(fun fd -> while self#read ~fd ~len:1024 = 1024 do () done); - true - end else false - end; - () -end - -(* Specific use of shell, for LablBrowser *) - -let shells : (string * shell) list ref = ref [] - -(* Called before exiting *) -let kill_all () = - List.iter !shells ~f:(fun (_,sh) -> if sh#alive then sh#kill ()); - shells := [] -let _ = at_exit kill_all - -let get_all () = - let all = List.filter !shells ~f:(fun (_,sh) -> sh#alive) in - shells := all; - all - -let may_exec prog = - try Unix.access prog ~perm:[Unix.X_OK]; true - with Unix.Unix_error _ -> false - -let f ~prog ~title = - let progargs = - List.filter ~f:((<>) "") (Str.split ~sep:(Str.regexp " ") prog) in - if progargs = [] then () else - let prog = List.hd progargs in - let path = try Sys.getenv "PATH" with Not_found -> "/bin:/usr/bin" in - let exec_path = Str.split ~sep:(Str.regexp":") path in - let prog = - if not (Filename.is_implicit prog) then - if may_exec prog then prog else "" - else - List.fold_left exec_path ~init:"" ~f: - begin fun acc dir -> - if acc <> "" then acc else - let prog = Filename.concat dir prog in - if may_exec prog then prog else acc - end - in - if prog = "" then () else - let reg = Str.regexp "TERM=" in - let env = Array.map (Unix.environment ()) ~f: - begin fun s -> - if Str.string_match ~pat:reg s ~pos:0 then "TERM=dumb" else s - end in - let load_path = - List.flatten (List.map !Config.load_path ~f:(fun dir -> ["-I"; dir])) in - let args = Array.of_list (progargs @ load_path) in - let current_dir = ref (Unix.getcwd ()) in - - let tl = GWindow.window ~title ~width:500 ~height:300 () in - let vbox = GPack.vbox ~packing:tl#add () in - let menus = GMenu.menu_bar ~packing:vbox#pack () in - let f = new GMenu.factory menus in - let accel_group = f#accel_group in - let file_menu = f#add_submenu "File" - and history_menu = f#add_submenu "History" - and signal_menu = f#add_submenu "Signal" in - - let hbox = GPack.hbox ~packing:vbox#add () in - let sh = new shell ~prog ~env ~args ~packing:hbox#add () in - let sb = - GRange.scrollbar `VERTICAL ~adjustment:sh#text#vadjustment - ~packing:hbox#pack () - in - - let f = new GMenu.factory file_menu ~accel_group in - f#add_item "Use..." ~callback: - begin fun () -> - File.dialog ~title:"Use File" ~filename:(!current_dir ^ "/") () ~callback: - begin fun name -> - current_dir := Filename.dirname name; - if Filename.check_suffix name ".ml" then - let cmd = "#use \"" ^ name ^ "\";;\n" in - sh#insert cmd; - sh#send cmd - end - end; - f#add_item "Load..." ~callback: - begin fun () -> - File.dialog ~title:"Load File" ~filename:(!current_dir ^ "/") () ~callback: - begin fun name -> - current_dir := Filename.dirname name; - if Filename.check_suffix name ".cmo" or - Filename.check_suffix name ".cma" - then - let cmd = Printf.sprintf "#load \"%s\";;\n" name in - sh#insert cmd; - sh#send cmd - end - end; - f#add_item "Import path" ~callback: - begin fun () -> - List.iter (List.rev !Config.load_path) - ~f:(fun dir -> sh#send (sprintf "#directory \"%s\";;\n" dir)) - end; - f#add_item "Close" ~key:_W ~callback:tl#destroy; - - let h = new GMenu.factory history_menu ~accel_group ~accel_modi:[`MOD1] in - h#add_item "Previous" ~key:_P ~callback:(fun () -> sh#history `previous); - h#add_item "Next" ~key:_N ~callback:(fun () -> sh#history `next); - let s = new GMenu.factory signal_menu ~accel_group in - s#add_item "Interrupt" ~key:_G ~callback:sh#interrupt; - s#add_item "Kill" ~callback:sh#kill; - shells := (title, sh) :: !shells; - tl#add_accel_group accel_group; - tl#show ()