Source file source_manager.ml
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
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
type tab = {
tab_file : Datatype.Filepath.t ;
tab_page : int ;
tab_select : line:int -> unit ;
tab_source_view : GSourceView.source_view;
}
type t = {
notebook : GPack.notebook;
file_index : (Datatype.Filepath.t,tab) Hashtbl.t;
name_index : (string,tab) Hashtbl.t;
page_index : (int,tab) Hashtbl.t;
mutable pages : int ;
}
let make ?tab_pos ?packing () =
let notebook = GPack.notebook
~scrollable:true ~show_tabs:true ?tab_pos ?packing ()
in
notebook#set_enable_popup true ;
{
notebook = notebook ;
file_index = Hashtbl.create 7;
name_index = Hashtbl.create 7;
page_index = Hashtbl.create 7;
pages = 0 ;
}
let clear w =
begin
for _i=1 to w.pages do w.notebook#remove_page 0 done ;
w.pages <- 0 ;
Hashtbl.clear w.file_index ;
Hashtbl.clear w.name_index ;
Hashtbl.clear w.page_index ;
end
let later f = ignore (Glib.Idle.add (fun () -> f () ; false))
let select_file w filename =
try
let tab = Hashtbl.find w.file_index filename in
later (fun () -> w.notebook#goto_page tab.tab_page)
with Not_found -> ()
let select_name w title =
try
let tab = Hashtbl.find w.name_index title in
later (fun () -> w.notebook#goto_page tab.tab_page)
with Not_found -> ()
let selection_locked = ref false
let load_file w ?title ~(filename : Datatype.Filepath.t) ?(line=(-1)) ~click_cb () =
Gui_parameters.debug ~level:2 "Opening file \"%a\" line %d"
Datatype.Filepath.pretty filename line ;
let tab =
begin
try Hashtbl.find w.file_index filename
with Not_found ->
let name = match title with
| None -> Filepath.Normalized.to_pretty_string filename
| Some s -> s
in
let label = GMisc.label ~text:name () in
let sw = GBin.scrolled_window
~vpolicy:`AUTOMATIC
~hpolicy:`AUTOMATIC
~packing:(fun arg ->
ignore
(w.notebook#append_page ~tab_label:label#coerce arg))
() in
let original_source_view = Source_viewer.make ~name:"original_source"
~packing:sw#add ()
in
let window = (original_source_view :> GText.view) in
let page_num = w.notebook#page_num sw#coerce in
let scan_references = Kernel.EagerLoadSources.get () in
let s =
match Parse_env.open_source ~scan_references (filename :> string) with
| Error _msg ->
let f = Filepath.Normalized.to_pretty_string filename in
"Error: cannot open file '" ^ f ^ "'"
| Ok s -> s
in
let (buffer:GText.buffer) = window#buffer in
buffer#set_text s;
let select_line ~line =
if !selection_locked then
selection_locked := false
else
begin
w.notebook#goto_page page_num;
if line >= 0 then
let it = buffer#get_iter (`LINE (line-1)) in
buffer#place_cursor ~where:it;
let y = if buffer#line_count < 20 then 0.23 else 0.3 in
window#scroll_to_mark ~use_align:true ~yalign:y `INSERT
end
in
ignore (window#event#connect#button_press
~callback:
(fun ev ->
(if GdkEvent.Button.button ev = 1 &&
List.mem `CONTROL
(Gdk.Convert.modifier (GdkEvent.Button.state ev))
then
Wutil.later
(fun () ->
try
let cur_page = w.notebook#current_page in
let tab = Hashtbl.find w.page_index cur_page in
let file = tab.tab_file in
let iter = buffer#get_iter_at_mark `INSERT in
let line = iter#line + 1 in
Gtk_helper.open_in_external_viewer ~line file
with Not_found ->
failwith (Printf.sprintf "ctrl+click cb: invalid page %d"
w.notebook#current_page)
);
if GdkEvent.Button.button ev = 1 then
Wutil.later
(fun () ->
try
let iter = buffer#get_iter_at_mark `INSERT in
let line = iter#line + 1 in
let col = iter#line_index in
let offset = iter#offset in
let pos = {Filepath.pos_path = filename;
Filepath.pos_lnum = line;
Filepath.pos_bol = offset - col;
Filepath.pos_cnum = offset;} in
let localz =
Printer_tag.loc_to_localizable ~precise_col:true pos
in
click_cb localz
with Not_found ->
failwith (Printf.sprintf "click cb: invalid page %d"
w.notebook#current_page)
);
);
false
));
let tab = {
tab_file = filename ;
tab_select = select_line ;
tab_page = page_num ;
tab_source_view = original_source_view;
} in
w.pages <- succ page_num ;
Hashtbl.add w.file_index filename tab ;
Hashtbl.add w.name_index name tab ;
Hashtbl.add w.page_index page_num tab ;
tab
end
in
later (fun () -> tab.tab_select ~line)
let get_current_source_view w =
try
let tab = Hashtbl.find w.page_index w.notebook#current_page in
tab.tab_source_view
with Not_found ->
failwith (Printf.sprintf "get_source_view: invalid page %d"
w.notebook#current_page)