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
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
|
(************************************************************************)
(* * The Coq Proof Assistant / The Coq Development Team *)
(* v * Copyright INRIA, CNRS and contributors *)
(* <O___,, * (see version control and CREDITS file for authors & dates) *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(* * (see LICENSE file for the text of the license) *)
(************************************************************************)
let all_bindings = ref []
(* example unicode bindings table:
[ ("\\pi", "π", None);
("\\lambdas", "λs", Some 4);
("\\lambda", "λ", Some 3);
("\\lake", "0", Some 2);
("\\lemma", "Lemma foo : x. Proof. Qed", Some 1); ] *)
(** Auxiliary function used by [load_files].
Takes as argument a valid path. *)
let process_file filename =
if not (Sys.file_exists filename) then begin
Ideutils.warning (Printf.sprintf "Warning: unicode bindings file '%s' was not found." filename)
end else begin
let ch = open_in filename in
begin try while true do
let line = input_line ch in
begin try
let chline = Scanf.Scanning.from_string line in
let (key,value) =
Scanf.bscanf chline "%s %s" (fun x y -> (x,y)) in
let prio =
try Scanf.bscanf chline " %d" (fun x -> Some x)
with Scanf.Scan_failure _ | Failure _ | End_of_file -> None
in
all_bindings := (key,value,prio)::!all_bindings;
(* Note: storing bindings in reverse order, flipping is done later *)
Scanf.Scanning.close_in chline;
with End_of_file -> () end;
done with End_of_file -> () end;
close_in ch
end
let load_files filenames =
let selected_filenames = ref [] in
let add f =
selected_filenames := f::!selected_filenames in
let warn_default_not_found () =
let dirs = Minilib.coqide_data_dirs () in
Ideutils.warning Format.(
asprintf
"@[Warning: the file 'ide/default.bindings' was not found in:@\n @[<v>%a@]@]."
(pp_print_list ~pp_sep:pp_print_cut pp_print_string) dirs) in
let warn_local_not_found () =
Ideutils.warning (Printf.sprintf
"Warning: the local configuration file 'coqide.bindings' was not found.") in
if filenames = [] then begin
(* If no argument is provided using [-unicode-bindings],
then use the default file and the local file, if it exists *)
begin match Preferences.get_unicode_bindings_default_file() with
| Some f -> add f
| None -> warn_default_not_found()
end;
begin match Preferences.get_unicode_bindings_local_file() with
| Some f -> add f
| None -> ()
end;
end else begin
(* If [-unicode-bindings] is used with a list of file, consider
these files in order, with a special treatment for the tokens
"default" and "local", which are replaced by the appropriate path. *)
let add_arg f =
match f with
| "default" ->
begin match Preferences.get_unicode_bindings_default_file() with
| Some f -> add f
| None -> warn_default_not_found()
end
| "local" ->
begin match Preferences.get_unicode_bindings_local_file() with
| Some f -> add f
| None -> warn_local_not_found()
end
| _ -> add f
in
List.iter add_arg filenames
end;
(* Files must be processed in order, to build the list of bindings
by iteratively consing entry to its head, the list being reversed
at the very end *)
let real_filenames = List.rev !selected_filenames in
List.iter process_file real_filenames;
all_bindings := List.rev !all_bindings
(* For debugging the list of unicode files loaded:
List.iter (fun f -> Printf.eprintf "%s\n" f) real_filenames; *)
(** Auxiliary function to test whether [s] is a prefix of [str];
Note that there might be overlap with wg_Completion::is_substring *)
let string_is_prefix s str =
let n = String.length s in
let m = String.length str in
if m < n
then false
else (s = String.sub str 0 n)
let lookup prefix =
let max_priority = 100000000 in
let cur_word = ref None in
let cur_prio = ref (max_priority+1) in
let test_binding (key, word, prio_opt) =
let prio =
match prio_opt with
| None -> max_priority
| Some p -> p
in
if string_is_prefix prefix key && prio < !cur_prio then begin
cur_word := Some word;
cur_prio := prio;
end in
List.iter test_binding !all_bindings;
!cur_word
(* For debugging the list of unicode bindings loaded:
let print_unicode_bindings () =
List.iter (fun (x,y,p) ->
Printf.eprintf "%s %s %d\n" x y (match p with None -> -1 | Some n -> n))
!all_bindings;
prerr_newline()
*)
|
