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
|