src/Pure/Tools/debugger.ML
author wenzelm
Mon, 10 Aug 2015 22:21:55 +0200
changeset 60885 d8d51f956f05
parent 60884 f3039309702e
child 60887 9d8b244234ab
permissions -rw-r--r--
report final debugger_state more robustly, e.g. after interrupt;
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
60869
878e32cf3131 more single stepping;
wenzelm
parents: 60864
diff changeset
    40
(* thread names and input *)
60765
e43e71a75838 support for ML debugger;
wenzelm
parents: 60749
diff changeset
    41
e43e71a75838 support for ML debugger;
wenzelm
parents: 60749
diff changeset
    42
datatype state =
e43e71a75838 support for ML debugger;
wenzelm
parents: 60749
diff changeset
    43
  State of {
60829
4b16b778ce0d clarified thread name;
wenzelm
parents: 60765
diff changeset
    44
    threads: Thread.thread Symtab.table,  (*thread name ~> thread*)
4b16b778ce0d clarified thread name;
wenzelm
parents: 60765
diff changeset
    45
    input: string list Queue.T Symtab.table  (*thread name ~> input queue*)
60765
e43e71a75838 support for ML debugger;
wenzelm
parents: 60749
diff changeset
    46
  };
e43e71a75838 support for ML debugger;
wenzelm
parents: 60749
diff changeset
    47
e43e71a75838 support for ML debugger;
wenzelm
parents: 60749
diff changeset
    48
fun make_state (threads, input) = State {threads = threads, input = input};
e43e71a75838 support for ML debugger;
wenzelm
parents: 60749
diff changeset
    49
val init_state = make_state (Symtab.empty, Symtab.empty);
e43e71a75838 support for ML debugger;
wenzelm
parents: 60749
diff changeset
    50
fun map_state f (State {threads, input}) = make_state (f (threads, input));
e43e71a75838 support for ML debugger;
wenzelm
parents: 60749
diff changeset
    51
e43e71a75838 support for ML debugger;
wenzelm
parents: 60749
diff changeset
    52
val global_state = Synchronized.var "Debugger.state" init_state;
e43e71a75838 support for ML debugger;
wenzelm
parents: 60749
diff changeset
    53
60842
5510c8444bc4 protocol support for thread debugger state;
wenzelm
parents: 60834
diff changeset
    54
fun cancel thread_name =
60765
e43e71a75838 support for ML debugger;
wenzelm
parents: 60749
diff changeset
    55
  Synchronized.change global_state (tap (fn State {threads, ...} =>
60842
5510c8444bc4 protocol support for thread debugger state;
wenzelm
parents: 60834
diff changeset
    56
    (case Symtab.lookup threads thread_name of
60765
e43e71a75838 support for ML debugger;
wenzelm
parents: 60749
diff changeset
    57
      NONE => ()
e43e71a75838 support for ML debugger;
wenzelm
parents: 60749
diff changeset
    58
    | SOME thread => Simple_Thread.interrupt_unsynchronized thread)));
e43e71a75838 support for ML debugger;
wenzelm
parents: 60749
diff changeset
    59
60842
5510c8444bc4 protocol support for thread debugger state;
wenzelm
parents: 60834
diff changeset
    60
fun input thread_name msg =
60765
e43e71a75838 support for ML debugger;
wenzelm
parents: 60749
diff changeset
    61
  Synchronized.change global_state (map_state (fn (threads, input) =>
60842
5510c8444bc4 protocol support for thread debugger state;
wenzelm
parents: 60834
diff changeset
    62
    let val input' = Symtab.map_default (thread_name, Queue.empty) (Queue.enqueue msg) input;
60765
e43e71a75838 support for ML debugger;
wenzelm
parents: 60749
diff changeset
    63
    in (threads, input') end));
e43e71a75838 support for ML debugger;
wenzelm
parents: 60749
diff changeset
    64
60842
5510c8444bc4 protocol support for thread debugger state;
wenzelm
parents: 60834
diff changeset
    65
fun get_input thread_name =
60765
e43e71a75838 support for ML debugger;
wenzelm
parents: 60749
diff changeset
    66
  Synchronized.guarded_access global_state (fn State {threads, input} =>
60842
5510c8444bc4 protocol support for thread debugger state;
wenzelm
parents: 60834
diff changeset
    67
    (case Symtab.lookup input thread_name of
60765
e43e71a75838 support for ML debugger;
wenzelm
parents: 60749
diff changeset
    68
      NONE => NONE
e43e71a75838 support for ML debugger;
wenzelm
parents: 60749
diff changeset
    69
    | SOME queue =>
e43e71a75838 support for ML debugger;
wenzelm
parents: 60749
diff changeset
    70
        let
e43e71a75838 support for ML debugger;
wenzelm
parents: 60749
diff changeset
    71
          val (msg, queue') = Queue.dequeue queue;
e43e71a75838 support for ML debugger;
wenzelm
parents: 60749
diff changeset
    72
          val input' =
60842
5510c8444bc4 protocol support for thread debugger state;
wenzelm
parents: 60834
diff changeset
    73
            if Queue.is_empty queue' then Symtab.delete_safe thread_name input
5510c8444bc4 protocol support for thread debugger state;
wenzelm
parents: 60834
diff changeset
    74
            else Symtab.update (thread_name, queue') input;
60765
e43e71a75838 support for ML debugger;
wenzelm
parents: 60749
diff changeset
    75
        in SOME (msg, make_state (threads, input')) end));
e43e71a75838 support for ML debugger;
wenzelm
parents: 60749
diff changeset
    76
e43e71a75838 support for ML debugger;
wenzelm
parents: 60749
diff changeset
    77
60869
878e32cf3131 more single stepping;
wenzelm
parents: 60864
diff changeset
    78
878e32cf3131 more single stepping;
wenzelm
parents: 60864
diff changeset
    79
(** thread state **)
878e32cf3131 more single stepping;
wenzelm
parents: 60864
diff changeset
    80
878e32cf3131 more single stepping;
wenzelm
parents: 60864
diff changeset
    81
(* stack frame during debugging *)
60856
eb21ae05ec43 clarified thread state;
wenzelm
parents: 60842
diff changeset
    82
eb21ae05ec43 clarified thread state;
wenzelm
parents: 60842
diff changeset
    83
local
eb21ae05ec43 clarified thread state;
wenzelm
parents: 60842
diff changeset
    84
  val tag = Universal.tag () : ML_Debugger.state list Universal.tag;
eb21ae05ec43 clarified thread state;
wenzelm
parents: 60842
diff changeset
    85
in
60765
e43e71a75838 support for ML debugger;
wenzelm
parents: 60749
diff changeset
    86
60856
eb21ae05ec43 clarified thread state;
wenzelm
parents: 60842
diff changeset
    87
fun get_debugging () = the_default [] (Thread.getLocal tag);
eb21ae05ec43 clarified thread state;
wenzelm
parents: 60842
diff changeset
    88
val is_debugging = not o null o get_debugging;
60765
e43e71a75838 support for ML debugger;
wenzelm
parents: 60749
diff changeset
    89
60856
eb21ae05ec43 clarified thread state;
wenzelm
parents: 60842
diff changeset
    90
fun with_debugging e =
eb21ae05ec43 clarified thread state;
wenzelm
parents: 60842
diff changeset
    91
  setmp_thread_data tag (get_debugging ()) (ML_Debugger.state (Thread.self ())) e ();
60765
e43e71a75838 support for ML debugger;
wenzelm
parents: 60749
diff changeset
    92
60749
f727b99faaf7 skeleton for interactive debugger;
wenzelm
parents:
diff changeset
    93
end;
f727b99faaf7 skeleton for interactive debugger;
wenzelm
parents:
diff changeset
    94
60858
7bf2188a0998 evaluate ML expressions within debugger context;
wenzelm
parents: 60857
diff changeset
    95
fun the_debug_state thread_name index =
7bf2188a0998 evaluate ML expressions within debugger context;
wenzelm
parents: 60857
diff changeset
    96
  (case get_debugging () of
7bf2188a0998 evaluate ML expressions within debugger context;
wenzelm
parents: 60857
diff changeset
    97
    [] => error ("Missing debugger information for thread " ^ quote thread_name)
7bf2188a0998 evaluate ML expressions within debugger context;
wenzelm
parents: 60857
diff changeset
    98
  | states =>
7bf2188a0998 evaluate ML expressions within debugger context;
wenzelm
parents: 60857
diff changeset
    99
      if index < 0 orelse index >= length states then
7bf2188a0998 evaluate ML expressions within debugger context;
wenzelm
parents: 60857
diff changeset
   100
        error ("Bad debugger stack index " ^ signed_string_of_int index ^ " for thread " ^
7bf2188a0998 evaluate ML expressions within debugger context;
wenzelm
parents: 60857
diff changeset
   101
          quote thread_name)
7bf2188a0998 evaluate ML expressions within debugger context;
wenzelm
parents: 60857
diff changeset
   102
      else nth states index);
7bf2188a0998 evaluate ML expressions within debugger context;
wenzelm
parents: 60857
diff changeset
   103
7bf2188a0998 evaluate ML expressions within debugger context;
wenzelm
parents: 60857
diff changeset
   104
60869
878e32cf3131 more single stepping;
wenzelm
parents: 60864
diff changeset
   105
(* flags for single-stepping *)
60765
e43e71a75838 support for ML debugger;
wenzelm
parents: 60749
diff changeset
   106
60869
878e32cf3131 more single stepping;
wenzelm
parents: 60864
diff changeset
   107
datatype stepping = Stepping of bool * int;  (*stepping enabled, stack depth limit*)
878e32cf3131 more single stepping;
wenzelm
parents: 60864
diff changeset
   108
878e32cf3131 more single stepping;
wenzelm
parents: 60864
diff changeset
   109
local
878e32cf3131 more single stepping;
wenzelm
parents: 60864
diff changeset
   110
  val tag = Universal.tag () : stepping Universal.tag;
878e32cf3131 more single stepping;
wenzelm
parents: 60864
diff changeset
   111
in
878e32cf3131 more single stepping;
wenzelm
parents: 60864
diff changeset
   112
878e32cf3131 more single stepping;
wenzelm
parents: 60864
diff changeset
   113
fun get_stepping () = the_default (Stepping (false, ~1)) (Thread.getLocal tag);
878e32cf3131 more single stepping;
wenzelm
parents: 60864
diff changeset
   114
fun put_stepping stepping = Thread.setLocal (tag, Stepping stepping);
878e32cf3131 more single stepping;
wenzelm
parents: 60864
diff changeset
   115
878e32cf3131 more single stepping;
wenzelm
parents: 60864
diff changeset
   116
end;
878e32cf3131 more single stepping;
wenzelm
parents: 60864
diff changeset
   117
878e32cf3131 more single stepping;
wenzelm
parents: 60864
diff changeset
   118
fun is_stepping () =
878e32cf3131 more single stepping;
wenzelm
parents: 60864
diff changeset
   119
  let
878e32cf3131 more single stepping;
wenzelm
parents: 60864
diff changeset
   120
    val stack = ML_Debugger.state (Thread.self ());
878e32cf3131 more single stepping;
wenzelm
parents: 60864
diff changeset
   121
    val Stepping (stepping, depth) = get_stepping ();
878e32cf3131 more single stepping;
wenzelm
parents: 60864
diff changeset
   122
  in stepping andalso (depth < 0 orelse length stack <= depth) end;
878e32cf3131 more single stepping;
wenzelm
parents: 60864
diff changeset
   123
878e32cf3131 more single stepping;
wenzelm
parents: 60864
diff changeset
   124
fun step_stepping () = put_stepping (true, ~1);
878e32cf3131 more single stepping;
wenzelm
parents: 60864
diff changeset
   125
fun step_over_stepping () = put_stepping (true, length (get_debugging ()));
878e32cf3131 more single stepping;
wenzelm
parents: 60864
diff changeset
   126
fun step_out_stepping () = put_stepping (true, length (get_debugging ()) - 1);
878e32cf3131 more single stepping;
wenzelm
parents: 60864
diff changeset
   127
fun continue_stepping () = put_stepping (false, ~1);
878e32cf3131 more single stepping;
wenzelm
parents: 60864
diff changeset
   128
878e32cf3131 more single stepping;
wenzelm
parents: 60864
diff changeset
   129
878e32cf3131 more single stepping;
wenzelm
parents: 60864
diff changeset
   130
(** eval ML **)
60765
e43e71a75838 support for ML debugger;
wenzelm
parents: 60749
diff changeset
   131
60862
097afdd8a2fd eval ML context;
wenzelm
parents: 60858
diff changeset
   132
local
097afdd8a2fd eval ML context;
wenzelm
parents: 60858
diff changeset
   133
097afdd8a2fd eval ML context;
wenzelm
parents: 60858
diff changeset
   134
val context_attempts =
097afdd8a2fd eval ML context;
wenzelm
parents: 60858
diff changeset
   135
  map ML_Lex.read
097afdd8a2fd eval ML context;
wenzelm
parents: 60858
diff changeset
   136
   ["Context.set_thread_data (SOME (Context.Theory ML_context))",
097afdd8a2fd eval ML context;
wenzelm
parents: 60858
diff changeset
   137
    "Context.set_thread_data (SOME (Context.Proof ML_context))",
097afdd8a2fd eval ML context;
wenzelm
parents: 60858
diff changeset
   138
    "Context.set_thread_data (SOME ML_context)"];
097afdd8a2fd eval ML context;
wenzelm
parents: 60858
diff changeset
   139
097afdd8a2fd eval ML context;
wenzelm
parents: 60858
diff changeset
   140
fun evaluate {SML, verbose} =
097afdd8a2fd eval ML context;
wenzelm
parents: 60858
diff changeset
   141
  ML_Context.eval
097afdd8a2fd eval ML context;
wenzelm
parents: 60858
diff changeset
   142
    {SML = SML, exchange = false, redirect = false, verbose = verbose,
097afdd8a2fd eval ML context;
wenzelm
parents: 60858
diff changeset
   143
      writeln = writeln_message, warning = warning_message}
097afdd8a2fd eval ML context;
wenzelm
parents: 60858
diff changeset
   144
    Position.none;
097afdd8a2fd eval ML context;
wenzelm
parents: 60858
diff changeset
   145
097afdd8a2fd eval ML context;
wenzelm
parents: 60858
diff changeset
   146
in
097afdd8a2fd eval ML context;
wenzelm
parents: 60858
diff changeset
   147
60858
7bf2188a0998 evaluate ML expressions within debugger context;
wenzelm
parents: 60857
diff changeset
   148
fun eval thread_name index SML txt1 txt2 =
7bf2188a0998 evaluate ML expressions within debugger context;
wenzelm
parents: 60857
diff changeset
   149
  let
60862
097afdd8a2fd eval ML context;
wenzelm
parents: 60858
diff changeset
   150
    val (toks1, toks2) = apply2 (ML_Lex.read_source SML o Input.string) (txt1, txt2);
60858
7bf2188a0998 evaluate ML expressions within debugger context;
wenzelm
parents: 60857
diff changeset
   151
60862
097afdd8a2fd eval ML context;
wenzelm
parents: 60858
diff changeset
   152
    val evaluate_verbose = evaluate {SML = SML, verbose = true};
60858
7bf2188a0998 evaluate ML expressions within debugger context;
wenzelm
parents: 60857
diff changeset
   153
    val context1 = ML_Context.the_generic_context ()
7bf2188a0998 evaluate ML expressions within debugger context;
wenzelm
parents: 60857
diff changeset
   154
      |> Context_Position.set_visible_generic false
60871
9b26f3118e40 clarified ML options;
wenzelm
parents: 60869
diff changeset
   155
      |> Config.put_generic ML_Options.debugger false
60862
097afdd8a2fd eval ML context;
wenzelm
parents: 60858
diff changeset
   156
      |> ML_Env.add_name_space {SML = SML}
097afdd8a2fd eval ML context;
wenzelm
parents: 60858
diff changeset
   157
          (ML_Debugger.debug_name_space (the_debug_state thread_name index));
097afdd8a2fd eval ML context;
wenzelm
parents: 60858
diff changeset
   158
    val context2 =
097afdd8a2fd eval ML context;
wenzelm
parents: 60858
diff changeset
   159
      if SML orelse forall (fn Antiquote.Text tok => ML_Lex.is_improper tok | _ => false) toks1
097afdd8a2fd eval ML context;
wenzelm
parents: 60858
diff changeset
   160
      then context1
097afdd8a2fd eval ML context;
wenzelm
parents: 60858
diff changeset
   161
      else
097afdd8a2fd eval ML context;
wenzelm
parents: 60858
diff changeset
   162
        let
097afdd8a2fd eval ML context;
wenzelm
parents: 60858
diff changeset
   163
          val context' = context1
097afdd8a2fd eval ML context;
wenzelm
parents: 60858
diff changeset
   164
            |> ML_Context.exec (fn () => evaluate_verbose (ML_Lex.read "val ML_context = " @ toks1));
097afdd8a2fd eval ML context;
wenzelm
parents: 60858
diff changeset
   165
          fun try_exec toks =
097afdd8a2fd eval ML context;
wenzelm
parents: 60858
diff changeset
   166
            try (ML_Context.exec (fn () => evaluate {SML = false, verbose = false} toks)) context';
097afdd8a2fd eval ML context;
wenzelm
parents: 60858
diff changeset
   167
        in
097afdd8a2fd eval ML context;
wenzelm
parents: 60858
diff changeset
   168
          (case get_first try_exec context_attempts of
097afdd8a2fd eval ML context;
wenzelm
parents: 60858
diff changeset
   169
            SOME context2 => context2
097afdd8a2fd eval ML context;
wenzelm
parents: 60858
diff changeset
   170
          | NONE => error "Malformed context: expected type theory, Proof.context, Context.generic")
097afdd8a2fd eval ML context;
wenzelm
parents: 60858
diff changeset
   171
        end;
097afdd8a2fd eval ML context;
wenzelm
parents: 60858
diff changeset
   172
  in Context.setmp_thread_data (SOME context2) evaluate_verbose toks2 end;
097afdd8a2fd eval ML context;
wenzelm
parents: 60858
diff changeset
   173
097afdd8a2fd eval ML context;
wenzelm
parents: 60858
diff changeset
   174
end;
60749
f727b99faaf7 skeleton for interactive debugger;
wenzelm
parents:
diff changeset
   175
60765
e43e71a75838 support for ML debugger;
wenzelm
parents: 60749
diff changeset
   176
60869
878e32cf3131 more single stepping;
wenzelm
parents: 60864
diff changeset
   177
878e32cf3131 more single stepping;
wenzelm
parents: 60864
diff changeset
   178
(** debugger entry point **)
60857
4c18d8e4fe14 clarified debugger loop;
wenzelm
parents: 60856
diff changeset
   179
4c18d8e4fe14 clarified debugger loop;
wenzelm
parents: 60856
diff changeset
   180
local
60765
e43e71a75838 support for ML debugger;
wenzelm
parents: 60749
diff changeset
   181
60842
5510c8444bc4 protocol support for thread debugger state;
wenzelm
parents: 60834
diff changeset
   182
fun debugger_state thread_name =
5510c8444bc4 protocol support for thread debugger state;
wenzelm
parents: 60834
diff changeset
   183
  Output.protocol_message (Markup.debugger_state thread_name)
60856
eb21ae05ec43 clarified thread state;
wenzelm
parents: 60842
diff changeset
   184
   [get_debugging ()
60842
5510c8444bc4 protocol support for thread debugger state;
wenzelm
parents: 60834
diff changeset
   185
    |> map (fn st =>
5510c8444bc4 protocol support for thread debugger state;
wenzelm
parents: 60834
diff changeset
   186
      (Position.properties_of (Exn_Properties.position_of (ML_Debugger.debug_location st)),
5510c8444bc4 protocol support for thread debugger state;
wenzelm
parents: 60834
diff changeset
   187
       ML_Debugger.debug_function st))
5510c8444bc4 protocol support for thread debugger state;
wenzelm
parents: 60834
diff changeset
   188
    |> let open XML.Encode in list (pair properties string) end
5510c8444bc4 protocol support for thread debugger state;
wenzelm
parents: 60834
diff changeset
   189
    |> YXML.string_of_body];
5510c8444bc4 protocol support for thread debugger state;
wenzelm
parents: 60834
diff changeset
   190
60857
4c18d8e4fe14 clarified debugger loop;
wenzelm
parents: 60856
diff changeset
   191
fun debugger_command thread_name =
4c18d8e4fe14 clarified debugger loop;
wenzelm
parents: 60856
diff changeset
   192
  (case get_input thread_name of
60869
878e32cf3131 more single stepping;
wenzelm
parents: 60864
diff changeset
   193
    ["step"] => (step_stepping (); false)
878e32cf3131 more single stepping;
wenzelm
parents: 60864
diff changeset
   194
  | ["step_over"] => (step_over_stepping (); false)
878e32cf3131 more single stepping;
wenzelm
parents: 60864
diff changeset
   195
  | ["step_out"] => (step_out_stepping (); false)
878e32cf3131 more single stepping;
wenzelm
parents: 60864
diff changeset
   196
  | ["continue"] => (continue_stepping (); false)
60857
4c18d8e4fe14 clarified debugger loop;
wenzelm
parents: 60856
diff changeset
   197
  | ["eval", index, SML, txt1, txt2] =>
4c18d8e4fe14 clarified debugger loop;
wenzelm
parents: 60856
diff changeset
   198
     (error_wrapper (fn () =>
4c18d8e4fe14 clarified debugger loop;
wenzelm
parents: 60856
diff changeset
   199
        eval thread_name (Markup.parse_int index) (Markup.parse_bool SML) txt1 txt2); true)
4c18d8e4fe14 clarified debugger loop;
wenzelm
parents: 60856
diff changeset
   200
  | bad =>
4c18d8e4fe14 clarified debugger loop;
wenzelm
parents: 60856
diff changeset
   201
     (Output.system_message
4c18d8e4fe14 clarified debugger loop;
wenzelm
parents: 60856
diff changeset
   202
        ("Debugger: bad input " ^ ML_Syntax.print_list ML_Syntax.print_string bad); true));
4c18d8e4fe14 clarified debugger loop;
wenzelm
parents: 60856
diff changeset
   203
60842
5510c8444bc4 protocol support for thread debugger state;
wenzelm
parents: 60834
diff changeset
   204
fun debugger_loop thread_name =
60885
d8d51f956f05 report final debugger_state more robustly, e.g. after interrupt;
wenzelm
parents: 60884
diff changeset
   205
  uninterruptible (fn restore_attributes => fn () =>
d8d51f956f05 report final debugger_state more robustly, e.g. after interrupt;
wenzelm
parents: 60884
diff changeset
   206
    let
d8d51f956f05 report final debugger_state more robustly, e.g. after interrupt;
wenzelm
parents: 60884
diff changeset
   207
      fun loop () =
d8d51f956f05 report final debugger_state more robustly, e.g. after interrupt;
wenzelm
parents: 60884
diff changeset
   208
        (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
   209
      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
   210
      val _ = debugger_state thread_name;
d8d51f956f05 report final debugger_state more robustly, e.g. after interrupt;
wenzelm
parents: 60884
diff changeset
   211
    in Exn.release result end) ();
60765
e43e71a75838 support for ML debugger;
wenzelm
parents: 60749
diff changeset
   212
60857
4c18d8e4fe14 clarified debugger loop;
wenzelm
parents: 60856
diff changeset
   213
in
4c18d8e4fe14 clarified debugger loop;
wenzelm
parents: 60856
diff changeset
   214
60765
e43e71a75838 support for ML debugger;
wenzelm
parents: 60749
diff changeset
   215
fun init () =
e43e71a75838 support for ML debugger;
wenzelm
parents: 60749
diff changeset
   216
  ML_Debugger.on_breakpoint
60869
878e32cf3131 more single stepping;
wenzelm
parents: 60864
diff changeset
   217
    (SOME (fn (_, break) =>
878e32cf3131 more single stepping;
wenzelm
parents: 60864
diff changeset
   218
      if not (is_debugging ()) andalso
60884
f3039309702e eliminated global option: breakpoints control this individually;
wenzelm
parents: 60880
diff changeset
   219
        (! break orelse is_stepping ()) andalso
60869
878e32cf3131 more single stepping;
wenzelm
parents: 60864
diff changeset
   220
        Options.default_bool @{system_option ML_debugger_active}
878e32cf3131 more single stepping;
wenzelm
parents: 60864
diff changeset
   221
      then
878e32cf3131 more single stepping;
wenzelm
parents: 60864
diff changeset
   222
        (case Simple_Thread.get_name () of
878e32cf3131 more single stepping;
wenzelm
parents: 60864
diff changeset
   223
          SOME thread_name => debugger_loop thread_name
878e32cf3131 more single stepping;
wenzelm
parents: 60864
diff changeset
   224
        | NONE => ())
878e32cf3131 more single stepping;
wenzelm
parents: 60864
diff changeset
   225
      else ()));
60765
e43e71a75838 support for ML debugger;
wenzelm
parents: 60749
diff changeset
   226
60857
4c18d8e4fe14 clarified debugger loop;
wenzelm
parents: 60856
diff changeset
   227
end;
4c18d8e4fe14 clarified debugger loop;
wenzelm
parents: 60856
diff changeset
   228
60765
e43e71a75838 support for ML debugger;
wenzelm
parents: 60749
diff changeset
   229
60869
878e32cf3131 more single stepping;
wenzelm
parents: 60864
diff changeset
   230
878e32cf3131 more single stepping;
wenzelm
parents: 60864
diff changeset
   231
(** protocol commands **)
60765
e43e71a75838 support for ML debugger;
wenzelm
parents: 60749
diff changeset
   232
e43e71a75838 support for ML debugger;
wenzelm
parents: 60749
diff changeset
   233
val _ =
e43e71a75838 support for ML debugger;
wenzelm
parents: 60749
diff changeset
   234
  Isabelle_Process.protocol_command "Debugger.init"
e43e71a75838 support for ML debugger;
wenzelm
parents: 60749
diff changeset
   235
    (fn [] => init ());
e43e71a75838 support for ML debugger;
wenzelm
parents: 60749
diff changeset
   236
e43e71a75838 support for ML debugger;
wenzelm
parents: 60749
diff changeset
   237
val _ =
60878
1f0d2bbcf38b added action to toggle breakpoints (on editor side);
wenzelm
parents: 60871
diff changeset
   238
  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
   239
    (fn [node_name, id0, breakpoint0, breakpoint_state0] =>
60878
1f0d2bbcf38b added action to toggle breakpoints (on editor side);
wenzelm
parents: 60871
diff changeset
   240
      let
60880
fa958e24ff24 set breakpoint state on ML side, relying on stable situation within the PIDE editing queue;
wenzelm
parents: 60878
diff changeset
   241
        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
   242
        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
   243
        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
   244
fa958e24ff24 set breakpoint state on ML side, relying on stable situation within the PIDE editing queue;
wenzelm
parents: 60878
diff changeset
   245
        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
   246
      in
fa958e24ff24 set breakpoint state on ML side, relying on stable situation within the PIDE editing queue;
wenzelm
parents: 60878
diff changeset
   247
        (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
   248
          SOME (eval, _) =>
fa958e24ff24 set breakpoint state on ML side, relying on stable situation within the PIDE editing queue;
wenzelm
parents: 60878
diff changeset
   249
            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
   250
              let
fa958e24ff24 set breakpoint state on ML side, relying on stable situation within the PIDE editing queue;
wenzelm
parents: 60878
diff changeset
   251
                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
   252
                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
   253
                  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
   254
              in
fa958e24ff24 set breakpoint state on ML side, relying on stable situation within the PIDE editing queue;
wenzelm
parents: 60878
diff changeset
   255
                (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
   256
                  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
   257
                | NONE => err ())
fa958e24ff24 set breakpoint state on ML side, relying on stable situation within the PIDE editing queue;
wenzelm
parents: 60878
diff changeset
   258
              end
fa958e24ff24 set breakpoint state on ML side, relying on stable situation within the PIDE editing queue;
wenzelm
parents: 60878
diff changeset
   259
            else err ()
fa958e24ff24 set breakpoint state on ML side, relying on stable situation within the PIDE editing queue;
wenzelm
parents: 60878
diff changeset
   260
        | NONE => err ())
fa958e24ff24 set breakpoint state on ML side, relying on stable situation within the PIDE editing queue;
wenzelm
parents: 60878
diff changeset
   261
      end);
60878
1f0d2bbcf38b added action to toggle breakpoints (on editor side);
wenzelm
parents: 60871
diff changeset
   262
1f0d2bbcf38b added action to toggle breakpoints (on editor side);
wenzelm
parents: 60871
diff changeset
   263
val _ =
60765
e43e71a75838 support for ML debugger;
wenzelm
parents: 60749
diff changeset
   264
  Isabelle_Process.protocol_command "Debugger.cancel"
60842
5510c8444bc4 protocol support for thread debugger state;
wenzelm
parents: 60834
diff changeset
   265
    (fn [thread_name] => cancel thread_name);
60765
e43e71a75838 support for ML debugger;
wenzelm
parents: 60749
diff changeset
   266
e43e71a75838 support for ML debugger;
wenzelm
parents: 60749
diff changeset
   267
val _ =
e43e71a75838 support for ML debugger;
wenzelm
parents: 60749
diff changeset
   268
  Isabelle_Process.protocol_command "Debugger.input"
60842
5510c8444bc4 protocol support for thread debugger state;
wenzelm
parents: 60834
diff changeset
   269
    (fn thread_name :: msg => input thread_name msg);
60765
e43e71a75838 support for ML debugger;
wenzelm
parents: 60749
diff changeset
   270
60749
f727b99faaf7 skeleton for interactive debugger;
wenzelm
parents:
diff changeset
   271
end;