src/Pure/Tools/debugger.ML
author wenzelm
Tue, 11 Aug 2015 20:05:27 +0200
changeset 60897 7aad4be8a48e
parent 60891 89b7c84b0480
child 60904 e0fab97c989f
permissions -rw-r--r--
print values for stack entry;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
60749
f727b99faaf7 skeleton for interactive debugger;
wenzelm
parents:
diff changeset
     1
(*  Title:      Pure/Tools/debugger.ML
f727b99faaf7 skeleton for interactive debugger;
wenzelm
parents:
diff changeset
     2
    Author:     Makarius
f727b99faaf7 skeleton for interactive debugger;
wenzelm
parents:
diff changeset
     3
f727b99faaf7 skeleton for interactive debugger;
wenzelm
parents:
diff changeset
     4
Interactive debugger for Isabelle/ML.
f727b99faaf7 skeleton for interactive debugger;
wenzelm
parents:
diff changeset
     5
*)
f727b99faaf7 skeleton for interactive debugger;
wenzelm
parents:
diff changeset
     6
60830
f56e189350b2 separate channel for debugger output;
wenzelm
parents: 60829
diff changeset
     7
signature DEBUGGER =
f56e189350b2 separate channel for debugger output;
wenzelm
parents: 60829
diff changeset
     8
sig
60834
781f1168d31e maintain debugger output messages;
wenzelm
parents: 60830
diff changeset
     9
  val writeln_message: string -> unit
781f1168d31e maintain debugger output messages;
wenzelm
parents: 60830
diff changeset
    10
  val warning_message: string -> unit
781f1168d31e maintain debugger output messages;
wenzelm
parents: 60830
diff changeset
    11
  val error_message: string -> unit
60830
f56e189350b2 separate channel for debugger output;
wenzelm
parents: 60829
diff changeset
    12
end;
f56e189350b2 separate channel for debugger output;
wenzelm
parents: 60829
diff changeset
    13
f56e189350b2 separate channel for debugger output;
wenzelm
parents: 60829
diff changeset
    14
structure Debugger: DEBUGGER =
60765
e43e71a75838 support for ML debugger;
wenzelm
parents: 60749
diff changeset
    15
struct
e43e71a75838 support for ML debugger;
wenzelm
parents: 60749
diff changeset
    16
60869
878e32cf3131 more single stepping;
wenzelm
parents: 60864
diff changeset
    17
(** global state **)
878e32cf3131 more single stepping;
wenzelm
parents: 60864
diff changeset
    18
878e32cf3131 more single stepping;
wenzelm
parents: 60864
diff changeset
    19
(* output messages *)
60830
f56e189350b2 separate channel for debugger output;
wenzelm
parents: 60829
diff changeset
    20
60856
eb21ae05ec43 clarified thread state;
wenzelm
parents: 60842
diff changeset
    21
val _ = Session.protocol_handler "isabelle.Debugger$Handler";
eb21ae05ec43 clarified thread state;
wenzelm
parents: 60842
diff changeset
    22
60834
781f1168d31e maintain debugger output messages;
wenzelm
parents: 60830
diff changeset
    23
fun output_message kind msg =
60864
20cfa048fe7c suppress empty messages as usual;
wenzelm
parents: 60862
diff changeset
    24
  if msg = "" then ()
20cfa048fe7c suppress empty messages as usual;
wenzelm
parents: 60862
diff changeset
    25
  else
20cfa048fe7c suppress empty messages as usual;
wenzelm
parents: 60862
diff changeset
    26
    Output.protocol_message
20cfa048fe7c suppress empty messages as usual;
wenzelm
parents: 60862
diff changeset
    27
      (Markup.debugger_output (Simple_Thread.the_name ()))
20cfa048fe7c suppress empty messages as usual;
wenzelm
parents: 60862
diff changeset
    28
      [Markup.markup (kind, Markup.serial_properties (serial ())) msg];
60834
781f1168d31e maintain debugger output messages;
wenzelm
parents: 60830
diff changeset
    29
781f1168d31e maintain debugger output messages;
wenzelm
parents: 60830
diff changeset
    30
val writeln_message = output_message Markup.writelnN;
781f1168d31e maintain debugger output messages;
wenzelm
parents: 60830
diff changeset
    31
val warning_message = output_message Markup.warningN;
781f1168d31e maintain debugger output messages;
wenzelm
parents: 60830
diff changeset
    32
val error_message = output_message Markup.errorN;
60830
f56e189350b2 separate channel for debugger output;
wenzelm
parents: 60829
diff changeset
    33
60856
eb21ae05ec43 clarified thread state;
wenzelm
parents: 60842
diff changeset
    34
fun error_wrapper e = e ()
eb21ae05ec43 clarified thread state;
wenzelm
parents: 60842
diff changeset
    35
  handle exn =>
eb21ae05ec43 clarified thread state;
wenzelm
parents: 60842
diff changeset
    36
    if Exn.is_interrupt exn then reraise exn
eb21ae05ec43 clarified thread state;
wenzelm
parents: 60842
diff changeset
    37
    else error_message (Runtime.exn_message exn);
eb21ae05ec43 clarified thread state;
wenzelm
parents: 60842
diff changeset
    38
60830
f56e189350b2 separate channel for debugger output;
wenzelm
parents: 60829
diff changeset
    39
60888
35d85fd89fc1 eliminated cancel operation: disrupts normal evaluation of thread;
wenzelm
parents: 60887
diff changeset
    40
(* thread input *)
60765
e43e71a75838 support for ML debugger;
wenzelm
parents: 60749
diff changeset
    41
60888
35d85fd89fc1 eliminated cancel operation: disrupts normal evaluation of thread;
wenzelm
parents: 60887
diff changeset
    42
val thread_input =
60891
89b7c84b0480 vacuous input means continue, e.g. after exit;
wenzelm
parents: 60889
diff changeset
    43
  Synchronized.var "Debugger.state" (NONE: string list Queue.T Symtab.table option);
89b7c84b0480 vacuous input means continue, e.g. after exit;
wenzelm
parents: 60889
diff changeset
    44
89b7c84b0480 vacuous input means continue, e.g. after exit;
wenzelm
parents: 60889
diff changeset
    45
fun init_input () = Synchronized.change thread_input (K (SOME Symtab.empty));
89b7c84b0480 vacuous input means continue, e.g. after exit;
wenzelm
parents: 60889
diff changeset
    46
fun exit_input () = Synchronized.change thread_input (K NONE);
60765
e43e71a75838 support for ML debugger;
wenzelm
parents: 60749
diff changeset
    47
60842
5510c8444bc4 protocol support for thread debugger state;
wenzelm
parents: 60834
diff changeset
    48
fun input thread_name msg =
60891
89b7c84b0480 vacuous input means continue, e.g. after exit;
wenzelm
parents: 60889
diff changeset
    49
  if null msg then error "Empty input"
89b7c84b0480 vacuous input means continue, e.g. after exit;
wenzelm
parents: 60889
diff changeset
    50
  else
89b7c84b0480 vacuous input means continue, e.g. after exit;
wenzelm
parents: 60889
diff changeset
    51
    Synchronized.change thread_input
89b7c84b0480 vacuous input means continue, e.g. after exit;
wenzelm
parents: 60889
diff changeset
    52
      (Option.map (Symtab.map_default (thread_name, Queue.empty) (Queue.enqueue msg)));
60887
9d8b244234ab register thread such that cancel works;
wenzelm
parents: 60885
diff changeset
    53
60842
5510c8444bc4 protocol support for thread debugger state;
wenzelm
parents: 60834
diff changeset
    54
fun get_input thread_name =
60891
89b7c84b0480 vacuous input means continue, e.g. after exit;
wenzelm
parents: 60889
diff changeset
    55
  Synchronized.guarded_access thread_input
89b7c84b0480 vacuous input means continue, e.g. after exit;
wenzelm
parents: 60889
diff changeset
    56
    (fn NONE => SOME ([], NONE)
89b7c84b0480 vacuous input means continue, e.g. after exit;
wenzelm
parents: 60889
diff changeset
    57
      | SOME input =>
89b7c84b0480 vacuous input means continue, e.g. after exit;
wenzelm
parents: 60889
diff changeset
    58
          (case Symtab.lookup input thread_name of
89b7c84b0480 vacuous input means continue, e.g. after exit;
wenzelm
parents: 60889
diff changeset
    59
            NONE => NONE
89b7c84b0480 vacuous input means continue, e.g. after exit;
wenzelm
parents: 60889
diff changeset
    60
          | SOME queue =>
89b7c84b0480 vacuous input means continue, e.g. after exit;
wenzelm
parents: 60889
diff changeset
    61
              let
89b7c84b0480 vacuous input means continue, e.g. after exit;
wenzelm
parents: 60889
diff changeset
    62
                val (msg, queue') = Queue.dequeue queue;
89b7c84b0480 vacuous input means continue, e.g. after exit;
wenzelm
parents: 60889
diff changeset
    63
                val input' =
89b7c84b0480 vacuous input means continue, e.g. after exit;
wenzelm
parents: 60889
diff changeset
    64
                  if Queue.is_empty queue' then Symtab.delete_safe thread_name input
89b7c84b0480 vacuous input means continue, e.g. after exit;
wenzelm
parents: 60889
diff changeset
    65
                  else Symtab.update (thread_name, queue') input;
89b7c84b0480 vacuous input means continue, e.g. after exit;
wenzelm
parents: 60889
diff changeset
    66
              in SOME (msg, SOME input') end));
60765
e43e71a75838 support for ML debugger;
wenzelm
parents: 60749
diff changeset
    67
e43e71a75838 support for ML debugger;
wenzelm
parents: 60749
diff changeset
    68
60869
878e32cf3131 more single stepping;
wenzelm
parents: 60864
diff changeset
    69
878e32cf3131 more single stepping;
wenzelm
parents: 60864
diff changeset
    70
(** thread state **)
878e32cf3131 more single stepping;
wenzelm
parents: 60864
diff changeset
    71
878e32cf3131 more single stepping;
wenzelm
parents: 60864
diff changeset
    72
(* stack frame during debugging *)
60856
eb21ae05ec43 clarified thread state;
wenzelm
parents: 60842
diff changeset
    73
eb21ae05ec43 clarified thread state;
wenzelm
parents: 60842
diff changeset
    74
local
eb21ae05ec43 clarified thread state;
wenzelm
parents: 60842
diff changeset
    75
  val tag = Universal.tag () : ML_Debugger.state list Universal.tag;
eb21ae05ec43 clarified thread state;
wenzelm
parents: 60842
diff changeset
    76
in
60765
e43e71a75838 support for ML debugger;
wenzelm
parents: 60749
diff changeset
    77
60856
eb21ae05ec43 clarified thread state;
wenzelm
parents: 60842
diff changeset
    78
fun get_debugging () = the_default [] (Thread.getLocal tag);
eb21ae05ec43 clarified thread state;
wenzelm
parents: 60842
diff changeset
    79
val is_debugging = not o null o get_debugging;
60765
e43e71a75838 support for ML debugger;
wenzelm
parents: 60749
diff changeset
    80
60856
eb21ae05ec43 clarified thread state;
wenzelm
parents: 60842
diff changeset
    81
fun with_debugging e =
eb21ae05ec43 clarified thread state;
wenzelm
parents: 60842
diff changeset
    82
  setmp_thread_data tag (get_debugging ()) (ML_Debugger.state (Thread.self ())) e ();
60765
e43e71a75838 support for ML debugger;
wenzelm
parents: 60749
diff changeset
    83
60749
f727b99faaf7 skeleton for interactive debugger;
wenzelm
parents:
diff changeset
    84
end;
f727b99faaf7 skeleton for interactive debugger;
wenzelm
parents:
diff changeset
    85
60858
7bf2188a0998 evaluate ML expressions within debugger context;
wenzelm
parents: 60857
diff changeset
    86
fun the_debug_state thread_name index =
7bf2188a0998 evaluate ML expressions within debugger context;
wenzelm
parents: 60857
diff changeset
    87
  (case get_debugging () of
7bf2188a0998 evaluate ML expressions within debugger context;
wenzelm
parents: 60857
diff changeset
    88
    [] => error ("Missing debugger information for thread " ^ quote thread_name)
7bf2188a0998 evaluate ML expressions within debugger context;
wenzelm
parents: 60857
diff changeset
    89
  | states =>
7bf2188a0998 evaluate ML expressions within debugger context;
wenzelm
parents: 60857
diff changeset
    90
      if index < 0 orelse index >= length states then
7bf2188a0998 evaluate ML expressions within debugger context;
wenzelm
parents: 60857
diff changeset
    91
        error ("Bad debugger stack index " ^ signed_string_of_int index ^ " for thread " ^
7bf2188a0998 evaluate ML expressions within debugger context;
wenzelm
parents: 60857
diff changeset
    92
          quote thread_name)
7bf2188a0998 evaluate ML expressions within debugger context;
wenzelm
parents: 60857
diff changeset
    93
      else nth states index);
7bf2188a0998 evaluate ML expressions within debugger context;
wenzelm
parents: 60857
diff changeset
    94
7bf2188a0998 evaluate ML expressions within debugger context;
wenzelm
parents: 60857
diff changeset
    95
60869
878e32cf3131 more single stepping;
wenzelm
parents: 60864
diff changeset
    96
(* flags for single-stepping *)
60765
e43e71a75838 support for ML debugger;
wenzelm
parents: 60749
diff changeset
    97
60869
878e32cf3131 more single stepping;
wenzelm
parents: 60864
diff changeset
    98
datatype stepping = Stepping of bool * int;  (*stepping enabled, stack depth limit*)
878e32cf3131 more single stepping;
wenzelm
parents: 60864
diff changeset
    99
878e32cf3131 more single stepping;
wenzelm
parents: 60864
diff changeset
   100
local
878e32cf3131 more single stepping;
wenzelm
parents: 60864
diff changeset
   101
  val tag = Universal.tag () : stepping Universal.tag;
878e32cf3131 more single stepping;
wenzelm
parents: 60864
diff changeset
   102
in
878e32cf3131 more single stepping;
wenzelm
parents: 60864
diff changeset
   103
878e32cf3131 more single stepping;
wenzelm
parents: 60864
diff changeset
   104
fun get_stepping () = the_default (Stepping (false, ~1)) (Thread.getLocal tag);
878e32cf3131 more single stepping;
wenzelm
parents: 60864
diff changeset
   105
fun put_stepping stepping = Thread.setLocal (tag, Stepping stepping);
878e32cf3131 more single stepping;
wenzelm
parents: 60864
diff changeset
   106
878e32cf3131 more single stepping;
wenzelm
parents: 60864
diff changeset
   107
end;
878e32cf3131 more single stepping;
wenzelm
parents: 60864
diff changeset
   108
878e32cf3131 more single stepping;
wenzelm
parents: 60864
diff changeset
   109
fun is_stepping () =
878e32cf3131 more single stepping;
wenzelm
parents: 60864
diff changeset
   110
  let
878e32cf3131 more single stepping;
wenzelm
parents: 60864
diff changeset
   111
    val stack = ML_Debugger.state (Thread.self ());
878e32cf3131 more single stepping;
wenzelm
parents: 60864
diff changeset
   112
    val Stepping (stepping, depth) = get_stepping ();
878e32cf3131 more single stepping;
wenzelm
parents: 60864
diff changeset
   113
  in stepping andalso (depth < 0 orelse length stack <= depth) end;
878e32cf3131 more single stepping;
wenzelm
parents: 60864
diff changeset
   114
60891
89b7c84b0480 vacuous input means continue, e.g. after exit;
wenzelm
parents: 60889
diff changeset
   115
fun continue_stepping () = put_stepping (false, ~1);
60869
878e32cf3131 more single stepping;
wenzelm
parents: 60864
diff changeset
   116
fun step_stepping () = put_stepping (true, ~1);
878e32cf3131 more single stepping;
wenzelm
parents: 60864
diff changeset
   117
fun step_over_stepping () = put_stepping (true, length (get_debugging ()));
878e32cf3131 more single stepping;
wenzelm
parents: 60864
diff changeset
   118
fun step_out_stepping () = put_stepping (true, length (get_debugging ()) - 1);
878e32cf3131 more single stepping;
wenzelm
parents: 60864
diff changeset
   119
878e32cf3131 more single stepping;
wenzelm
parents: 60864
diff changeset
   120
878e32cf3131 more single stepping;
wenzelm
parents: 60864
diff changeset
   121
(** eval ML **)
60765
e43e71a75838 support for ML debugger;
wenzelm
parents: 60749
diff changeset
   122
60862
097afdd8a2fd eval ML context;
wenzelm
parents: 60858
diff changeset
   123
local
097afdd8a2fd eval ML context;
wenzelm
parents: 60858
diff changeset
   124
097afdd8a2fd eval ML context;
wenzelm
parents: 60858
diff changeset
   125
val context_attempts =
097afdd8a2fd eval ML context;
wenzelm
parents: 60858
diff changeset
   126
  map ML_Lex.read
097afdd8a2fd eval ML context;
wenzelm
parents: 60858
diff changeset
   127
   ["Context.set_thread_data (SOME (Context.Theory ML_context))",
097afdd8a2fd eval ML context;
wenzelm
parents: 60858
diff changeset
   128
    "Context.set_thread_data (SOME (Context.Proof ML_context))",
097afdd8a2fd eval ML context;
wenzelm
parents: 60858
diff changeset
   129
    "Context.set_thread_data (SOME ML_context)"];
097afdd8a2fd eval ML context;
wenzelm
parents: 60858
diff changeset
   130
097afdd8a2fd eval ML context;
wenzelm
parents: 60858
diff changeset
   131
fun evaluate {SML, verbose} =
097afdd8a2fd eval ML context;
wenzelm
parents: 60858
diff changeset
   132
  ML_Context.eval
097afdd8a2fd eval ML context;
wenzelm
parents: 60858
diff changeset
   133
    {SML = SML, exchange = false, redirect = false, verbose = verbose,
097afdd8a2fd eval ML context;
wenzelm
parents: 60858
diff changeset
   134
      writeln = writeln_message, warning = warning_message}
097afdd8a2fd eval ML context;
wenzelm
parents: 60858
diff changeset
   135
    Position.none;
097afdd8a2fd eval ML context;
wenzelm
parents: 60858
diff changeset
   136
60897
7aad4be8a48e print values for stack entry;
wenzelm
parents: 60891
diff changeset
   137
fun eval_context thread_name index SML toks =
60858
7bf2188a0998 evaluate ML expressions within debugger context;
wenzelm
parents: 60857
diff changeset
   138
  let
60897
7aad4be8a48e print values for stack entry;
wenzelm
parents: 60891
diff changeset
   139
    val context1 =
7aad4be8a48e print values for stack entry;
wenzelm
parents: 60891
diff changeset
   140
      ML_Context.the_generic_context ()
60858
7bf2188a0998 evaluate ML expressions within debugger context;
wenzelm
parents: 60857
diff changeset
   141
      |> Context_Position.set_visible_generic false
60871
9b26f3118e40 clarified ML options;
wenzelm
parents: 60869
diff changeset
   142
      |> Config.put_generic ML_Options.debugger false
60862
097afdd8a2fd eval ML context;
wenzelm
parents: 60858
diff changeset
   143
      |> ML_Env.add_name_space {SML = SML}
097afdd8a2fd eval ML context;
wenzelm
parents: 60858
diff changeset
   144
          (ML_Debugger.debug_name_space (the_debug_state thread_name index));
097afdd8a2fd eval ML context;
wenzelm
parents: 60858
diff changeset
   145
    val context2 =
60897
7aad4be8a48e print values for stack entry;
wenzelm
parents: 60891
diff changeset
   146
      if SML orelse forall (fn Antiquote.Text tok => ML_Lex.is_improper tok | _ => false) toks
60862
097afdd8a2fd eval ML context;
wenzelm
parents: 60858
diff changeset
   147
      then context1
097afdd8a2fd eval ML context;
wenzelm
parents: 60858
diff changeset
   148
      else
097afdd8a2fd eval ML context;
wenzelm
parents: 60858
diff changeset
   149
        let
097afdd8a2fd eval ML context;
wenzelm
parents: 60858
diff changeset
   150
          val context' = context1
60897
7aad4be8a48e print values for stack entry;
wenzelm
parents: 60891
diff changeset
   151
            |> ML_Context.exec (fn () =>
7aad4be8a48e print values for stack entry;
wenzelm
parents: 60891
diff changeset
   152
                evaluate {SML = SML, verbose = true} (ML_Lex.read "val ML_context = " @ toks));
60862
097afdd8a2fd eval ML context;
wenzelm
parents: 60858
diff changeset
   153
          fun try_exec toks =
097afdd8a2fd eval ML context;
wenzelm
parents: 60858
diff changeset
   154
            try (ML_Context.exec (fn () => evaluate {SML = false, verbose = false} toks)) context';
097afdd8a2fd eval ML context;
wenzelm
parents: 60858
diff changeset
   155
        in
097afdd8a2fd eval ML context;
wenzelm
parents: 60858
diff changeset
   156
          (case get_first try_exec context_attempts of
097afdd8a2fd eval ML context;
wenzelm
parents: 60858
diff changeset
   157
            SOME context2 => context2
097afdd8a2fd eval ML context;
wenzelm
parents: 60858
diff changeset
   158
          | NONE => error "Malformed context: expected type theory, Proof.context, Context.generic")
097afdd8a2fd eval ML context;
wenzelm
parents: 60858
diff changeset
   159
        end;
60897
7aad4be8a48e print values for stack entry;
wenzelm
parents: 60891
diff changeset
   160
  in context2 end;
7aad4be8a48e print values for stack entry;
wenzelm
parents: 60891
diff changeset
   161
7aad4be8a48e print values for stack entry;
wenzelm
parents: 60891
diff changeset
   162
in
7aad4be8a48e print values for stack entry;
wenzelm
parents: 60891
diff changeset
   163
7aad4be8a48e print values for stack entry;
wenzelm
parents: 60891
diff changeset
   164
fun eval thread_name index SML txt1 txt2 =
7aad4be8a48e print values for stack entry;
wenzelm
parents: 60891
diff changeset
   165
  let
7aad4be8a48e print values for stack entry;
wenzelm
parents: 60891
diff changeset
   166
    val (toks1, toks2) = apply2 (ML_Lex.read_source SML o Input.string) (txt1, txt2);
7aad4be8a48e print values for stack entry;
wenzelm
parents: 60891
diff changeset
   167
    val context = eval_context thread_name index SML toks1;
7aad4be8a48e print values for stack entry;
wenzelm
parents: 60891
diff changeset
   168
  in Context.setmp_thread_data (SOME context) evaluate {SML = SML, verbose = true} toks2 end;
7aad4be8a48e print values for stack entry;
wenzelm
parents: 60891
diff changeset
   169
7aad4be8a48e print values for stack entry;
wenzelm
parents: 60891
diff changeset
   170
fun print_vals thread_name index SML txt =
7aad4be8a48e print values for stack entry;
wenzelm
parents: 60891
diff changeset
   171
  let
7aad4be8a48e print values for stack entry;
wenzelm
parents: 60891
diff changeset
   172
    val context = eval_context thread_name index SML (ML_Lex.read_source SML (Input.string txt));
7aad4be8a48e print values for stack entry;
wenzelm
parents: 60891
diff changeset
   173
    val space = ML_Debugger.debug_name_space (the_debug_state thread_name index);
7aad4be8a48e print values for stack entry;
wenzelm
parents: 60891
diff changeset
   174
7aad4be8a48e print values for stack entry;
wenzelm
parents: 60891
diff changeset
   175
    fun print x =
7aad4be8a48e print values for stack entry;
wenzelm
parents: 60891
diff changeset
   176
      Pretty.from_ML (ML_Name_Space.display_val (x, ML_Options.get_print_depth (), space));
7aad4be8a48e print values for stack entry;
wenzelm
parents: 60891
diff changeset
   177
    fun print_all () =
7aad4be8a48e print values for stack entry;
wenzelm
parents: 60891
diff changeset
   178
      #allVal (ML_Debugger.debug_name_space (the_debug_state thread_name index)) ()
7aad4be8a48e print values for stack entry;
wenzelm
parents: 60891
diff changeset
   179
      |> sort_wrt #1 |> map (Pretty.item o single o print o #2)
7aad4be8a48e print values for stack entry;
wenzelm
parents: 60891
diff changeset
   180
      |> Pretty.chunks |> Pretty.string_of |> writeln_message;
7aad4be8a48e print values for stack entry;
wenzelm
parents: 60891
diff changeset
   181
  in Context.setmp_thread_data (SOME context) print_all () end;
60862
097afdd8a2fd eval ML context;
wenzelm
parents: 60858
diff changeset
   182
097afdd8a2fd eval ML context;
wenzelm
parents: 60858
diff changeset
   183
end;
60749
f727b99faaf7 skeleton for interactive debugger;
wenzelm
parents:
diff changeset
   184
60765
e43e71a75838 support for ML debugger;
wenzelm
parents: 60749
diff changeset
   185
60869
878e32cf3131 more single stepping;
wenzelm
parents: 60864
diff changeset
   186
60891
89b7c84b0480 vacuous input means continue, e.g. after exit;
wenzelm
parents: 60889
diff changeset
   187
(** debugger loop **)
60857
4c18d8e4fe14 clarified debugger loop;
wenzelm
parents: 60856
diff changeset
   188
4c18d8e4fe14 clarified debugger loop;
wenzelm
parents: 60856
diff changeset
   189
local
60765
e43e71a75838 support for ML debugger;
wenzelm
parents: 60749
diff changeset
   190
60842
5510c8444bc4 protocol support for thread debugger state;
wenzelm
parents: 60834
diff changeset
   191
fun debugger_state thread_name =
5510c8444bc4 protocol support for thread debugger state;
wenzelm
parents: 60834
diff changeset
   192
  Output.protocol_message (Markup.debugger_state thread_name)
60856
eb21ae05ec43 clarified thread state;
wenzelm
parents: 60842
diff changeset
   193
   [get_debugging ()
60842
5510c8444bc4 protocol support for thread debugger state;
wenzelm
parents: 60834
diff changeset
   194
    |> map (fn st =>
5510c8444bc4 protocol support for thread debugger state;
wenzelm
parents: 60834
diff changeset
   195
      (Position.properties_of (Exn_Properties.position_of (ML_Debugger.debug_location st)),
5510c8444bc4 protocol support for thread debugger state;
wenzelm
parents: 60834
diff changeset
   196
       ML_Debugger.debug_function st))
5510c8444bc4 protocol support for thread debugger state;
wenzelm
parents: 60834
diff changeset
   197
    |> let open XML.Encode in list (pair properties string) end
5510c8444bc4 protocol support for thread debugger state;
wenzelm
parents: 60834
diff changeset
   198
    |> YXML.string_of_body];
5510c8444bc4 protocol support for thread debugger state;
wenzelm
parents: 60834
diff changeset
   199
60857
4c18d8e4fe14 clarified debugger loop;
wenzelm
parents: 60856
diff changeset
   200
fun debugger_command thread_name =
4c18d8e4fe14 clarified debugger loop;
wenzelm
parents: 60856
diff changeset
   201
  (case get_input thread_name of
60891
89b7c84b0480 vacuous input means continue, e.g. after exit;
wenzelm
parents: 60889
diff changeset
   202
    [] => (continue_stepping (); false)
89b7c84b0480 vacuous input means continue, e.g. after exit;
wenzelm
parents: 60889
diff changeset
   203
  | ["continue"] => (continue_stepping (); false)
89b7c84b0480 vacuous input means continue, e.g. after exit;
wenzelm
parents: 60889
diff changeset
   204
  | ["step"] => (step_stepping (); false)
60869
878e32cf3131 more single stepping;
wenzelm
parents: 60864
diff changeset
   205
  | ["step_over"] => (step_over_stepping (); false)
878e32cf3131 more single stepping;
wenzelm
parents: 60864
diff changeset
   206
  | ["step_out"] => (step_out_stepping (); false)
60857
4c18d8e4fe14 clarified debugger loop;
wenzelm
parents: 60856
diff changeset
   207
  | ["eval", index, SML, txt1, txt2] =>
4c18d8e4fe14 clarified debugger loop;
wenzelm
parents: 60856
diff changeset
   208
     (error_wrapper (fn () =>
4c18d8e4fe14 clarified debugger loop;
wenzelm
parents: 60856
diff changeset
   209
        eval thread_name (Markup.parse_int index) (Markup.parse_bool SML) txt1 txt2); true)
60897
7aad4be8a48e print values for stack entry;
wenzelm
parents: 60891
diff changeset
   210
  | ["print_vals", index, SML, txt] =>
7aad4be8a48e print values for stack entry;
wenzelm
parents: 60891
diff changeset
   211
     (error_wrapper (fn () =>
7aad4be8a48e print values for stack entry;
wenzelm
parents: 60891
diff changeset
   212
        print_vals thread_name (Markup.parse_int index) (Markup.parse_bool SML) txt); true)
60857
4c18d8e4fe14 clarified debugger loop;
wenzelm
parents: 60856
diff changeset
   213
  | bad =>
4c18d8e4fe14 clarified debugger loop;
wenzelm
parents: 60856
diff changeset
   214
     (Output.system_message
4c18d8e4fe14 clarified debugger loop;
wenzelm
parents: 60856
diff changeset
   215
        ("Debugger: bad input " ^ ML_Syntax.print_list ML_Syntax.print_string bad); true));
4c18d8e4fe14 clarified debugger loop;
wenzelm
parents: 60856
diff changeset
   216
60889
7f210887cc4e init/exit depending on active debugger panels;
wenzelm
parents: 60888
diff changeset
   217
in
7f210887cc4e init/exit depending on active debugger panels;
wenzelm
parents: 60888
diff changeset
   218
60842
5510c8444bc4 protocol support for thread debugger state;
wenzelm
parents: 60834
diff changeset
   219
fun debugger_loop thread_name =
60885
d8d51f956f05 report final debugger_state more robustly, e.g. after interrupt;
wenzelm
parents: 60884
diff changeset
   220
  uninterruptible (fn restore_attributes => fn () =>
d8d51f956f05 report final debugger_state more robustly, e.g. after interrupt;
wenzelm
parents: 60884
diff changeset
   221
    let
d8d51f956f05 report final debugger_state more robustly, e.g. after interrupt;
wenzelm
parents: 60884
diff changeset
   222
      fun loop () =
d8d51f956f05 report final debugger_state more robustly, e.g. after interrupt;
wenzelm
parents: 60884
diff changeset
   223
        (debugger_state thread_name; if debugger_command thread_name then loop () else ());
d8d51f956f05 report final debugger_state more robustly, e.g. after interrupt;
wenzelm
parents: 60884
diff changeset
   224
      val result = Exn.capture (restore_attributes with_debugging) loop;
d8d51f956f05 report final debugger_state more robustly, e.g. after interrupt;
wenzelm
parents: 60884
diff changeset
   225
      val _ = debugger_state thread_name;
d8d51f956f05 report final debugger_state more robustly, e.g. after interrupt;
wenzelm
parents: 60884
diff changeset
   226
    in Exn.release result end) ();
60765
e43e71a75838 support for ML debugger;
wenzelm
parents: 60749
diff changeset
   227
60857
4c18d8e4fe14 clarified debugger loop;
wenzelm
parents: 60856
diff changeset
   228
end;
4c18d8e4fe14 clarified debugger loop;
wenzelm
parents: 60856
diff changeset
   229
60765
e43e71a75838 support for ML debugger;
wenzelm
parents: 60749
diff changeset
   230
60869
878e32cf3131 more single stepping;
wenzelm
parents: 60864
diff changeset
   231
878e32cf3131 more single stepping;
wenzelm
parents: 60864
diff changeset
   232
(** protocol commands **)
60765
e43e71a75838 support for ML debugger;
wenzelm
parents: 60749
diff changeset
   233
e43e71a75838 support for ML debugger;
wenzelm
parents: 60749
diff changeset
   234
val _ =
e43e71a75838 support for ML debugger;
wenzelm
parents: 60749
diff changeset
   235
  Isabelle_Process.protocol_command "Debugger.init"
60889
7f210887cc4e init/exit depending on active debugger panels;
wenzelm
parents: 60888
diff changeset
   236
    (fn [] =>
60891
89b7c84b0480 vacuous input means continue, e.g. after exit;
wenzelm
parents: 60889
diff changeset
   237
     (init_input ();
60889
7f210887cc4e init/exit depending on active debugger panels;
wenzelm
parents: 60888
diff changeset
   238
      ML_Debugger.on_breakpoint
7f210887cc4e init/exit depending on active debugger panels;
wenzelm
parents: 60888
diff changeset
   239
        (SOME (fn (_, break) =>
7f210887cc4e init/exit depending on active debugger panels;
wenzelm
parents: 60888
diff changeset
   240
          if not (is_debugging ()) andalso (! break orelse is_stepping ()) then
7f210887cc4e init/exit depending on active debugger panels;
wenzelm
parents: 60888
diff changeset
   241
            (case Simple_Thread.get_name () of
7f210887cc4e init/exit depending on active debugger panels;
wenzelm
parents: 60888
diff changeset
   242
              SOME thread_name => debugger_loop thread_name
7f210887cc4e init/exit depending on active debugger panels;
wenzelm
parents: 60888
diff changeset
   243
            | NONE => ())
60891
89b7c84b0480 vacuous input means continue, e.g. after exit;
wenzelm
parents: 60889
diff changeset
   244
          else ()))));
60889
7f210887cc4e init/exit depending on active debugger panels;
wenzelm
parents: 60888
diff changeset
   245
7f210887cc4e init/exit depending on active debugger panels;
wenzelm
parents: 60888
diff changeset
   246
val _ =
7f210887cc4e init/exit depending on active debugger panels;
wenzelm
parents: 60888
diff changeset
   247
  Isabelle_Process.protocol_command "Debugger.exit"
60891
89b7c84b0480 vacuous input means continue, e.g. after exit;
wenzelm
parents: 60889
diff changeset
   248
    (fn [] => (ML_Debugger.on_breakpoint NONE; exit_input ()));
60765
e43e71a75838 support for ML debugger;
wenzelm
parents: 60749
diff changeset
   249
e43e71a75838 support for ML debugger;
wenzelm
parents: 60749
diff changeset
   250
val _ =
60878
1f0d2bbcf38b added action to toggle breakpoints (on editor side);
wenzelm
parents: 60871
diff changeset
   251
  Isabelle_Process.protocol_command "Debugger.breakpoint"
60880
fa958e24ff24 set breakpoint state on ML side, relying on stable situation within the PIDE editing queue;
wenzelm
parents: 60878
diff changeset
   252
    (fn [node_name, id0, breakpoint0, breakpoint_state0] =>
60878
1f0d2bbcf38b added action to toggle breakpoints (on editor side);
wenzelm
parents: 60871
diff changeset
   253
      let
60880
fa958e24ff24 set breakpoint state on ML side, relying on stable situation within the PIDE editing queue;
wenzelm
parents: 60878
diff changeset
   254
        val id = Markup.parse_int id0;
fa958e24ff24 set breakpoint state on ML side, relying on stable situation within the PIDE editing queue;
wenzelm
parents: 60878
diff changeset
   255
        val breakpoint = Markup.parse_int breakpoint0;
fa958e24ff24 set breakpoint state on ML side, relying on stable situation within the PIDE editing queue;
wenzelm
parents: 60878
diff changeset
   256
        val breakpoint_state = Markup.parse_bool breakpoint_state0;
fa958e24ff24 set breakpoint state on ML side, relying on stable situation within the PIDE editing queue;
wenzelm
parents: 60878
diff changeset
   257
fa958e24ff24 set breakpoint state on ML side, relying on stable situation within the PIDE editing queue;
wenzelm
parents: 60878
diff changeset
   258
        fun err () = error ("Bad exec for command " ^ Markup.print_int id);
fa958e24ff24 set breakpoint state on ML side, relying on stable situation within the PIDE editing queue;
wenzelm
parents: 60878
diff changeset
   259
      in
fa958e24ff24 set breakpoint state on ML side, relying on stable situation within the PIDE editing queue;
wenzelm
parents: 60878
diff changeset
   260
        (case Document.command_exec (Document.state ()) node_name id of
fa958e24ff24 set breakpoint state on ML side, relying on stable situation within the PIDE editing queue;
wenzelm
parents: 60878
diff changeset
   261
          SOME (eval, _) =>
fa958e24ff24 set breakpoint state on ML side, relying on stable situation within the PIDE editing queue;
wenzelm
parents: 60878
diff changeset
   262
            if Command.eval_finished eval then
fa958e24ff24 set breakpoint state on ML side, relying on stable situation within the PIDE editing queue;
wenzelm
parents: 60878
diff changeset
   263
              let
fa958e24ff24 set breakpoint state on ML side, relying on stable situation within the PIDE editing queue;
wenzelm
parents: 60878
diff changeset
   264
                val st = Command.eval_result_state eval;
fa958e24ff24 set breakpoint state on ML side, relying on stable situation within the PIDE editing queue;
wenzelm
parents: 60878
diff changeset
   265
                val ctxt = Toplevel.presentation_context_of st
fa958e24ff24 set breakpoint state on ML side, relying on stable situation within the PIDE editing queue;
wenzelm
parents: 60878
diff changeset
   266
                  handle Toplevel.UNDEF => err ();
fa958e24ff24 set breakpoint state on ML side, relying on stable situation within the PIDE editing queue;
wenzelm
parents: 60878
diff changeset
   267
              in
fa958e24ff24 set breakpoint state on ML side, relying on stable situation within the PIDE editing queue;
wenzelm
parents: 60878
diff changeset
   268
                (case ML_Env.get_breakpoint (Context.Proof ctxt) breakpoint of
fa958e24ff24 set breakpoint state on ML side, relying on stable situation within the PIDE editing queue;
wenzelm
parents: 60878
diff changeset
   269
                  SOME (b, _) => b := breakpoint_state
fa958e24ff24 set breakpoint state on ML side, relying on stable situation within the PIDE editing queue;
wenzelm
parents: 60878
diff changeset
   270
                | NONE => err ())
fa958e24ff24 set breakpoint state on ML side, relying on stable situation within the PIDE editing queue;
wenzelm
parents: 60878
diff changeset
   271
              end
fa958e24ff24 set breakpoint state on ML side, relying on stable situation within the PIDE editing queue;
wenzelm
parents: 60878
diff changeset
   272
            else err ()
fa958e24ff24 set breakpoint state on ML side, relying on stable situation within the PIDE editing queue;
wenzelm
parents: 60878
diff changeset
   273
        | NONE => err ())
fa958e24ff24 set breakpoint state on ML side, relying on stable situation within the PIDE editing queue;
wenzelm
parents: 60878
diff changeset
   274
      end);
60878
1f0d2bbcf38b added action to toggle breakpoints (on editor side);
wenzelm
parents: 60871
diff changeset
   275
1f0d2bbcf38b added action to toggle breakpoints (on editor side);
wenzelm
parents: 60871
diff changeset
   276
val _ =
60765
e43e71a75838 support for ML debugger;
wenzelm
parents: 60749
diff changeset
   277
  Isabelle_Process.protocol_command "Debugger.input"
60842
5510c8444bc4 protocol support for thread debugger state;
wenzelm
parents: 60834
diff changeset
   278
    (fn thread_name :: msg => input thread_name msg);
60765
e43e71a75838 support for ML debugger;
wenzelm
parents: 60749
diff changeset
   279
60749
f727b99faaf7 skeleton for interactive debugger;
wenzelm
parents:
diff changeset
   280
end;