src/Pure/Tools/debugger.ML
author wenzelm
Fri, 07 Aug 2015 14:46:56 +0200
changeset 60862 097afdd8a2fd
parent 60858 7bf2188a0998
child 60864 20cfa048fe7c
permissions -rw-r--r--
eval ML context; tuned GUI;
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
60830
f56e189350b2 separate channel for debugger output;
wenzelm
parents: 60829
diff changeset
    17
(* messages *)
f56e189350b2 separate channel for debugger output;
wenzelm
parents: 60829
diff changeset
    18
60856
eb21ae05ec43 clarified thread state;
wenzelm
parents: 60842
diff changeset
    19
val _ = Session.protocol_handler "isabelle.Debugger$Handler";
eb21ae05ec43 clarified thread state;
wenzelm
parents: 60842
diff changeset
    20
60834
781f1168d31e maintain debugger output messages;
wenzelm
parents: 60830
diff changeset
    21
fun output_message kind msg =
60830
f56e189350b2 separate channel for debugger output;
wenzelm
parents: 60829
diff changeset
    22
  Output.protocol_message
60834
781f1168d31e maintain debugger output messages;
wenzelm
parents: 60830
diff changeset
    23
    (Markup.debugger_output (Simple_Thread.the_name ()))
781f1168d31e maintain debugger output messages;
wenzelm
parents: 60830
diff changeset
    24
    [Markup.markup (kind, Markup.serial_properties (serial ())) msg];
781f1168d31e maintain debugger output messages;
wenzelm
parents: 60830
diff changeset
    25
781f1168d31e maintain debugger output messages;
wenzelm
parents: 60830
diff changeset
    26
val writeln_message = output_message Markup.writelnN;
781f1168d31e maintain debugger output messages;
wenzelm
parents: 60830
diff changeset
    27
val warning_message = output_message Markup.warningN;
781f1168d31e maintain debugger output messages;
wenzelm
parents: 60830
diff changeset
    28
val error_message = output_message Markup.errorN;
60830
f56e189350b2 separate channel for debugger output;
wenzelm
parents: 60829
diff changeset
    29
60856
eb21ae05ec43 clarified thread state;
wenzelm
parents: 60842
diff changeset
    30
fun error_wrapper e = e ()
eb21ae05ec43 clarified thread state;
wenzelm
parents: 60842
diff changeset
    31
  handle exn =>
eb21ae05ec43 clarified thread state;
wenzelm
parents: 60842
diff changeset
    32
    if Exn.is_interrupt exn then reraise exn
eb21ae05ec43 clarified thread state;
wenzelm
parents: 60842
diff changeset
    33
    else error_message (Runtime.exn_message exn);
eb21ae05ec43 clarified thread state;
wenzelm
parents: 60842
diff changeset
    34
60830
f56e189350b2 separate channel for debugger output;
wenzelm
parents: 60829
diff changeset
    35
60765
e43e71a75838 support for ML debugger;
wenzelm
parents: 60749
diff changeset
    36
(* global state *)
e43e71a75838 support for ML debugger;
wenzelm
parents: 60749
diff changeset
    37
e43e71a75838 support for ML debugger;
wenzelm
parents: 60749
diff changeset
    38
datatype state =
e43e71a75838 support for ML debugger;
wenzelm
parents: 60749
diff changeset
    39
  State of {
60829
4b16b778ce0d clarified thread name;
wenzelm
parents: 60765
diff changeset
    40
    threads: Thread.thread Symtab.table,  (*thread name ~> thread*)
4b16b778ce0d clarified thread name;
wenzelm
parents: 60765
diff changeset
    41
    input: string list Queue.T Symtab.table  (*thread name ~> input queue*)
60765
e43e71a75838 support for ML debugger;
wenzelm
parents: 60749
diff changeset
    42
  };
e43e71a75838 support for ML debugger;
wenzelm
parents: 60749
diff changeset
    43
e43e71a75838 support for ML debugger;
wenzelm
parents: 60749
diff changeset
    44
fun make_state (threads, input) = State {threads = threads, input = input};
e43e71a75838 support for ML debugger;
wenzelm
parents: 60749
diff changeset
    45
val init_state = make_state (Symtab.empty, Symtab.empty);
e43e71a75838 support for ML debugger;
wenzelm
parents: 60749
diff changeset
    46
fun map_state f (State {threads, input}) = make_state (f (threads, input));
e43e71a75838 support for ML debugger;
wenzelm
parents: 60749
diff changeset
    47
e43e71a75838 support for ML debugger;
wenzelm
parents: 60749
diff changeset
    48
val global_state = Synchronized.var "Debugger.state" init_state;
e43e71a75838 support for ML debugger;
wenzelm
parents: 60749
diff changeset
    49
60842
5510c8444bc4 protocol support for thread debugger state;
wenzelm
parents: 60834
diff changeset
    50
fun cancel thread_name =
60765
e43e71a75838 support for ML debugger;
wenzelm
parents: 60749
diff changeset
    51
  Synchronized.change global_state (tap (fn State {threads, ...} =>
60842
5510c8444bc4 protocol support for thread debugger state;
wenzelm
parents: 60834
diff changeset
    52
    (case Symtab.lookup threads thread_name of
60765
e43e71a75838 support for ML debugger;
wenzelm
parents: 60749
diff changeset
    53
      NONE => ()
e43e71a75838 support for ML debugger;
wenzelm
parents: 60749
diff changeset
    54
    | SOME thread => Simple_Thread.interrupt_unsynchronized thread)));
e43e71a75838 support for ML debugger;
wenzelm
parents: 60749
diff changeset
    55
60842
5510c8444bc4 protocol support for thread debugger state;
wenzelm
parents: 60834
diff changeset
    56
fun input thread_name msg =
60765
e43e71a75838 support for ML debugger;
wenzelm
parents: 60749
diff changeset
    57
  Synchronized.change global_state (map_state (fn (threads, input) =>
60842
5510c8444bc4 protocol support for thread debugger state;
wenzelm
parents: 60834
diff changeset
    58
    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
    59
    in (threads, input') end));
e43e71a75838 support for ML debugger;
wenzelm
parents: 60749
diff changeset
    60
60842
5510c8444bc4 protocol support for thread debugger state;
wenzelm
parents: 60834
diff changeset
    61
fun get_input thread_name =
60765
e43e71a75838 support for ML debugger;
wenzelm
parents: 60749
diff changeset
    62
  Synchronized.guarded_access global_state (fn State {threads, input} =>
60842
5510c8444bc4 protocol support for thread debugger state;
wenzelm
parents: 60834
diff changeset
    63
    (case Symtab.lookup input thread_name of
60765
e43e71a75838 support for ML debugger;
wenzelm
parents: 60749
diff changeset
    64
      NONE => NONE
e43e71a75838 support for ML debugger;
wenzelm
parents: 60749
diff changeset
    65
    | SOME queue =>
e43e71a75838 support for ML debugger;
wenzelm
parents: 60749
diff changeset
    66
        let
e43e71a75838 support for ML debugger;
wenzelm
parents: 60749
diff changeset
    67
          val (msg, queue') = Queue.dequeue queue;
e43e71a75838 support for ML debugger;
wenzelm
parents: 60749
diff changeset
    68
          val input' =
60842
5510c8444bc4 protocol support for thread debugger state;
wenzelm
parents: 60834
diff changeset
    69
            if Queue.is_empty queue' then Symtab.delete_safe thread_name input
5510c8444bc4 protocol support for thread debugger state;
wenzelm
parents: 60834
diff changeset
    70
            else Symtab.update (thread_name, queue') input;
60765
e43e71a75838 support for ML debugger;
wenzelm
parents: 60749
diff changeset
    71
        in SOME (msg, make_state (threads, input')) end));
e43e71a75838 support for ML debugger;
wenzelm
parents: 60749
diff changeset
    72
e43e71a75838 support for ML debugger;
wenzelm
parents: 60749
diff changeset
    73
60856
eb21ae05ec43 clarified thread state;
wenzelm
parents: 60842
diff changeset
    74
(* thread state *)
eb21ae05ec43 clarified thread state;
wenzelm
parents: 60842
diff changeset
    75
eb21ae05ec43 clarified thread state;
wenzelm
parents: 60842
diff changeset
    76
local
eb21ae05ec43 clarified thread state;
wenzelm
parents: 60842
diff changeset
    77
  val tag = Universal.tag () : ML_Debugger.state list Universal.tag;
eb21ae05ec43 clarified thread state;
wenzelm
parents: 60842
diff changeset
    78
in
60765
e43e71a75838 support for ML debugger;
wenzelm
parents: 60749
diff changeset
    79
60856
eb21ae05ec43 clarified thread state;
wenzelm
parents: 60842
diff changeset
    80
fun get_debugging () = the_default [] (Thread.getLocal tag);
eb21ae05ec43 clarified thread state;
wenzelm
parents: 60842
diff changeset
    81
val is_debugging = not o null o get_debugging;
60765
e43e71a75838 support for ML debugger;
wenzelm
parents: 60749
diff changeset
    82
60856
eb21ae05ec43 clarified thread state;
wenzelm
parents: 60842
diff changeset
    83
fun with_debugging e =
eb21ae05ec43 clarified thread state;
wenzelm
parents: 60842
diff changeset
    84
  setmp_thread_data tag (get_debugging ()) (ML_Debugger.state (Thread.self ())) e ();
60765
e43e71a75838 support for ML debugger;
wenzelm
parents: 60749
diff changeset
    85
60749
f727b99faaf7 skeleton for interactive debugger;
wenzelm
parents:
diff changeset
    86
end;
f727b99faaf7 skeleton for interactive debugger;
wenzelm
parents:
diff changeset
    87
60858
7bf2188a0998 evaluate ML expressions within debugger context;
wenzelm
parents: 60857
diff changeset
    88
fun the_debug_state thread_name index =
7bf2188a0998 evaluate ML expressions within debugger context;
wenzelm
parents: 60857
diff changeset
    89
  (case get_debugging () of
7bf2188a0998 evaluate ML expressions within debugger context;
wenzelm
parents: 60857
diff changeset
    90
    [] => error ("Missing debugger information for thread " ^ quote thread_name)
7bf2188a0998 evaluate ML expressions within debugger context;
wenzelm
parents: 60857
diff changeset
    91
  | states =>
7bf2188a0998 evaluate ML expressions within debugger context;
wenzelm
parents: 60857
diff changeset
    92
      if index < 0 orelse index >= length states then
7bf2188a0998 evaluate ML expressions within debugger context;
wenzelm
parents: 60857
diff changeset
    93
        error ("Bad debugger stack index " ^ signed_string_of_int index ^ " for thread " ^
7bf2188a0998 evaluate ML expressions within debugger context;
wenzelm
parents: 60857
diff changeset
    94
          quote thread_name)
7bf2188a0998 evaluate ML expressions within debugger context;
wenzelm
parents: 60857
diff changeset
    95
      else nth states index);
7bf2188a0998 evaluate ML expressions within debugger context;
wenzelm
parents: 60857
diff changeset
    96
7bf2188a0998 evaluate ML expressions within debugger context;
wenzelm
parents: 60857
diff changeset
    97
60765
e43e71a75838 support for ML debugger;
wenzelm
parents: 60749
diff changeset
    98
60856
eb21ae05ec43 clarified thread state;
wenzelm
parents: 60842
diff changeset
    99
(* eval ML *)
60765
e43e71a75838 support for ML debugger;
wenzelm
parents: 60749
diff changeset
   100
60862
097afdd8a2fd eval ML context;
wenzelm
parents: 60858
diff changeset
   101
local
097afdd8a2fd eval ML context;
wenzelm
parents: 60858
diff changeset
   102
097afdd8a2fd eval ML context;
wenzelm
parents: 60858
diff changeset
   103
val context_attempts =
097afdd8a2fd eval ML context;
wenzelm
parents: 60858
diff changeset
   104
  map ML_Lex.read
097afdd8a2fd eval ML context;
wenzelm
parents: 60858
diff changeset
   105
   ["Context.set_thread_data (SOME (Context.Theory ML_context))",
097afdd8a2fd eval ML context;
wenzelm
parents: 60858
diff changeset
   106
    "Context.set_thread_data (SOME (Context.Proof ML_context))",
097afdd8a2fd eval ML context;
wenzelm
parents: 60858
diff changeset
   107
    "Context.set_thread_data (SOME ML_context)"];
097afdd8a2fd eval ML context;
wenzelm
parents: 60858
diff changeset
   108
097afdd8a2fd eval ML context;
wenzelm
parents: 60858
diff changeset
   109
fun evaluate {SML, verbose} =
097afdd8a2fd eval ML context;
wenzelm
parents: 60858
diff changeset
   110
  ML_Context.eval
097afdd8a2fd eval ML context;
wenzelm
parents: 60858
diff changeset
   111
    {SML = SML, exchange = false, redirect = false, verbose = verbose,
097afdd8a2fd eval ML context;
wenzelm
parents: 60858
diff changeset
   112
      writeln = writeln_message, warning = warning_message}
097afdd8a2fd eval ML context;
wenzelm
parents: 60858
diff changeset
   113
    Position.none;
097afdd8a2fd eval ML context;
wenzelm
parents: 60858
diff changeset
   114
097afdd8a2fd eval ML context;
wenzelm
parents: 60858
diff changeset
   115
in
097afdd8a2fd eval ML context;
wenzelm
parents: 60858
diff changeset
   116
60858
7bf2188a0998 evaluate ML expressions within debugger context;
wenzelm
parents: 60857
diff changeset
   117
fun eval thread_name index SML txt1 txt2 =
7bf2188a0998 evaluate ML expressions within debugger context;
wenzelm
parents: 60857
diff changeset
   118
  let
60862
097afdd8a2fd eval ML context;
wenzelm
parents: 60858
diff changeset
   119
    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
   120
60862
097afdd8a2fd eval ML context;
wenzelm
parents: 60858
diff changeset
   121
    val evaluate_verbose = evaluate {SML = SML, verbose = true};
60858
7bf2188a0998 evaluate ML expressions within debugger context;
wenzelm
parents: 60857
diff changeset
   122
    val context1 = ML_Context.the_generic_context ()
7bf2188a0998 evaluate ML expressions within debugger context;
wenzelm
parents: 60857
diff changeset
   123
      |> Context_Position.set_visible_generic false
60862
097afdd8a2fd eval ML context;
wenzelm
parents: 60858
diff changeset
   124
      |> ML_Env.add_name_space {SML = SML}
097afdd8a2fd eval ML context;
wenzelm
parents: 60858
diff changeset
   125
          (ML_Debugger.debug_name_space (the_debug_state thread_name index));
097afdd8a2fd eval ML context;
wenzelm
parents: 60858
diff changeset
   126
    val context2 =
097afdd8a2fd eval ML context;
wenzelm
parents: 60858
diff changeset
   127
      if SML orelse forall (fn Antiquote.Text tok => ML_Lex.is_improper tok | _ => false) toks1
097afdd8a2fd eval ML context;
wenzelm
parents: 60858
diff changeset
   128
      then context1
097afdd8a2fd eval ML context;
wenzelm
parents: 60858
diff changeset
   129
      else
097afdd8a2fd eval ML context;
wenzelm
parents: 60858
diff changeset
   130
        let
097afdd8a2fd eval ML context;
wenzelm
parents: 60858
diff changeset
   131
          val context' = context1
097afdd8a2fd eval ML context;
wenzelm
parents: 60858
diff changeset
   132
            |> ML_Context.exec (fn () => evaluate_verbose (ML_Lex.read "val ML_context = " @ toks1));
097afdd8a2fd eval ML context;
wenzelm
parents: 60858
diff changeset
   133
          fun try_exec toks =
097afdd8a2fd eval ML context;
wenzelm
parents: 60858
diff changeset
   134
            try (ML_Context.exec (fn () => evaluate {SML = false, verbose = false} toks)) context';
097afdd8a2fd eval ML context;
wenzelm
parents: 60858
diff changeset
   135
        in
097afdd8a2fd eval ML context;
wenzelm
parents: 60858
diff changeset
   136
          (case get_first try_exec context_attempts of
097afdd8a2fd eval ML context;
wenzelm
parents: 60858
diff changeset
   137
            SOME context2 => context2
097afdd8a2fd eval ML context;
wenzelm
parents: 60858
diff changeset
   138
          | NONE => error "Malformed context: expected type theory, Proof.context, Context.generic")
097afdd8a2fd eval ML context;
wenzelm
parents: 60858
diff changeset
   139
        end;
097afdd8a2fd eval ML context;
wenzelm
parents: 60858
diff changeset
   140
  in Context.setmp_thread_data (SOME context2) evaluate_verbose toks2 end;
097afdd8a2fd eval ML context;
wenzelm
parents: 60858
diff changeset
   141
097afdd8a2fd eval ML context;
wenzelm
parents: 60858
diff changeset
   142
end;
60749
f727b99faaf7 skeleton for interactive debugger;
wenzelm
parents:
diff changeset
   143
60765
e43e71a75838 support for ML debugger;
wenzelm
parents: 60749
diff changeset
   144
60857
4c18d8e4fe14 clarified debugger loop;
wenzelm
parents: 60856
diff changeset
   145
(* debugger entry point *)
4c18d8e4fe14 clarified debugger loop;
wenzelm
parents: 60856
diff changeset
   146
4c18d8e4fe14 clarified debugger loop;
wenzelm
parents: 60856
diff changeset
   147
local
60765
e43e71a75838 support for ML debugger;
wenzelm
parents: 60749
diff changeset
   148
60842
5510c8444bc4 protocol support for thread debugger state;
wenzelm
parents: 60834
diff changeset
   149
fun debugger_state thread_name =
5510c8444bc4 protocol support for thread debugger state;
wenzelm
parents: 60834
diff changeset
   150
  Output.protocol_message (Markup.debugger_state thread_name)
60856
eb21ae05ec43 clarified thread state;
wenzelm
parents: 60842
diff changeset
   151
   [get_debugging ()
60842
5510c8444bc4 protocol support for thread debugger state;
wenzelm
parents: 60834
diff changeset
   152
    |> map (fn st =>
5510c8444bc4 protocol support for thread debugger state;
wenzelm
parents: 60834
diff changeset
   153
      (Position.properties_of (Exn_Properties.position_of (ML_Debugger.debug_location st)),
5510c8444bc4 protocol support for thread debugger state;
wenzelm
parents: 60834
diff changeset
   154
       ML_Debugger.debug_function st))
5510c8444bc4 protocol support for thread debugger state;
wenzelm
parents: 60834
diff changeset
   155
    |> let open XML.Encode in list (pair properties string) end
5510c8444bc4 protocol support for thread debugger state;
wenzelm
parents: 60834
diff changeset
   156
    |> YXML.string_of_body];
5510c8444bc4 protocol support for thread debugger state;
wenzelm
parents: 60834
diff changeset
   157
60857
4c18d8e4fe14 clarified debugger loop;
wenzelm
parents: 60856
diff changeset
   158
fun debugger_command thread_name =
4c18d8e4fe14 clarified debugger loop;
wenzelm
parents: 60856
diff changeset
   159
  (case get_input thread_name of
4c18d8e4fe14 clarified debugger loop;
wenzelm
parents: 60856
diff changeset
   160
    ["continue"] => false
4c18d8e4fe14 clarified debugger loop;
wenzelm
parents: 60856
diff changeset
   161
  | ["eval", index, SML, txt1, txt2] =>
4c18d8e4fe14 clarified debugger loop;
wenzelm
parents: 60856
diff changeset
   162
     (error_wrapper (fn () =>
4c18d8e4fe14 clarified debugger loop;
wenzelm
parents: 60856
diff changeset
   163
        eval thread_name (Markup.parse_int index) (Markup.parse_bool SML) txt1 txt2); true)
4c18d8e4fe14 clarified debugger loop;
wenzelm
parents: 60856
diff changeset
   164
  | bad =>
4c18d8e4fe14 clarified debugger loop;
wenzelm
parents: 60856
diff changeset
   165
     (Output.system_message
4c18d8e4fe14 clarified debugger loop;
wenzelm
parents: 60856
diff changeset
   166
        ("Debugger: bad input " ^ ML_Syntax.print_list ML_Syntax.print_string bad); true));
4c18d8e4fe14 clarified debugger loop;
wenzelm
parents: 60856
diff changeset
   167
60842
5510c8444bc4 protocol support for thread debugger state;
wenzelm
parents: 60834
diff changeset
   168
fun debugger_loop thread_name =
60856
eb21ae05ec43 clarified thread state;
wenzelm
parents: 60842
diff changeset
   169
  let
eb21ae05ec43 clarified thread state;
wenzelm
parents: 60842
diff changeset
   170
    fun loop () =
60857
4c18d8e4fe14 clarified debugger loop;
wenzelm
parents: 60856
diff changeset
   171
      (debugger_state thread_name; if debugger_command thread_name then loop () else ());
60856
eb21ae05ec43 clarified thread state;
wenzelm
parents: 60842
diff changeset
   172
  in with_debugging loop; debugger_state thread_name end;
60765
e43e71a75838 support for ML debugger;
wenzelm
parents: 60749
diff changeset
   173
e43e71a75838 support for ML debugger;
wenzelm
parents: 60749
diff changeset
   174
fun debugger cond =
60856
eb21ae05ec43 clarified thread state;
wenzelm
parents: 60842
diff changeset
   175
  if is_debugging () orelse not (cond ()) orelse
60765
e43e71a75838 support for ML debugger;
wenzelm
parents: 60749
diff changeset
   176
    not (Options.default_bool @{system_option ML_debugger_active})
e43e71a75838 support for ML debugger;
wenzelm
parents: 60749
diff changeset
   177
  then ()
e43e71a75838 support for ML debugger;
wenzelm
parents: 60749
diff changeset
   178
  else
60856
eb21ae05ec43 clarified thread state;
wenzelm
parents: 60842
diff changeset
   179
    (case Simple_Thread.get_name () of
eb21ae05ec43 clarified thread state;
wenzelm
parents: 60842
diff changeset
   180
      NONE => ()
eb21ae05ec43 clarified thread state;
wenzelm
parents: 60842
diff changeset
   181
    | SOME thread_name => debugger_loop thread_name);
60765
e43e71a75838 support for ML debugger;
wenzelm
parents: 60749
diff changeset
   182
60857
4c18d8e4fe14 clarified debugger loop;
wenzelm
parents: 60856
diff changeset
   183
in
4c18d8e4fe14 clarified debugger loop;
wenzelm
parents: 60856
diff changeset
   184
60765
e43e71a75838 support for ML debugger;
wenzelm
parents: 60749
diff changeset
   185
fun init () =
e43e71a75838 support for ML debugger;
wenzelm
parents: 60749
diff changeset
   186
  ML_Debugger.on_breakpoint
e43e71a75838 support for ML debugger;
wenzelm
parents: 60749
diff changeset
   187
    (SOME (fn (_, b) =>
e43e71a75838 support for ML debugger;
wenzelm
parents: 60749
diff changeset
   188
      debugger (fn () => ! b orelse Options.default_bool @{system_option ML_debugger_stepping})));
e43e71a75838 support for ML debugger;
wenzelm
parents: 60749
diff changeset
   189
60857
4c18d8e4fe14 clarified debugger loop;
wenzelm
parents: 60856
diff changeset
   190
end;
4c18d8e4fe14 clarified debugger loop;
wenzelm
parents: 60856
diff changeset
   191
60765
e43e71a75838 support for ML debugger;
wenzelm
parents: 60749
diff changeset
   192
e43e71a75838 support for ML debugger;
wenzelm
parents: 60749
diff changeset
   193
(* protocol commands *)
e43e71a75838 support for ML debugger;
wenzelm
parents: 60749
diff changeset
   194
e43e71a75838 support for ML debugger;
wenzelm
parents: 60749
diff changeset
   195
val _ =
e43e71a75838 support for ML debugger;
wenzelm
parents: 60749
diff changeset
   196
  Isabelle_Process.protocol_command "Debugger.init"
e43e71a75838 support for ML debugger;
wenzelm
parents: 60749
diff changeset
   197
    (fn [] => init ());
e43e71a75838 support for ML debugger;
wenzelm
parents: 60749
diff changeset
   198
e43e71a75838 support for ML debugger;
wenzelm
parents: 60749
diff changeset
   199
val _ =
e43e71a75838 support for ML debugger;
wenzelm
parents: 60749
diff changeset
   200
  Isabelle_Process.protocol_command "Debugger.cancel"
60842
5510c8444bc4 protocol support for thread debugger state;
wenzelm
parents: 60834
diff changeset
   201
    (fn [thread_name] => cancel thread_name);
60765
e43e71a75838 support for ML debugger;
wenzelm
parents: 60749
diff changeset
   202
e43e71a75838 support for ML debugger;
wenzelm
parents: 60749
diff changeset
   203
val _ =
e43e71a75838 support for ML debugger;
wenzelm
parents: 60749
diff changeset
   204
  Isabelle_Process.protocol_command "Debugger.input"
60842
5510c8444bc4 protocol support for thread debugger state;
wenzelm
parents: 60834
diff changeset
   205
    (fn thread_name :: msg => input thread_name msg);
60765
e43e71a75838 support for ML debugger;
wenzelm
parents: 60749
diff changeset
   206
60749
f727b99faaf7 skeleton for interactive debugger;
wenzelm
parents:
diff changeset
   207
end;