Review #2

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)

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

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

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 ->

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

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;

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;

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

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