blob: 3edd65aacd7ba31b2611869b8f89850c10850b6e (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
|
open Preferences
exception Forbidden
let lib_ide = Filename.concat Coq_config.coqlib "ide"
let get_insert input_buffer = input_buffer#get_iter_at_mark `INSERT
let is_char_start c = let code = Char.code c in code < 0x80 || code >= 0xc0
let byte_offset_to_char_offset s byte_offset =
assert (byte_offset < String.length s);
let count_delta = ref 0 in
for i = 0 to byte_offset do
let code = Char.code s.[i] in
if code >= 0x80 && code < 0xc0 then incr count_delta
done;
byte_offset - !count_delta
let process_pending () =
while Glib.Main.pending () do
ignore (Glib.Main.iteration false)
done
let debug = ref true
let prerr_endline s =
if !debug then (prerr_endline s;flush stderr) else ()
let print_id id =
prerr_endline ("GOT sig id :"^(string_of_int (Obj.magic id)))
let try_convert s =
try
if Glib.Utf8.validate s then s else
(prerr_endline
"Coqide warning: input is not UTF-8 encoded. Trying to convert from locale.";
Glib.Convert.locale_to_utf8 s)
with _ ->
"(* Fatal error: wrong encoding in input.
Please set your locale according to your file encoding.*)"
let try_export file_name s =
try
let s = Glib.Convert.locale_from_utf8 s in
let oc = open_out file_name in
output_string oc s;
close_out oc
with e -> prerr_endline (Printexc.to_string e)
let browse url =
let l,r = current.cmd_browse in
ignore (Sys.command (l ^ url ^ r))
let url_for_keyword =
let ht = Hashtbl.create 97 in
begin try
let cin = open_in (Filename.concat lib_ide "index_urls.txt") in
try while true do
let s = input_line cin in
try
let i = String.index s ',' in
let k = String.sub s 0 i in
let u = String.sub s (i + 1) (String.length s - i - 1) in
Hashtbl.add ht k u
with _ ->
()
done with End_of_file ->
close_in cin
with _ ->
()
end;
(Hashtbl.find ht : string -> string)
let browse_keyword text =
try
let u = url_for_keyword text in browse (current.doc_url ^ u)
with _ -> ()
|
