From 00b9d4ec3c6f8ccb1fb2fc0fd909b25c15e2dc44 Mon Sep 17 00:00:00 2001 From: Jim Fehrle Date: Sun, 10 Oct 2021 20:47:23 -0700 Subject: [PATCH] Review #2 --- ide/coqide/coq.ml | 1 - ide/coqide/coq.mli | 1 - ide/coqide/coqOps.ml | 6 --- ide/coqide/coqOps.mli | 2 - ide/coqide/coqide.ml | 79 ++++++++++------------------- ide/coqide/idetop.ml | 63 +++++++---------------- ide/coqide/protocol/interface.ml | 1 - ide/coqide/protocol/xmlprotocol.ml | 21 ++------ ide/coqide/protocol/xmlprotocol.mli | 1 - ide/coqide/wg_MessageView.ml | 5 -- ide/coqide/wg_MessageView.mli | 1 - plugins/ltac/pptactic.ml | 1 - plugins/ltac/tactic_debug.ml | 55 ++++++++++++++++---- vernac/debugHook.ml | 28 ++++++---- vernac/debugHook.mli | 36 +++---------- 15 files changed, 118 insertions(+), 183 deletions(-) diff --git a/ide/coqide/coq.ml b/ide/coqide/coq.ml index fd3ab0d0f1edb..cc7dbb55797ad 100644 --- a/ide/coqide/coq.ml +++ b/ide/coqide/coq.ml @@ -607,7 +607,6 @@ let init x = eval_call (Xmlprotocol.init x) let stop_worker x = eval_call (Xmlprotocol.stop_worker x) let proof_diff x = eval_call (Xmlprotocol.proof_diff x) let db_cmd x = eval_call ~db:true (Xmlprotocol.db_cmd x) -let db_loc x = eval_call ~db:true (Xmlprotocol.db_loc x) let db_upd_bpts x = eval_call ~db:true (Xmlprotocol.db_upd_bpts x) let db_continue x = eval_call ~db:true (Xmlprotocol.db_continue x) let db_stack x = eval_call ~db:true (Xmlprotocol.db_stack x) diff --git a/ide/coqide/coq.mli b/ide/coqide/coq.mli index f0c82924ba097..38ec3efe7b853 100644 --- a/ide/coqide/coq.mli +++ b/ide/coqide/coq.mli @@ -160,7 +160,6 @@ val search : Interface.search_sty -> Interface.search_rty query val init : Interface.init_sty -> Interface.init_rty query val proof_diff : Interface.proof_diff_sty -> Interface.proof_diff_rty query val db_cmd : Interface.db_cmd_sty -> Interface.db_cmd_rty query -val db_loc : Interface.db_loc_sty -> Interface.db_loc_rty query val db_upd_bpts: Interface.db_upd_bpts_sty-> Interface.db_upd_bpts_rty query val db_continue: Interface.db_continue_sty-> Interface.db_continue_rty query val db_stack : Interface.db_stack_sty -> Interface.db_stack_rty query diff --git a/ide/coqide/coqOps.ml b/ide/coqide/coqOps.ml index bf05b2fa1e914..19555f81d8047 100644 --- a/ide/coqide/coqOps.ml +++ b/ide/coqide/coqOps.ml @@ -140,8 +140,6 @@ object method process_next_phrase : unit task method process_db_cmd : string -> next:(Interface.db_cmd_rty Interface.value -> unit task) -> unit task - method process_db_loc : - next:(Interface.db_loc_rty Interface.value -> unit task) -> unit task method process_db_upd_bpts : ((string * int) * bool) list -> next:(Interface.db_upd_bpts_rty Interface.value -> unit task) -> unit task method process_db_continue : db_continue_opt -> @@ -768,10 +766,6 @@ object(self) let db_cmd = Coq.db_cmd cmd in Coq.bind db_cmd next - method process_db_loc ~next : unit Coq.task = - let db_loc = Coq.db_loc () in - Coq.bind db_loc next - method process_db_upd_bpts updates ~next : unit Coq.task = let db_upd_bpts = Coq.db_upd_bpts updates in Coq.bind db_upd_bpts next diff --git a/ide/coqide/coqOps.mli b/ide/coqide/coqOps.mli index 5add38e6e9d76..4da5a0ebe682b 100644 --- a/ide/coqide/coqOps.mli +++ b/ide/coqide/coqOps.mli @@ -18,8 +18,6 @@ object method process_next_phrase : unit task method process_db_cmd : string -> next:(Interface.db_cmd_rty Interface.value -> unit task) -> unit task - method process_db_loc : - next:(Interface.db_loc_rty Interface.value -> unit task) -> unit task method process_db_upd_bpts : ((string * int) * bool) list -> next:(Interface.db_upd_bpts_rty Interface.value -> unit task) -> unit task method process_db_continue : db_continue_opt -> diff --git a/ide/coqide/coqide.ml b/ide/coqide/coqide.ml index 617669a9a8a3b..c311fc4f98720 100644 --- a/ide/coqide/coqide.ml +++ b/ide/coqide/coqide.ml @@ -176,8 +176,6 @@ let db_cmd sn cmd = (sn.coqops#process_db_cmd cmd ~next:(function | _ -> Coq.return ())) (fun () -> Minilib.log "Coq busy, discarding db_cmd") -let forward_db_loc = ref ((fun _ -> failwith "forward_db_loc") - : session -> unit -> unit) let forward_db_stack = ref ((fun _ -> failwith "forward_db_stack") : session -> unit -> unit) let forward_db_vars = ref ((fun _ -> failwith "forward_db_vars") @@ -195,7 +193,6 @@ let create_session f = sn.debugger#set_forward_get_basename (fun _ -> sn.basename); Coq.set_restore_bpts sn.coqtop (fun _ -> !forward_restore_bpts sn); (sn.messages#route 0)#set_forward_send_db_cmd (db_cmd sn); - (sn.messages#route 0)#set_forward_send_db_loc (!forward_db_loc sn); (sn.messages#route 0)#set_forward_send_db_stack (!forward_db_stack sn); sn.debugger#set_forward_highlight_code (!forward_highlight_code sn); sn.debugger#set_forward_clear_db_highlight (clear_db_highlight sn); @@ -216,31 +213,6 @@ let db_upd_bpts updates sn = (sn.coqops#process_db_upd_bpts updates ~next:(function | _ -> Coq.return ())) (fun () -> Minilib.log "Coq busy, discarding db_upd_bpts") -(* figure out which breakpoint locations have changed because the script was edited *) -let calculate_bpt_updates () = - let fn = "ToplevelInput" in - let rec update_bpts sn upd bpts_res = function - | bp :: tl -> - let iter = sn.buffer#get_iter_at_mark (`NAME bp.mark_id) in - let has_tag = iter#has_tag Tags.Script.breakpoint in - let prev_byte_offset = bp.prev_byte_offset in - if not has_tag then begin - sn.buffer#delete_mark (`NAME bp.mark_id); (* remove *) - update_bpts sn (((fn, prev_byte_offset), false) :: upd) bpts_res tl - end else if iter#offset <> bp.prev_uni_offset then begin - bp.prev_uni_offset <- iter#offset; (* move *) - let byte_offset = Ideutils.buffer_off_to_byte_off sn.buffer iter#offset in - bp.prev_byte_offset <- byte_offset; - update_bpts sn (((fn, byte_offset), true) - :: ((fn, prev_byte_offset), false) :: upd) - (bp :: bpts_res) tl (* move *) - end else - update_bpts sn upd (bp :: bpts_res) tl (* no change, keep *) - | [] -> (List.rev upd, List.rev bpts_res) (* order matters *) - in - let upds = List.mapi (fun i sn -> update_bpts sn [] [] sn.breakpoints) notebook#pages in - upds - let reapply_bpts sn = (* breakpoints in this file *) let upds = List.map (fun bp -> @@ -785,6 +757,31 @@ let resume_debugger ?sid opt = true end else false +(* figure out which breakpoint locations have changed because the script was edited *) +let calculate_bpt_updates () = + let fn = "ToplevelInput" in + let rec update_bpts sn upd bpts_res = function + | bp :: tl -> + let iter = sn.buffer#get_iter_at_mark (`NAME bp.mark_id) in + let has_tag = iter#has_tag Tags.Script.breakpoint in + let prev_byte_offset = bp.prev_byte_offset in + if not has_tag then begin + sn.buffer#delete_mark (`NAME bp.mark_id); (* remove *) + update_bpts sn (((fn, prev_byte_offset), false) :: upd) bpts_res tl + end else if iter#offset <> bp.prev_uni_offset then begin + bp.prev_uni_offset <- iter#offset; (* move *) + let byte_offset = Ideutils.buffer_off_to_byte_off sn.buffer iter#offset in + bp.prev_byte_offset <- byte_offset; + update_bpts sn (((fn, byte_offset), true) + :: ((fn, prev_byte_offset), false) :: upd) + (bp :: bpts_res) tl (* move *) + end else + update_bpts sn upd (bp :: bpts_res) tl (* no change, keep *) + | [] -> (List.rev upd, List.rev bpts_res) (* order matters *) + in + let upds = List.map (fun sn -> update_bpts sn [] [] sn.breakpoints) notebook#pages in + upds + let maybe_update_breakpoints () = let upds = calculate_bpt_updates () in List.iter2 (fun sn (_, bpts) -> @@ -797,9 +794,8 @@ let maybe_update_breakpoints () = List.map (fun ((_, off), set) -> ((fn, off), set)) upd | None -> [] ) notebook#pages) in - match sn_upds with - | [] -> () - | upd -> Coq.add_do_when_ready sn.coqtop (fun _ -> db_upd_bpts upd sn) + if sn_upds <> [] then + Coq.add_do_when_ready sn.coqtop (fun _ -> db_upd_bpts sn_upds sn) ) notebook#pages upds module Nav = struct @@ -1044,27 +1040,6 @@ let highlight_code sn loc = let _ = forward_highlight_code := highlight_code -let db_loc sn _ = - Coq.add_do_when_ready sn.coqtop (fun _ -> - ignore @@ Coq.try_grab ~db:true sn.coqtop (sn.coqops#process_db_loc - ~next:(function - | Interface.Good Some (file, ints) -> -(* Printf.printf "db_loc returns %s: %d %d\n%!" file (List.hd ints) (List.nth ints 1);*) - highlight_code sn (file, List.hd ints, List.nth ints 1); - Coq.return () - | Interface.Good None -> -(* Printf.printf "db_loc returns None\n%!";*) - clear_db_highlight sn (); - Coq.return () - | Interface.Fail _ -> - Coq.return () - )) - (fun () -> Minilib.log "Coq busy, discarding db_loc") - ) - -let _ = forward_db_loc := db_loc - -(* todo: maybe combine with db_loc--don't need to call both *) let db_stack sn _ = Coq.add_do_when_ready sn.coqtop (fun _ -> ignore @@ Coq.try_grab ~db:true sn.coqtop (sn.coqops#process_db_stack diff --git a/ide/coqide/idetop.ml b/ide/coqide/idetop.ml index 4a762c3e4a774..5c3b74c0be396 100644 --- a/ide/coqide/idetop.ml +++ b/ide/coqide/idetop.ml @@ -418,10 +418,6 @@ let cvt_loc loc = end | None -> None (* nothing to highlight, e.g. not in a .v file *) -let db_loc () = - let open DebugHook in - cvt_loc debugger_state.cur_loc - let db_continue opt = let open DebugHook.Action in debug_cmd := match opt with @@ -432,22 +428,11 @@ let db_continue opt = | Interface.Interrupt -> Interrupt let db_upd_bpts updates = - let open DebugHook in -(* Printf.printf "before pid = %d # bpts set after = %d\n\n%!" (Unix.getpid ()) (IBPSet.cardinal !ide_breakpoints);*) List.iter (fun op -> let ((file, offset), opt) = op in - let bp = { file; offset } in - match opt with - | true -> - ide_breakpoints := IBPSet.add bp !ide_breakpoints; (* todo: error if already set? *) - DebugHook.update_bpt true bp - | false -> - ide_breakpoints := IBPSet.remove bp !ide_breakpoints; (* todo: error if not found? *) - DebugHook.update_bpt false bp +(* Printf.printf "db_upd %s %d %b\n%!" file offset opt;*) + DebugHook.upd_ide_bpt file offset opt; ) updates -(* IBPSet.iter (fun e -> Printf.printf "pid = %d file = %s offset = %d\n%!" (Unix.getpid ())*) -(* e.file e.offset) !ide_breakpoints;*) -(* Printf.printf "after pid = %d # bpts set after = %d\n\n%!" (Unix.getpid ()) (IBPSet.cardinal !ide_breakpoints)*) let format_frame text loc = @@ -476,35 +461,26 @@ let format_frame text loc = with _ -> text let db_stack () = - let open DebugHook in (* Printf.printf "server: db_stack call\n%!";*) - let s = debugger_state.get_stack () in - let rec shift s prev_loc res = - let ploc = cvt_loc prev_loc in - match s with - | (tacn, loc) :: tl -> - let tacn = if ploc = None then - tacn ^ " (no location)" - else - format_frame tacn prev_loc in - shift tl loc ((tacn, ploc) :: res) - | [] -> - match prev_loc with - | Some { Loc.line_nb } -> - (":" ^ (string_of_int line_nb), ploc) :: res - | None -> (": (no location)", ploc) :: res - in - List.rev (shift s debugger_state.cur_loc []) + let s = !DebugHook.forward_get_stack () in + List.map (fun (tac, loc) -> + let floc = cvt_loc loc in + match tac with + | Some tacn -> + let tacn = if loc = None then + tacn ^ " (no location)" + else + format_frame tacn loc in + (tacn, floc) + | None -> + match loc with + | Some { Loc.line_nb } -> + (":" ^ (string_of_int line_nb), floc) + | None -> (": (no location)", floc) + ) s let db_vars framenum = - let open DebugHook in - let open Names in -(* Printf.printf "server: db_vars call\n%!";*) - let vars = List.nth debugger_state.varmaps framenum in - List.map (fun b -> - let (id, v) = b in - (Id.to_string id, !forward_pr_value v) - ) (Id.Map.bindings vars) + !DebugHook.forward_get_vars framenum let get_options () = let table = Goptions.get_tables () in @@ -596,7 +572,6 @@ let eval_call c = Interface.search = interruptible search; Interface.proof_diff = interruptible proof_diff; Interface.db_cmd = db_cmd; - Interface.db_loc = db_loc; Interface.db_upd_bpts = db_upd_bpts; Interface.db_continue = db_continue; Interface.db_stack = db_stack; diff --git a/ide/coqide/protocol/interface.ml b/ide/coqide/protocol/interface.ml index 8f6ee121d7a0c..609b423b2bbc3 100644 --- a/ide/coqide/protocol/interface.ml +++ b/ide/coqide/protocol/interface.ml @@ -290,7 +290,6 @@ type handler = { annotate : annotate_sty -> annotate_rty; proof_diff : proof_diff_sty -> proof_diff_rty; db_cmd : db_cmd_sty -> db_cmd_rty; - db_loc : db_loc_sty -> db_loc_rty; db_upd_bpts : db_upd_bpts_sty -> db_upd_bpts_rty; db_continue : db_continue_sty -> db_continue_rty; db_stack : db_stack_sty -> db_stack_rty; diff --git a/ide/coqide/protocol/xmlprotocol.ml b/ide/coqide/protocol/xmlprotocol.ml index cff402ad43876..b445a84f6d17e 100644 --- a/ide/coqide/protocol/xmlprotocol.ml +++ b/ide/coqide/protocol/xmlprotocol.ml @@ -587,7 +587,6 @@ let print_ast_sty_t : print_ast_sty val_t = state_id_t let annotate_sty_t : annotate_sty val_t = string_t let proof_diff_sty_t : proof_diff_sty val_t = pair_t string_t state_id_t let db_cmd_sty_t : db_cmd_sty val_t = string_t -let db_loc_sty_t : db_loc_sty val_t = unit_t let db_upd_bpts_sty_t : db_upd_bpts_sty val_t = list_t (pair_t (pair_t string_t int_t) bool_t) let db_continue_sty_t : db_continue_sty val_t = db_cont_opt_t @@ -620,7 +619,6 @@ let print_ast_rty_t : print_ast_rty val_t = xml_t let annotate_rty_t : annotate_rty val_t = xml_t let proof_diff_rty_t : proof_diff_rty val_t = pp_t let db_cmd_rty_t : db_cmd_rty val_t = unit_t -let db_loc_rty_t : db_loc_rty val_t = option_t (pair_t string_t (list_t int_t)) let db_upd_bpts_rty_t : db_upd_bpts_rty val_t = unit_t let db_continue_rty_t : db_continue_rty val_t = unit_t let db_stack_rty_t : db_stack_rty val_t = @@ -651,7 +649,6 @@ let calls = [| "Annotate", ($)annotate_sty_t, ($)annotate_rty_t; "PDiff", ($)proof_diff_sty_t, ($)proof_diff_rty_t; "Db_cmd", ($)db_cmd_sty_t, ($)db_cmd_rty_t; - "Db_loc", ($)db_loc_sty_t, ($)db_loc_rty_t; "Db_upd_bpts",($)db_upd_bpts_sty_t, ($)db_upd_bpts_rty_t; "Db_continue",($)db_continue_sty_t, ($)db_continue_rty_t; "Db_stack", ($)db_stack_sty_t, ($)db_stack_rty_t; @@ -682,7 +679,6 @@ type 'a call = | Annotate : annotate_sty -> annotate_rty call | PDiff : proof_diff_sty -> proof_diff_rty call | Db_cmd : db_cmd_sty -> db_cmd_rty call - | Db_loc : db_loc_sty -> db_loc_rty call | Db_upd_bpts: db_upd_bpts_sty -> db_upd_bpts_rty call | Db_continue: db_continue_sty -> db_continue_rty call | Db_stack : db_stack_sty -> db_stack_rty call @@ -711,11 +707,10 @@ let id_of_call : type a. a call -> int = function | Annotate _ -> 18 | PDiff _ -> 19 | Db_cmd _ -> 20 - | Db_loc _ -> 21 - | Db_upd_bpts _-> 22 - | Db_continue _-> 23 - | Db_stack _ -> 24 - | Db_vars _ -> 25 + | Db_upd_bpts _-> 21 + | Db_continue _-> 22 + | Db_stack _ -> 23 + | Db_vars _ -> 24 let str_of_call c = pi1 calls.(id_of_call c) @@ -742,7 +737,6 @@ let print_ast x : print_ast_rty call = PrintAst x let annotate x : annotate_rty call = Annotate x let proof_diff x : proof_diff_rty call = PDiff x let db_cmd x : db_cmd_rty call = Db_cmd x -let db_loc x : db_loc_rty call = Db_loc x let db_upd_bpts x : db_upd_bpts_rty call = Db_upd_bpts x let db_continue x : db_continue_rty call = Db_continue x let db_stack x : db_stack_rty call = Db_stack x @@ -773,7 +767,6 @@ let abstract_eval_call : type a. _ -> a call -> a value = fun handler c -> | Annotate x -> mkGood (handler.annotate x) | PDiff x -> mkGood (handler.proof_diff x) | Db_cmd x -> mkGood (handler.db_cmd x) - | Db_loc x -> mkGood (handler.db_loc x) | Db_upd_bpts x-> mkGood (handler.db_upd_bpts x) | Db_continue x-> mkGood (handler.db_continue x) | Db_stack x -> mkGood (handler.db_stack x) @@ -805,7 +798,6 @@ let of_answer : type a. a call -> a value -> xml = function | Annotate _ -> of_value (of_value_type annotate_rty_t ) | PDiff _ -> of_value (of_value_type proof_diff_rty_t ) | Db_cmd _ -> of_value (of_value_type db_cmd_rty_t ) - | Db_loc _ -> of_value (of_value_type db_loc_rty_t ) | Db_upd_bpts _-> of_value (of_value_type db_upd_bpts_rty_t) | Db_continue _-> of_value (of_value_type db_continue_rty_t) | Db_stack _ -> of_value (of_value_type db_stack_rty_t ) @@ -836,7 +828,6 @@ let to_answer : type a. a call -> xml -> a value = function | Annotate _ -> to_value (to_value_type annotate_rty_t ) | PDiff _ -> to_value (to_value_type proof_diff_rty_t ) | Db_cmd _ -> to_value (to_value_type db_cmd_rty_t ) - | Db_loc _ -> to_value (to_value_type db_loc_rty_t ) | Db_upd_bpts _-> to_value (to_value_type db_upd_bpts_rty_t) | Db_continue _-> to_value (to_value_type db_continue_rty_t) | Db_stack _ -> to_value (to_value_type db_stack_rty_t ) @@ -866,7 +857,6 @@ let of_call : type a. a call -> xml = fun q -> | Annotate x -> mkCall (of_value_type annotate_sty_t x) | PDiff x -> mkCall (of_value_type proof_diff_sty_t x) | Db_cmd x -> mkCall (of_value_type db_cmd_sty_t x) - | Db_loc x -> mkCall (of_value_type db_loc_sty_t x) | Db_upd_bpts x-> mkCall (of_value_type db_upd_bpts_sty_t x) | Db_continue x-> mkCall (of_value_type db_continue_sty_t x) | Db_stack x -> mkCall (of_value_type db_stack_sty_t x) @@ -897,7 +887,6 @@ let to_call : xml -> unknown_call = | "Annotate" -> Unknown (Annotate (mkCallArg annotate_sty_t a)) | "PDiff" -> Unknown (PDiff (mkCallArg proof_diff_sty_t a)) | "Db_cmd" -> Unknown (Db_cmd (mkCallArg db_cmd_sty_t a)) - | "Db_loc" -> Unknown (Db_loc (mkCallArg db_loc_sty_t a)) | "Db_upd_bpts"-> Unknown (Db_upd_bpts(mkCallArg db_upd_bpts_sty_t a)) | "Db_continue"-> Unknown (Db_continue(mkCallArg db_continue_sty_t a)) | "Db_stack" -> Unknown (Db_stack (mkCallArg db_stack_sty_t a)) @@ -935,7 +924,6 @@ let pr_full_value : type a. a call -> a value -> string = fun call value -> matc | Annotate _ -> pr_value_gen (print annotate_rty_t ) value | PDiff _ -> pr_value_gen (print proof_diff_rty_t ) value | Db_cmd _ -> pr_value_gen (print db_cmd_rty_t ) value - | Db_loc _ -> pr_value_gen (print db_loc_rty_t ) value | Db_upd_bpts _-> pr_value_gen (print db_upd_bpts_rty_t) value | Db_continue _-> pr_value_gen (print db_continue_rty_t) value | Db_stack _ -> pr_value_gen (print db_stack_rty_t ) value @@ -964,7 +952,6 @@ let pr_call : type a. a call -> string = fun call -> | Annotate x -> return annotate_sty_t x | PDiff x -> return proof_diff_sty_t x | Db_cmd x -> return db_cmd_sty_t x - | Db_loc x -> return db_loc_sty_t x | Db_upd_bpts x-> return db_upd_bpts_sty_t x | Db_continue x-> return db_continue_sty_t x | Db_stack x -> return db_stack_sty_t x diff --git a/ide/coqide/protocol/xmlprotocol.mli b/ide/coqide/protocol/xmlprotocol.mli index 3e3940582c734..9c8ab32182698 100644 --- a/ide/coqide/protocol/xmlprotocol.mli +++ b/ide/coqide/protocol/xmlprotocol.mli @@ -39,7 +39,6 @@ val print_ast : print_ast_sty -> print_ast_rty call val annotate : annotate_sty -> annotate_rty call val proof_diff : proof_diff_sty -> proof_diff_rty call val db_cmd : db_cmd_sty -> db_cmd_rty call -val db_loc : db_loc_sty -> db_loc_rty call val db_upd_bpts : db_upd_bpts_sty -> db_upd_bpts_rty call val db_continue : db_continue_sty -> db_continue_rty call val db_stack : db_stack_sty -> db_stack_rty call diff --git a/ide/coqide/wg_MessageView.ml b/ide/coqide/wg_MessageView.ml index ad3f721f3c7bf..8ddb013f4af9c 100644 --- a/ide/coqide/wg_MessageView.ml +++ b/ide/coqide/wg_MessageView.ml @@ -45,7 +45,6 @@ class type message_view = method editable2 : bool method set_editable2 : bool -> unit method set_forward_send_db_cmd : (string -> unit) -> unit - method set_forward_send_db_loc : (unit -> unit) -> unit method set_forward_send_db_stack : (unit -> unit) -> unit method set_forward_show_debugger : (unit -> unit) -> unit end @@ -108,8 +107,6 @@ let message_view sid : message_view = lines in - let forward_send_db_loc = ref ((fun x -> failwith "forward_send_db_loc") - : unit -> unit) in let forward_send_db_stack = ref ((fun x -> failwith "forward_send_db_stack") : unit -> unit) in let forward_show_debugger = ref ((fun x -> failwith "forward_show_debugger") @@ -118,7 +115,6 @@ let message_view sid : message_view = (* Insert a prompt and make the buffer editable. *) let insert_ltac_debug_prompt ?(refresh=false) msg = if not refresh then begin - !forward_send_db_loc (); !forward_send_db_stack (); !forward_show_debugger (); end; @@ -269,7 +265,6 @@ let message_view sid : message_view = method editable2 = view#editable method set_editable2 v = view#set_editable v; view#set_cursor_visible v method set_forward_send_db_cmd f = forward_send_db_cmd := f - method set_forward_send_db_loc f = forward_send_db_loc := f method set_forward_send_db_stack f = forward_send_db_stack := f method set_forward_show_debugger f = forward_show_debugger := f end diff --git a/ide/coqide/wg_MessageView.mli b/ide/coqide/wg_MessageView.mli index 0d9d5e1dadec4..d886281626fb0 100644 --- a/ide/coqide/wg_MessageView.mli +++ b/ide/coqide/wg_MessageView.mli @@ -33,7 +33,6 @@ class type message_view = method editable2 : bool method set_editable2 : bool -> unit method set_forward_send_db_cmd : (string -> unit) -> unit - method set_forward_send_db_loc : (unit -> unit) -> unit method set_forward_send_db_stack : (unit -> unit) -> unit method set_forward_show_debugger : (unit -> unit) -> unit end diff --git a/plugins/ltac/pptactic.ml b/plugins/ltac/pptactic.ml index 510bff357900e..200516ae2624f 100644 --- a/plugins/ltac/pptactic.ml +++ b/plugins/ltac/pptactic.ml @@ -163,7 +163,6 @@ let string_of_genarg_arg (ArgumentType arg) = end | _ -> default - let () = DebugHook.forward_pr_value := pr_value Constrexpr.LevelSome let pr_with_occurrences pr c = Ppred.pr_with_occurrences pr keyword c let pr_red_expr env sigma pr c = Ppred.pr_red_expr_env env sigma pr keyword c diff --git a/plugins/ltac/tactic_debug.ml b/plugins/ltac/tactic_debug.ml index e1095f35a425c..b8890adb35437 100644 --- a/plugins/ltac/tactic_debug.ml +++ b/plugins/ltac/tactic_debug.ml @@ -202,7 +202,7 @@ let print_loc_tac tac = print_loc desc loc [@@@ocaml.warning "+32"] -let get_stack stack () = +let cvt_stack stack = List.map (fun k -> let (loc, k) = k in (* todo: compare to explain_ltac_call_trace below *) @@ -231,30 +231,42 @@ let pop_chunk trace = trace_chunks := List.tl !trace_chunks let prev_stack = ref (Some []) (* previous stopping point in debugger *) let prev_trace_chunks : ltac_trace list ref = ref [([], [])] + +type debugger_state = { + (* location of next code to execute, is not in stack *) + mutable cur_loc : Loc.t option; + (* yields the call stack *) + mutable stack : (string * Loc.t option) list; + (* variable value maps for each stack frame *) + mutable varmaps : Geninterp.Val.t Names.Id.Map.t list; +} + +let debugger_state = { cur_loc=None; stack=[]; varmaps=[] } + let save_loc tac varmap trace = (* Comm.print (print_loc_tac tac);*) let stack, varmaps = match trace with | Some (stack, varmaps) -> stack, varmaps | None -> [], [] in - DebugHook.(debugger_state.cur_loc <- CAst.(tac.loc)); + debugger_state.cur_loc <- CAst.(tac.loc); let (pstack, pvars) = List.fold_right (fun (s,v) (os, ov) -> (s @ os), (v @ ov)) !trace_chunks ([],[]) in - DebugHook.(debugger_state.get_stack <- get_stack (stack @ pstack)); - DebugHook.(debugger_state.varmaps <- varmap :: (varmaps @ pvars)) + debugger_state.stack <- cvt_stack (stack @ pstack); + debugger_state.varmaps <- varmap :: (varmaps @ pvars) (* Prints the goal and the command to be executed *) let goal_com tac varmap trace = save_loc tac varmap trace; Proofview.tclTHEN db_pr_goal - (if Comm.isTerminal () || DebugHook.(debugger_state.cur_loc) = None then + (if Comm.isTerminal () || debugger_state.cur_loc = None then (Proofview.tclLIFT (Comm.output (str "Going to execute:" ++ fnl () ++ prtac tac))) else Proofview.tclLIFT (Proofview.NonLogical.return ())) (* [run (new_ref _)] gives us a ref shared among [NonLogical.t] - expressions. It avoids parametrizing everything over a + expressions. It avoids parameterizing everything over a reference. *) let skipped = Proofview.NonLogical.run (Proofview.NonLogical.ref 0) let skip = Proofview.NonLogical.run (Proofview.NonLogical.ref 0) @@ -326,15 +338,14 @@ let rec prompt level = | Ignore -> failwith "Ignore" (* not possible *) let at_breakpoint tac = - let open DebugHook in let open Loc in - let checkbpt dirpath offset = + let check_bpt dirpath offset = (* Printf.printf "In tactic_debug, dirpath = %s offset = %d\n%!" dirpath bp;*) - BPSet.mem { dirpath; offset } !breakpoints + DebugHook.check_bpt dirpath offset in match CAst.(tac.loc) with - | Some {fname=InFile {dirpath=Some dirpath}; bp} -> checkbpt dirpath bp - | Some {fname=ToplevelInput; bp} -> checkbpt "Top" bp + | Some {fname=InFile {dirpath=Some dirpath}; bp} -> check_bpt dirpath bp + | Some {fname=ToplevelInput; bp} -> check_bpt "Top" bp | _ -> false [@@@ocaml.warning "-32"] @@ -677,3 +688,25 @@ let get_ltac_trace info = | Some trace -> Some (extract_ltac_trace ?loc trace) let () = CErrors.register_additional_error_info get_ltac_trace + +let get_stack () = + let rec shift s prev_loc res = + match s with + | (tacn, loc) :: tl -> + shift tl loc (((Some tacn), prev_loc) :: res) + | [] -> (None, prev_loc) :: res + in + List.rev (shift debugger_state.stack debugger_state.cur_loc []) + +let () = DebugHook.forward_get_stack := get_stack + +let get_vars framenum = + let open Names in +(* Printf.printf "server: db_vars call\n%!";*) + let vars = List.nth debugger_state.varmaps framenum in + List.map (fun b -> + let (id, v) = b in + (Id.to_string id, Pptactic.pr_value Constrexpr.LevelSome v) + ) (Id.Map.bindings vars) + +let () = DebugHook.forward_get_vars := get_vars diff --git a/vernac/debugHook.ml b/vernac/debugHook.ml index 51a3f992c75b6..269fe2b78ed00 100644 --- a/vernac/debugHook.ml +++ b/vernac/debugHook.ml @@ -95,7 +95,7 @@ end (* breakpoints as used by tactic_debug *) type breakpoint = { - dirpath : string; + dirpath : string; (* module dirpath *) offset : int; } @@ -108,6 +108,9 @@ module BPSet = CSet.Make(struct let breakpoints = ref BPSet.empty +let check_bpt dirpath offset = + BPSet.mem { dirpath; offset } !breakpoints + (* breakpoints as defined by the debugger IDE, using absolute file names *) type ide_breakpoint = { file : string; @@ -121,6 +124,7 @@ module IBPSet = CSet.Make(struct if c1 <> 0 then c1 else String.compare b1.file b2.file end) +(* breakpoints as defined by the debugger IDE, using absolute file names *) let ide_breakpoints = ref IBPSet.empty (** add or remove a single breakpoint. Maps the breakpoint from @@ -158,15 +162,19 @@ let refresh_bpts () = breakpoints := BPSet.empty; IBPSet.iter (update_bpt true) !ide_breakpoints -type debugger_state = { - mutable cur_loc : Loc.t option; - mutable get_stack : unit -> (string * Loc.t option) list; - mutable varmaps : Geninterp.Val.t Names.Id.Map.t list; -} - -let debugger_state = { cur_loc=None; get_stack=(fun () -> []); varmaps=[] } - -let forward_pr_value = ref (fun x -> failwith "forward_pr_value") +(** opt = true to add a breakpoint, false to remove *) +let upd_ide_bpt file offset opt = + let bp = { file; offset } in + match opt with + | true -> + ide_breakpoints := IBPSet.add bp !ide_breakpoints; (* todo: error if already set? *) + update_bpt true bp + | false -> + ide_breakpoints := IBPSet.remove bp !ide_breakpoints; (* todo: error if not found? *) + update_bpt false bp + +let forward_get_stack = ref (fun x -> failwith "forward_get_stack") +let forward_get_vars = ref (fun x -> failwith "forward_get_vars") let ltac_break = ref false (* causes the Ltac debugger to stop at the next step *) diff --git a/vernac/debugHook.mli b/vernac/debugHook.mli index 82e3a8a7c5b11..648ac0d0a08a5 100644 --- a/vernac/debugHook.mli +++ b/vernac/debugHook.mli @@ -50,40 +50,16 @@ module Intf : sig val get : unit -> t option end -(** breakpoints as used by tactic_debug *) -type breakpoint = { - dirpath : string; - offset : int; -} +(* set or clear a breakpoint at the given filepath and offset *) +val upd_ide_bpt : string -> int -> bool -> unit -module BPSet : CSet.S with type elt = breakpoint +(* test if (module dirpath, offset) has a breakpoint *) +val check_bpt : string -> int -> bool -val breakpoints : BPSet.t ref - -(** breakpoints as defined by the debugger IDE, using absolute file names *) -type ide_breakpoint = { - file : string; - offset : int; -} -module IBPSet : CSet.S with type elt = ide_breakpoint - -val ide_breakpoints : IBPSet.t ref - -val update_bpt : bool -> ide_breakpoint -> unit val refresh_bpts : unit -> unit -type debugger_state = { - (* location of next code to execute, is not in stack *) - mutable cur_loc : Loc.t option; - (* yields the call stack *) - mutable get_stack : unit -> (string * Loc.t option) list; - (* variable value maps for each stack frame *) - mutable varmaps : Geninterp.Val.t Names.Id.Map.t list; -} - -val debugger_state : debugger_state - -val forward_pr_value : (Geninterp.Val.t -> Pp.t) ref +val forward_get_stack : (unit -> (string option * Loc.t option) list) ref +val forward_get_vars : (int -> (string * Pp.t) list) ref val ltac_break : bool ref (** Set to true to cause the Ltac debugger to stop at the next step *)