src/Pure/Tools/debugger.ML

vacuous input means continue, e.g. after exit;

(*  Title:      Pure/Tools/debugger.ML
    Author:     Makarius

Interactive debugger for Isabelle/ML.
*)

signature DEBUGGER =
sig
  val writeln_message: string -> unit
  val warning_message: string -> unit
  val error_message: string -> unit
end;

structure Debugger: DEBUGGER =
struct

(** global state **)

(* output messages *)

val _ = Session.protocol_handler "isabelle.Debugger$Handler";

fun output_message kind msg =
  if msg = "" then ()
  else
    Output.protocol_message
      (Markup.debugger_output (Simple_Thread.the_name ()))
      [Markup.markup (kind, Markup.serial_properties (serial ())) msg];

val writeln_message = output_message Markup.writelnN;
val warning_message = output_message Markup.warningN;
val error_message = output_message Markup.errorN;

fun error_wrapper e = e ()
  handle exn =>
    if Exn.is_interrupt exn then reraise exn
    else error_message (Runtime.exn_message exn);


(* thread input *)

val thread_input =
  Synchronized.var "Debugger.state" (NONE: string list Queue.T Symtab.table option);

fun init_input () = Synchronized.change thread_input (K (SOME Symtab.empty));
fun exit_input () = Synchronized.change thread_input (K NONE);

fun input thread_name msg =
  if null msg then error "Empty input"
  else
    Synchronized.change thread_input
      (Option.map (Symtab.map_default (thread_name, Queue.empty) (Queue.enqueue msg)));

fun get_input thread_name =
  Synchronized.guarded_access thread_input
    (fn NONE => SOME ([], NONE)
      | SOME input =>
          (case Symtab.lookup input thread_name of
            NONE => NONE
          | SOME queue =>
              let
                val (msg, queue') = Queue.dequeue queue;
                val input' =
                  if Queue.is_empty queue' then Symtab.delete_safe thread_name input
                  else Symtab.update (thread_name, queue') input;
              in SOME (msg, SOME input') end));



(** thread state **)

(* stack frame during debugging *)

local
  val tag = Universal.tag () : ML_Debugger.state list Universal.tag;
in

fun get_debugging () = the_default [] (Thread.getLocal tag);
val is_debugging = not o null o get_debugging;

fun with_debugging e =
  setmp_thread_data tag (get_debugging ()) (ML_Debugger.state (Thread.self ())) e ();

end;

fun the_debug_state thread_name index =
  (case get_debugging () of
    [] => error ("Missing debugger information for thread " ^ quote thread_name)
  | states =>
      if index < 0 orelse index >= length states then
        error ("Bad debugger stack index " ^ signed_string_of_int index ^ " for thread " ^
          quote thread_name)
      else nth states index);


(* flags for single-stepping *)

datatype stepping = Stepping of bool * int;  (*stepping enabled, stack depth limit*)

local
  val tag = Universal.tag () : stepping Universal.tag;
in

fun get_stepping () = the_default (Stepping (false, ~1)) (Thread.getLocal tag);
fun put_stepping stepping = Thread.setLocal (tag, Stepping stepping);

end;

fun is_stepping () =
  let
    val stack = ML_Debugger.state (Thread.self ());
    val Stepping (stepping, depth) = get_stepping ();
  in stepping andalso (depth < 0 orelse length stack <= depth) end;

fun continue_stepping () = put_stepping (false, ~1);
fun step_stepping () = put_stepping (true, ~1);
fun step_over_stepping () = put_stepping (true, length (get_debugging ()));
fun step_out_stepping () = put_stepping (true, length (get_debugging ()) - 1);


(** eval ML **)

local

val context_attempts =
  map ML_Lex.read
   ["Context.set_thread_data (SOME (Context.Theory ML_context))",
    "Context.set_thread_data (SOME (Context.Proof ML_context))",
    "Context.set_thread_data (SOME ML_context)"];

fun evaluate {SML, verbose} =
  ML_Context.eval
    {SML = SML, exchange = false, redirect = false, verbose = verbose,
      writeln = writeln_message, warning = warning_message}
    Position.none;

in

fun eval thread_name index SML txt1 txt2 =
  let
    val (toks1, toks2) = apply2 (ML_Lex.read_source SML o Input.string) (txt1, txt2);

    val evaluate_verbose = evaluate {SML = SML, verbose = true};
    val context1 = ML_Context.the_generic_context ()
      |> Context_Position.set_visible_generic false
      |> Config.put_generic ML_Options.debugger false
      |> ML_Env.add_name_space {SML = SML}
          (ML_Debugger.debug_name_space (the_debug_state thread_name index));
    val context2 =
      if SML orelse forall (fn Antiquote.Text tok => ML_Lex.is_improper tok | _ => false) toks1
      then context1
      else
        let
          val context' = context1
            |> ML_Context.exec (fn () => evaluate_verbose (ML_Lex.read "val ML_context = " @ toks1));
          fun try_exec toks =
            try (ML_Context.exec (fn () => evaluate {SML = false, verbose = false} toks)) context';
        in
          (case get_first try_exec context_attempts of
            SOME context2 => context2
          | NONE => error "Malformed context: expected type theory, Proof.context, Context.generic")
        end;
  in Context.setmp_thread_data (SOME context2) evaluate_verbose toks2 end;

end;



(** debugger loop **)

local

fun debugger_state thread_name =
  Output.protocol_message (Markup.debugger_state thread_name)
   [get_debugging ()
    |> map (fn st =>
      (Position.properties_of (Exn_Properties.position_of (ML_Debugger.debug_location st)),
       ML_Debugger.debug_function st))
    |> let open XML.Encode in list (pair properties string) end
    |> YXML.string_of_body];

fun debugger_command thread_name =
  (case get_input thread_name of
    [] => (continue_stepping (); false)
  | ["continue"] => (continue_stepping (); false)
  | ["step"] => (step_stepping (); false)
  | ["step_over"] => (step_over_stepping (); false)
  | ["step_out"] => (step_out_stepping (); false)
  | ["eval", index, SML, txt1, txt2] =>
     (error_wrapper (fn () =>
        eval thread_name (Markup.parse_int index) (Markup.parse_bool SML) txt1 txt2); true)
  | bad =>
     (Output.system_message
        ("Debugger: bad input " ^ ML_Syntax.print_list ML_Syntax.print_string bad); true));

in

fun debugger_loop thread_name =
  uninterruptible (fn restore_attributes => fn () =>
    let
      fun loop () =
        (debugger_state thread_name; if debugger_command thread_name then loop () else ());
      val result = Exn.capture (restore_attributes with_debugging) loop;
      val _ = debugger_state thread_name;
    in Exn.release result end) ();

end;



(** protocol commands **)

val _ =
  Isabelle_Process.protocol_command "Debugger.init"
    (fn [] =>
     (init_input ();
      ML_Debugger.on_breakpoint
        (SOME (fn (_, break) =>
          if not (is_debugging ()) andalso (! break orelse is_stepping ()) then
            (case Simple_Thread.get_name () of
              SOME thread_name => debugger_loop thread_name
            | NONE => ())
          else ()))));

val _ =
  Isabelle_Process.protocol_command "Debugger.exit"
    (fn [] => (ML_Debugger.on_breakpoint NONE; exit_input ()));

val _ =
  Isabelle_Process.protocol_command "Debugger.breakpoint"
    (fn [node_name, id0, breakpoint0, breakpoint_state0] =>
      let
        val id = Markup.parse_int id0;
        val breakpoint = Markup.parse_int breakpoint0;
        val breakpoint_state = Markup.parse_bool breakpoint_state0;

        fun err () = error ("Bad exec for command " ^ Markup.print_int id);
      in
        (case Document.command_exec (Document.state ()) node_name id of
          SOME (eval, _) =>
            if Command.eval_finished eval then
              let
                val st = Command.eval_result_state eval;
                val ctxt = Toplevel.presentation_context_of st
                  handle Toplevel.UNDEF => err ();
              in
                (case ML_Env.get_breakpoint (Context.Proof ctxt) breakpoint of
                  SOME (b, _) => b := breakpoint_state
                | NONE => err ())
              end
            else err ()
        | NONE => err ())
      end);

val _ =
  Isabelle_Process.protocol_command "Debugger.input"
    (fn thread_name :: msg => input thread_name msg);

end;