File: wg_Debugger.ml

package info (click to toggle)
coq 8.16.1%2Bdfsg-1
  • links: PTS, VCS
  • area: main
  • in suites: bookworm
  • size: 40,596 kB
  • sloc: ml: 219,376; sh: 3,545; python: 3,231; ansic: 2,529; makefile: 767; lisp: 279; javascript: 63; xml: 24; sed: 2
file content (355 lines) | stat: -rw-r--r-- 14,387 bytes parent folder | download | duplicates (2)
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
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
(************************************************************************)
(*         *   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)         *)
(************************************************************************)

type stack_t = (string * (string * int list) option) list
type vars_t = (string * Pp.t) list

class type debugger_view =
  object
    method coerce : GObj.widget
    method set_stack : stack_t -> unit
    method set_vars : vars_t -> unit
    method hide : unit -> unit
    method show : unit -> unit
    method set_forward_highlight_code : (string * int * int -> unit) -> unit
    method set_forward_clear_db_highlight : (unit -> unit) -> unit
    method set_forward_db_vars : (int -> unit) -> unit
    method set_forward_paned_pos : (int -> unit) -> unit
    method set_forward_get_basename : (unit -> string) -> unit
  end

let forward_keystroke = ref ((fun x -> failwith "forward_keystroke (db)")
    : Gdk.keysym * Gdk.Tags.modifier list -> int -> bool)

let find_string_col s l =
  match List.assoc s l with `StringC c -> c | _ -> assert false

let make_table_widget cd cb =
  let frame = GBin.scrolled_window ~hpolicy:`AUTOMATIC ~vpolicy:`AUTOMATIC () in
  let columns, store =
    let cols = new GTree.column_list in
    let columns = List.map (function
      | (`Int,n,_)    -> n, `IntC (cols#add Gobject.Data.int)
      | (`String,n,_) -> n, `StringC (cols#add Gobject.Data.string))
    cd in
    columns, GTree.tree_store cols in
  let data = GTree.view  (* todo: call "view" *)
      ~vadjustment:frame#vadjustment ~hadjustment:frame#hadjustment
      ~rules_hint:true ~headers_visible:false
      ~model:store ~packing:frame#add () in

  let selection = data#selection in
  selection#set_mode `MULTIPLE;
  let copy = GtkData.AccelGroup.parse "<Ctrl>C" in

  let vars_keypress_cb ev =
    let key_ev = Ideutils.filter_key ev in
    if key_ev = copy then begin
      let rows = selection#get_selected_rows in
      let get_value iter = store#get ~row:iter ~column:(find_string_col "Var" columns) in
      let buf = Buffer.create 100 in
      List.iter (fun row ->
          let iter = store#get_iter row in
          let depth = store#iter_depth iter in
          let top_iter = Option.default iter (store#iter_parent iter) in
          if depth = 0 || not (selection#iter_is_selected top_iter) then begin
            let value =
              if store#iter_has_child top_iter then
                (get_value top_iter) ^ "\n" ^
                (get_value (store#iter_children (Some top_iter)))
              else
                get_value top_iter
            in
            Buffer.add_string buf (value ^ "\n\n");
          end
        ) rows;
      (GData.clipboard Gdk.Atom.clipboard)#set_text (Buffer.contents buf);
      true
    end else
      false
  in
  let _ = data#event#connect#key_press ~callback:vars_keypress_cb in

(* FIXME: handle this using CSS *)
(*   let refresh clr = data#misc#modify_bg [`NORMAL, `NAME clr] in *)
(*   let _ = background_color#connect#changed ~callback:refresh in *)
(*   let _ = data#misc#connect#realize ~callback:(fun () -> refresh background_color#get) in *)
  let mk_rend c = GTree.cell_renderer_text [], ["text",c] in
  let cols =
    List.map2 (fun (_,c) (_,n,v) ->
      let c = match c with
        | `IntC c -> GTree.view_column ~renderer:(mk_rend c) ()
        | `StringC c -> GTree.view_column ~renderer:(mk_rend c) () in
      c#set_title n;
      c#set_visible v;
      c#set_sizing `AUTOSIZE;
      c)
    columns cd in
  List.iter (fun c -> ignore(data#append_column c)) cols;
  ignore @@ data#connect#row_activated ~callback:(fun tp vc -> cb columns store tp vc);
  let cb view ft = view#misc#modify_font (GPango.font_description_from_string ft) in
  Preferences.(stick text_font data (cb data));
  frame, (fun f -> f columns store), store

let debugger title sid =
  let forward_set_paned_pos = ref ((fun x -> failwith "forward_set_paned_pos")
    : int -> unit) in

  let forward_get_basename = ref ((fun x -> failwith "forward_get_basename")
    : unit -> string) in

  let debugger_detachable = Wg_Detachable.detachable ~title () in
  debugger_detachable#close_button#misc#show ();
  ignore(debugger_detachable#close_button#connect#clicked
    ~callback:(fun _ -> !forward_set_paned_pos 1000000));

  let paned = GPack.paned `HORIZONTAL ~packing:(debugger_detachable#pack ~expand:true) () in

  let stack_view = GText.view ~editable:false ~cursor_visible:false ~wrap_mode:`NONE () in
  let stack_buffer = stack_view#buffer in
  let stack = ref [] in

  let vb_stack = GPack.vbox ~packing:(paned#pack1 ~shrink:false ~resize:true) () in
  let _ = GMisc.label ~text:"Call Stack" ~xalign:0.02 (* todo: use padding instead of xalign *)
    ~packing:(vb_stack#pack ~expand:false ~fill:true ~padding:3) () in
  let stack_scroll = GBin.scrolled_window
    ~vpolicy:`AUTOMATIC ~hpolicy:`AUTOMATIC ~packing:(vb_stack#pack ~expand:true) () in
  stack_scroll#add stack_view#coerce;

  let tree, access, store =
    make_table_widget
      [`String, "Var", true]
      (fun columns store tp vc ->
        let row = store#get_iter tp in
        let _ = store#get ~row ~column:(find_string_col "Var" columns) in ()) in

  let vars_view = GText.view ~editable:false ~cursor_visible:false ~wrap_mode:`NONE () in
  let cb view ft = view#misc#modify_font (GPango.font_description_from_string ft) in
  Preferences.(stick text_font vars_view (cb vars_view));
  Preferences.(stick text_font stack_view (cb stack_view));

  let vars = ref [] in

  let vb_vars = GPack.vbox ~packing:(paned#pack2 ~shrink:false ~resize:true) () in
  let _ = GMisc.label ~text:"Variables" ~xalign:0.02 (* todo: use padding instead of xalign *)
    ~packing:(vb_vars#pack ~expand:false ~fill:true ~padding:3) () in
  let () = vb_vars#pack ~expand:true tree#coerce in

(* doesn't help, not getting the correct widths
  ignore @@ Glib.Idle.add (fun _ ->
    let open Gtk in
    let open GtkBase in
    let dwidth = (Widget.allocation debugger_detachable#as_widget).width in
    let bwidth = (Widget.allocation debugger_detachable#close_button#as_widget).width in
    Printf.printf "dwidth = %d bwidth = %d\n%!" dwidth bwidth;
    paned #set_position (dwidth/2 - bwidth);
    false);
*)

  let highlighted_line = ref None in
  let forward_highlight_code = ref ((fun x -> failwith "forward_highlight_code")
    : (string * int * int) -> unit) in
  let forward_clear_db_highlight = ref ((fun x -> failwith "forward_clear_db_highlight")
    : unit -> unit) in
  let forward_db_vars = ref ((fun x -> failwith "forward_db_vars")
    : int -> unit) in

  (* workaround *)
  let relayout () =
    paned#remove vb_stack#coerce; (* appears not to be destroyed *)
    paned#remove vb_vars#coerce;
    paned#pack1 ~shrink:false ~resize:true vb_stack#coerce;
    paned#pack2 ~shrink:false ~resize:true vb_vars#coerce;
  in

  let attach_cb _ =
    debugger_detachable#show;
    relayout ()
  in
  let () = debugger_detachable#connect#attached ~callback:attach_cb in

  let detach_cb _ =
    let open Gtk in
    let open GtkBase in
    let alloc = Widget.allocation debugger_detachable#as_widget in
    ignore @@ Glib.Idle.add (fun _ ->
      debugger_detachable#win#resize ~width:alloc.width ~height:alloc.height;
      false);
    relayout ();
    !forward_set_paned_pos 1000000;  (* looks OK but debugger_paned in main window is still resizable *)
  in
  let () = debugger_detachable#connect#detached ~callback:detach_cb in

  (* todo: better to share with Tags.Script.debugging, but it isn't set for GText *)
  let debugging_tag = stack_buffer#create_tag
    [ `BACKGROUND_SET true; `BACKGROUND Preferences.db_stopping_point_color#get;
      `FOREGROUND_SET true; `FOREGROUND "white"] in

  let clear_highlight () =
    let start = stack_buffer#get_iter `START in
    let stop = stack_buffer#get_iter `END in
    stack_buffer#remove_tag debugging_tag ~start ~stop;
    highlighted_line := None
  in

  let highlight line =
    if line < List.length !stack then begin
      let start = stack_buffer#get_iter (`LINE line) in
      let stop = stack_buffer#get_iter (`LINE (line+1)) in
      stack_buffer#apply_tag debugging_tag ~start ~stop;
      highlighted_line := Some line;
      let (_, loc) = List.nth !stack line in
      !forward_db_vars line;
      match loc with
      | Some (file, bp :: ep :: _) ->
        !forward_highlight_code (file, bp, ep)
      | _ -> !forward_clear_db_highlight ()  (* e.g. for simple tactic call *)
    end
  in

  let up = GtkData.AccelGroup.parse "Up" in
  let down = GtkData.AccelGroup.parse "Down" in

  let stack_keypress_cb ev =
    let move dir =
      match !highlighted_line with
      | Some l ->
        let line = l+dir in
        if line >= 0 && line < List.length !stack then
          (clear_highlight (); highlight line)
      | None -> ()
    in

    let key_ev = Ideutils.filter_key ev in
    if key_ev = up then
      (move (-1); true)
    else if key_ev = down then
      (move 1; true)
    else
      !forward_keystroke key_ev sid (* support some function keys when Debugger is detached *)
  in
  let _ = stack_view#event#connect#key_press ~callback:stack_keypress_cb in

  let keypress_cb2 ev =
    let key_ev = Ideutils.filter_key ev in
    !forward_keystroke key_ev sid (* support some function keys when Debugger is detached *)
  in
  let _ = paned#event#connect#key_press ~callback:keypress_cb2 in

  (* click handler *)
  let click_cb ev =
    let open GdkEvent.Button in
    let y = y ev in
    let button = button ev in
    let scroll_pos = stack_scroll#vadjustment#value in
    let metrics = stack_view#coerce#misc#pango_context#get_metrics () in
    let line_height = GPango.to_pixels (metrics#ascent+metrics#descent) in
    let line = (truncate (y +. scroll_pos))/line_height in
    if button = 1 && line < List.length !stack then
      (clear_highlight (); highlight line);
    false (* let the panel get the focus *)
  in
  let _ = stack_view#event#connect#button_press ~callback:click_cb in

  let debugger = object (self)

    method coerce = debugger_detachable#coerce
    method set_stack (stack_v : stack_t) =
      stack := if stack_v = [] then [] else begin
        (* adjust text in the bottom frame of the stack *)
        let rs = List.rev stack_v in
        let (text, loc) = List.hd rs in
        match loc with
          | Some (_, locs) ->
            let basename = !forward_get_basename () in
            let basename = if basename = "*scratch*" then "Top" else basename in
            let s = Printf.sprintf "%s, %s" text basename in
            List.rev ((s, loc) :: (List.tl rs))
          | _ -> stack_v
      end;
      stack_buffer#set_text
        (String.concat "\n" (List.map (fun i -> let (tacn, loc) = i in tacn) !stack));
      clear_highlight ();
      if !stack <> [] then
        highlight 0

    method set_vars (vars_v : vars_t) =
      (* workaround: zero entries may show stale data GTK! :-( *)
      vars := if vars_v = [] then [("", Pp.mt ())] else vars_v;
      store#clear ();
      let cwidth () =
        let open Gtk in
        let open GtkBase in
        let pixel_width = (Widget.allocation tree#as_widget).width in
        let metrics = vars_view#misc#pango_context#get_metrics ()  in
        let char_width = GPango.to_pixels metrics#approx_char_width in
        (pixel_width - 100) / char_width
      in
      let print_pp width pp =
        let pp_buffer = Buffer.create 180 in
        let open Format in
        let ft = formatter_of_buffer pp_buffer in
        pp_set_margin ft width;
        pp_set_max_indent ft width;
      (*  pp_set_max_boxes ft 50 ;*)
      (*  pp_set_ellipsis_text ft "..."*)
        Pp.pp_with ft pp;
        pp_print_flush ft ();
        Buffer.contents pp_buffer
      in
      let show width =
        let insert = store#get_iter_first = None in
        let path = GtkTree.TreePath.from_string "0" in
        List.iter (fun (name, value) ->
            let width = max width 30 in
            let value = print_pp width value in
            access (fun columns store ->
                let column = (find_string_col "Var" columns) in
                let row = if insert then store#append () else store#get_iter path in
                GtkTree.TreePath.next path;
                if String.length value < width && (not (String.contains value '\n')) then begin
                  let text = if name = "" then " " else (name ^ " = " ^ value) in
                  store#set ~row ~column text;
                  if store#iter_has_child row then
                    ignore @@ store#remove (store#iter_children (Some row));
                end else begin
                  store#set ~row ~column (name ^ " = ");
                  let row2 = if insert || (not (store#iter_has_child row)) then
                    store#append ~parent:row ()
                  else
                    store#iter_children (Some row) in
                  store#set ~row:row2 ~column:(find_string_col "Var" columns) value
                end
              )
          ) !vars
      in
      let width = cwidth () in
      let pwidth = ref width in (* initially negative if not allocated *)
      if paned#position > 0 then show width;

      let w_cb (_ : Gtk.rectangle) =
        let width = cwidth () in
        if width <> !pwidth then begin
          pwidth := width;
          show width
        end
      in
      ignore (paned#misc#connect#size_allocate ~callback:w_cb)

    method hide () = debugger_detachable#hide  (* todo: give up focus *)
    method show () = debugger_detachable#show  (* todo: take focus? *)
    method set_forward_highlight_code f = forward_highlight_code := f
    method set_forward_clear_db_highlight f = forward_clear_db_highlight := f
    method set_forward_db_vars f = forward_db_vars := f
    method set_forward_paned_pos f = forward_set_paned_pos := f
    method set_forward_get_basename f = forward_get_basename := f
  end
  in
  debugger