diff options
Diffstat (limited to 'ide/ideutils.ml')
| -rw-r--r-- | ide/ideutils.ml | 22 |
1 files changed, 16 insertions, 6 deletions
diff --git a/ide/ideutils.ml b/ide/ideutils.ml index 8ec0e9e4..dc3bcf71 100644 --- a/ide/ideutils.ml +++ b/ide/ideutils.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: ideutils.ml,v 1.30.2.1 2004/07/16 19:30:20 herbelin Exp $ *) +(* $Id: ideutils.ml,v 1.30.2.4 2006/01/06 15:40:37 barras Exp $ *) open Preferences @@ -32,7 +32,12 @@ let prerr_endline s = let prerr_string s = if !debug then (prerr_string s;flush stderr) -let lib_ide = Filename.concat Coq_config.coqlib "ide" +let lib_ide_file f = + let coqlib = + if !Options.boot then Coq_config.coqtop + else + System.getenv_else "COQLIB" Coq_config.coqlib in + Filename.concat (Filename.concat coqlib "ide") f let get_insert input_buffer = input_buffer#get_iter_at_mark `INSERT @@ -210,10 +215,15 @@ let find_tag_stop (tag :GText.tag) (it:GText.iter) = let find_tag_limits (tag :GText.tag) (it:GText.iter) = (find_tag_start tag it , find_tag_stop tag it) -(* explanations ?? *) +(* explanations: Win32 threads won't work if events are produced + in a thread different from the thread of the Gtk loop. In this + case we must use GtkThread.async to push a callback in the + main thread. Beware that the synchronus version may produce + deadlocks. *) let async = - if Sys.os_type <> "Unix" then GtkThread.async else - (fun x -> x) + if Sys.os_type = "Win32" then GtkThread.async else (fun x -> x) +let sync = + if Sys.os_type = "Win32" then GtkThread.sync else (fun x -> x) let stock_to_widget ?(size=`DIALOG) s = let img = GMisc.image () @@ -254,7 +264,7 @@ let browse f url = let url_for_keyword = let ht = Hashtbl.create 97 in begin try - let cin = open_in (Filename.concat lib_ide "index_urls.txt") in + let cin = open_in (lib_ide_file "index_urls.txt") in try while true do let s = input_line cin in try |