src/Pure/Tools/debugger.ML
author wenzelm
Fri, 18 Mar 2016 16:26:35 +0100
changeset 62663 bea354f6ff21
parent 62516 5732f1c31566
child 62821 48c24d0b6d85
permissions -rw-r--r--
clarified modules; tuned signature;
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
61556
0d4ee4168e41 clarified modules;
wenzelm
parents: 60956
diff changeset
    27
      (Markup.debugger_output (Standard_Thread.the_name ()))
60864
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 =>
62505
9e2a65912111 clarified modules;
wenzelm
parents: 62504
diff changeset
    36
    if Exn.is_interrupt exn then Exn.reraise exn
60856
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
60932
13ee73f57c85 allow to break running threads at next possible breakpoint (simplified version of former option, see f3039309702e);
wenzelm
parents: 60931
diff changeset
    69
(* global break *)
13ee73f57c85 allow to break running threads at next possible breakpoint (simplified version of former option, see f3039309702e);
wenzelm
parents: 60931
diff changeset
    70
13ee73f57c85 allow to break running threads at next possible breakpoint (simplified version of former option, see f3039309702e);
wenzelm
parents: 60931
diff changeset
    71
local
13ee73f57c85 allow to break running threads at next possible breakpoint (simplified version of former option, see f3039309702e);
wenzelm
parents: 60931
diff changeset
    72
  val break = Synchronized.var "Debugger.break" false;
13ee73f57c85 allow to break running threads at next possible breakpoint (simplified version of former option, see f3039309702e);
wenzelm
parents: 60931
diff changeset
    73
in
13ee73f57c85 allow to break running threads at next possible breakpoint (simplified version of former option, see f3039309702e);
wenzelm
parents: 60931
diff changeset
    74
13ee73f57c85 allow to break running threads at next possible breakpoint (simplified version of former option, see f3039309702e);
wenzelm
parents: 60931
diff changeset
    75
fun is_break () = Synchronized.value break;
13ee73f57c85 allow to break running threads at next possible breakpoint (simplified version of former option, see f3039309702e);
wenzelm
parents: 60931
diff changeset
    76
fun set_break b = Synchronized.change break (K b);
13ee73f57c85 allow to break running threads at next possible breakpoint (simplified version of former option, see f3039309702e);
wenzelm
parents: 60931
diff changeset
    77
13ee73f57c85 allow to break running threads at next possible breakpoint (simplified version of former option, see f3039309702e);
wenzelm
parents: 60931
diff changeset
    78
end;
13ee73f57c85 allow to break running threads at next possible breakpoint (simplified version of former option, see f3039309702e);
wenzelm
parents: 60931
diff changeset
    79
13ee73f57c85 allow to break running threads at next possible breakpoint (simplified version of former option, see f3039309702e);
wenzelm
parents: 60931
diff changeset
    80
60869
878e32cf3131 more single stepping;
wenzelm
parents: 60864
diff changeset
    81
878e32cf3131 more single stepping;
wenzelm
parents: 60864
diff changeset
    82
(** thread state **)
878e32cf3131 more single stepping;
wenzelm
parents: 60864
diff changeset
    83
878e32cf3131 more single stepping;
wenzelm
parents: 60864
diff changeset
    84
(* stack frame during debugging *)
60856
eb21ae05ec43 clarified thread state;
wenzelm
parents: 60842
diff changeset
    85
eb21ae05ec43 clarified thread state;
wenzelm
parents: 60842
diff changeset
    86
local
eb21ae05ec43 clarified thread state;
wenzelm
parents: 60842
diff changeset
    87
  val tag = Universal.tag () : ML_Debugger.state list Universal.tag;
eb21ae05ec43 clarified thread state;
wenzelm
parents: 60842
diff changeset
    88
in
60765
e43e71a75838 support for ML debugger;
wenzelm
parents: 60749
diff changeset
    89
60856
eb21ae05ec43 clarified thread state;
wenzelm
parents: 60842
diff changeset
    90
fun get_debugging () = the_default [] (Thread.getLocal tag);
eb21ae05ec43 clarified thread state;
wenzelm
parents: 60842
diff changeset
    91
val is_debugging = not o null o get_debugging;
60765
e43e71a75838 support for ML debugger;
wenzelm
parents: 60749
diff changeset
    92
60856
eb21ae05ec43 clarified thread state;
wenzelm
parents: 60842
diff changeset
    93
fun with_debugging e =
eb21ae05ec43 clarified thread state;
wenzelm
parents: 60842
diff changeset
    94
  setmp_thread_data tag (get_debugging ()) (ML_Debugger.state (Thread.self ())) e ();
60765
e43e71a75838 support for ML debugger;
wenzelm
parents: 60749
diff changeset
    95
60749
f727b99faaf7 skeleton for interactive debugger;
wenzelm
parents:
diff changeset
    96
end;
f727b99faaf7 skeleton for interactive debugger;
wenzelm
parents:
diff changeset
    97
60858
7bf2188a0998 evaluate ML expressions within debugger context;
wenzelm
parents: 60857
diff changeset
    98
fun the_debug_state thread_name index =
7bf2188a0998 evaluate ML expressions within debugger context;
wenzelm
parents: 60857
diff changeset
    99
  (case get_debugging () of
7bf2188a0998 evaluate ML expressions within debugger context;
wenzelm
parents: 60857
diff changeset
   100
    [] => error ("Missing debugger information for thread " ^ quote thread_name)
7bf2188a0998 evaluate ML expressions within debugger context;
wenzelm
parents: 60857
diff changeset
   101
  | states =>
7bf2188a0998 evaluate ML expressions within debugger context;
wenzelm
parents: 60857
diff changeset
   102
      if index < 0 orelse index >= length states then
7bf2188a0998 evaluate ML expressions within debugger context;
wenzelm
parents: 60857
diff changeset
   103
        error ("Bad debugger stack index " ^ signed_string_of_int index ^ " for thread " ^
7bf2188a0998 evaluate ML expressions within debugger context;
wenzelm
parents: 60857
diff changeset
   104
          quote thread_name)
7bf2188a0998 evaluate ML expressions within debugger context;
wenzelm
parents: 60857
diff changeset
   105
      else nth states index);
7bf2188a0998 evaluate ML expressions within debugger context;
wenzelm
parents: 60857
diff changeset
   106
7bf2188a0998 evaluate ML expressions within debugger context;
wenzelm
parents: 60857
diff changeset
   107
60869
878e32cf3131 more single stepping;
wenzelm
parents: 60864
diff changeset
   108
(* flags for single-stepping *)
60765
e43e71a75838 support for ML debugger;
wenzelm
parents: 60749
diff changeset
   109
60869
878e32cf3131 more single stepping;
wenzelm
parents: 60864
diff changeset
   110
datatype stepping = Stepping of bool * int;  (*stepping enabled, stack depth limit*)
878e32cf3131 more single stepping;
wenzelm
parents: 60864
diff changeset
   111
878e32cf3131 more single stepping;
wenzelm
parents: 60864
diff changeset
   112
local
878e32cf3131 more single stepping;
wenzelm
parents: 60864
diff changeset
   113
  val tag = Universal.tag () : stepping Universal.tag;
878e32cf3131 more single stepping;
wenzelm
parents: 60864
diff changeset
   114
in
878e32cf3131 more single stepping;
wenzelm
parents: 60864
diff changeset
   115
878e32cf3131 more single stepping;
wenzelm
parents: 60864
diff changeset
   116
fun get_stepping () = the_default (Stepping (false, ~1)) (Thread.getLocal tag);
878e32cf3131 more single stepping;
wenzelm
parents: 60864
diff changeset
   117
fun put_stepping stepping = Thread.setLocal (tag, Stepping stepping);
878e32cf3131 more single stepping;
wenzelm
parents: 60864
diff changeset
   118
878e32cf3131 more single stepping;
wenzelm
parents: 60864
diff changeset
   119
end;
878e32cf3131 more single stepping;
wenzelm
parents: 60864
diff changeset
   120
878e32cf3131 more single stepping;
wenzelm
parents: 60864
diff changeset
   121
fun is_stepping () =
878e32cf3131 more single stepping;
wenzelm
parents: 60864
diff changeset
   122
  let
878e32cf3131 more single stepping;
wenzelm
parents: 60864
diff changeset
   123
    val stack = ML_Debugger.state (Thread.self ());
878e32cf3131 more single stepping;
wenzelm
parents: 60864
diff changeset
   124
    val Stepping (stepping, depth) = get_stepping ();
878e32cf3131 more single stepping;
wenzelm
parents: 60864
diff changeset
   125
  in stepping andalso (depth < 0 orelse length stack <= depth) end;
878e32cf3131 more single stepping;
wenzelm
parents: 60864
diff changeset
   126
60931
f4bc0400bd15 tuned signature;
wenzelm
parents: 60924
diff changeset
   127
fun continue () = put_stepping (false, ~1);
f4bc0400bd15 tuned signature;
wenzelm
parents: 60924
diff changeset
   128
fun step () = put_stepping (true, ~1);
f4bc0400bd15 tuned signature;
wenzelm
parents: 60924
diff changeset
   129
fun step_over () = put_stepping (true, length (get_debugging ()));
f4bc0400bd15 tuned signature;
wenzelm
parents: 60924
diff changeset
   130
fun step_out () = put_stepping (true, length (get_debugging ()) - 1);
60869
878e32cf3131 more single stepping;
wenzelm
parents: 60864
diff changeset
   131
878e32cf3131 more single stepping;
wenzelm
parents: 60864
diff changeset
   132
60935
441c03582afa proper setup of evaluation context;
wenzelm
parents: 60932
diff changeset
   133
60869
878e32cf3131 more single stepping;
wenzelm
parents: 60864
diff changeset
   134
(** eval ML **)
60765
e43e71a75838 support for ML debugger;
wenzelm
parents: 60749
diff changeset
   135
60862
097afdd8a2fd eval ML context;
wenzelm
parents: 60858
diff changeset
   136
local
097afdd8a2fd eval ML context;
wenzelm
parents: 60858
diff changeset
   137
097afdd8a2fd eval ML context;
wenzelm
parents: 60858
diff changeset
   138
val context_attempts =
097afdd8a2fd eval ML context;
wenzelm
parents: 60858
diff changeset
   139
  map ML_Lex.read
097afdd8a2fd eval ML context;
wenzelm
parents: 60858
diff changeset
   140
   ["Context.set_thread_data (SOME (Context.Theory ML_context))",
097afdd8a2fd eval ML context;
wenzelm
parents: 60858
diff changeset
   141
    "Context.set_thread_data (SOME (Context.Proof ML_context))",
097afdd8a2fd eval ML context;
wenzelm
parents: 60858
diff changeset
   142
    "Context.set_thread_data (SOME ML_context)"];
097afdd8a2fd eval ML context;
wenzelm
parents: 60858
diff changeset
   143
097afdd8a2fd eval ML context;
wenzelm
parents: 60858
diff changeset
   144
fun evaluate {SML, verbose} =
097afdd8a2fd eval ML context;
wenzelm
parents: 60858
diff changeset
   145
  ML_Context.eval
097afdd8a2fd eval ML context;
wenzelm
parents: 60858
diff changeset
   146
    {SML = SML, exchange = false, redirect = false, verbose = verbose,
60956
10d463883dc2 explicit debug flag for ML compiler;
wenzelm
parents: 60935
diff changeset
   147
      debug = SOME false, writeln = writeln_message, warning = warning_message}
60862
097afdd8a2fd eval ML context;
wenzelm
parents: 60858
diff changeset
   148
    Position.none;
097afdd8a2fd eval ML context;
wenzelm
parents: 60858
diff changeset
   149
60935
441c03582afa proper setup of evaluation context;
wenzelm
parents: 60932
diff changeset
   150
fun eval_setup thread_name index SML context =
441c03582afa proper setup of evaluation context;
wenzelm
parents: 60932
diff changeset
   151
  context
441c03582afa proper setup of evaluation context;
wenzelm
parents: 60932
diff changeset
   152
  |> Context_Position.set_visible_generic false
441c03582afa proper setup of evaluation context;
wenzelm
parents: 60932
diff changeset
   153
  |> ML_Env.add_name_space {SML = SML}
441c03582afa proper setup of evaluation context;
wenzelm
parents: 60932
diff changeset
   154
      (ML_Debugger.debug_name_space (the_debug_state thread_name index));
441c03582afa proper setup of evaluation context;
wenzelm
parents: 60932
diff changeset
   155
60897
7aad4be8a48e print values for stack entry;
wenzelm
parents: 60891
diff changeset
   156
fun eval_context thread_name index SML toks =
60858
7bf2188a0998 evaluate ML expressions within debugger context;
wenzelm
parents: 60857
diff changeset
   157
  let
60935
441c03582afa proper setup of evaluation context;
wenzelm
parents: 60932
diff changeset
   158
    val context = ML_Context.the_generic_context ();
60897
7aad4be8a48e print values for stack entry;
wenzelm
parents: 60891
diff changeset
   159
    val context1 =
7aad4be8a48e print values for stack entry;
wenzelm
parents: 60891
diff changeset
   160
      if SML orelse forall (fn Antiquote.Text tok => ML_Lex.is_improper tok | _ => false) toks
60935
441c03582afa proper setup of evaluation context;
wenzelm
parents: 60932
diff changeset
   161
      then context
60862
097afdd8a2fd eval ML context;
wenzelm
parents: 60858
diff changeset
   162
      else
097afdd8a2fd eval ML context;
wenzelm
parents: 60858
diff changeset
   163
        let
60935
441c03582afa proper setup of evaluation context;
wenzelm
parents: 60932
diff changeset
   164
          val context' = context
441c03582afa proper setup of evaluation context;
wenzelm
parents: 60932
diff changeset
   165
            |> eval_setup thread_name index SML
60897
7aad4be8a48e print values for stack entry;
wenzelm
parents: 60891
diff changeset
   166
            |> ML_Context.exec (fn () =>
7aad4be8a48e print values for stack entry;
wenzelm
parents: 60891
diff changeset
   167
                evaluate {SML = SML, verbose = true} (ML_Lex.read "val ML_context = " @ toks));
60862
097afdd8a2fd eval ML context;
wenzelm
parents: 60858
diff changeset
   168
          fun try_exec toks =
097afdd8a2fd eval ML context;
wenzelm
parents: 60858
diff changeset
   169
            try (ML_Context.exec (fn () => evaluate {SML = false, verbose = false} toks)) context';
097afdd8a2fd eval ML context;
wenzelm
parents: 60858
diff changeset
   170
        in
097afdd8a2fd eval ML context;
wenzelm
parents: 60858
diff changeset
   171
          (case get_first try_exec context_attempts of
097afdd8a2fd eval ML context;
wenzelm
parents: 60858
diff changeset
   172
            SOME context2 => context2
097afdd8a2fd eval ML context;
wenzelm
parents: 60858
diff changeset
   173
          | NONE => error "Malformed context: expected type theory, Proof.context, Context.generic")
097afdd8a2fd eval ML context;
wenzelm
parents: 60858
diff changeset
   174
        end;
60935
441c03582afa proper setup of evaluation context;
wenzelm
parents: 60932
diff changeset
   175
  in context1 |> eval_setup thread_name index SML end;
60897
7aad4be8a48e print values for stack entry;
wenzelm
parents: 60891
diff changeset
   176
7aad4be8a48e print values for stack entry;
wenzelm
parents: 60891
diff changeset
   177
in
7aad4be8a48e print values for stack entry;
wenzelm
parents: 60891
diff changeset
   178
7aad4be8a48e print values for stack entry;
wenzelm
parents: 60891
diff changeset
   179
fun eval thread_name index SML txt1 txt2 =
7aad4be8a48e print values for stack entry;
wenzelm
parents: 60891
diff changeset
   180
  let
7aad4be8a48e print values for stack entry;
wenzelm
parents: 60891
diff changeset
   181
    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
   182
    val context = eval_context thread_name index SML toks1;
60904
e0fab97c989f proper context (amending 7aad4be8a48e);
wenzelm
parents: 60897
diff changeset
   183
  in Context.setmp_thread_data (SOME context) (evaluate {SML = SML, verbose = true}) toks2 end;
60897
7aad4be8a48e print values for stack entry;
wenzelm
parents: 60891
diff changeset
   184
7aad4be8a48e print values for stack entry;
wenzelm
parents: 60891
diff changeset
   185
fun print_vals thread_name index SML txt =
7aad4be8a48e print values for stack entry;
wenzelm
parents: 60891
diff changeset
   186
  let
60935
441c03582afa proper setup of evaluation context;
wenzelm
parents: 60932
diff changeset
   187
    val toks = ML_Lex.read_source SML (Input.string txt)
441c03582afa proper setup of evaluation context;
wenzelm
parents: 60932
diff changeset
   188
    val context = eval_context thread_name index SML toks;
60897
7aad4be8a48e print values for stack entry;
wenzelm
parents: 60891
diff changeset
   189
    val space = ML_Debugger.debug_name_space (the_debug_state thread_name index);
7aad4be8a48e print values for stack entry;
wenzelm
parents: 60891
diff changeset
   190
7aad4be8a48e print values for stack entry;
wenzelm
parents: 60891
diff changeset
   191
    fun print x =
62663
bea354f6ff21 clarified modules;
wenzelm
parents: 62516
diff changeset
   192
      Pretty.from_polyml
bea354f6ff21 clarified modules;
wenzelm
parents: 62516
diff changeset
   193
        (ML_Name_Space.displayVal (x, FixedInt.fromInt (ML_Options.get_print_depth ()), space));
60897
7aad4be8a48e print values for stack entry;
wenzelm
parents: 60891
diff changeset
   194
    fun print_all () =
61886
5a9a85c4cfb3 tuned message;
wenzelm
parents: 61556
diff changeset
   195
      #allVal (ML_Debugger.debug_local_name_space (the_debug_state thread_name index)) ()
60924
610794dff23c tuned signature, in accordance to sortBy in Scala;
wenzelm
parents: 60904
diff changeset
   196
      |> sort_by #1 |> map (Pretty.item o single o print o #2)
60897
7aad4be8a48e print values for stack entry;
wenzelm
parents: 60891
diff changeset
   197
      |> Pretty.chunks |> Pretty.string_of |> writeln_message;
7aad4be8a48e print values for stack entry;
wenzelm
parents: 60891
diff changeset
   198
  in Context.setmp_thread_data (SOME context) print_all () end;
60862
097afdd8a2fd eval ML context;
wenzelm
parents: 60858
diff changeset
   199
097afdd8a2fd eval ML context;
wenzelm
parents: 60858
diff changeset
   200
end;
60749
f727b99faaf7 skeleton for interactive debugger;
wenzelm
parents:
diff changeset
   201
60765
e43e71a75838 support for ML debugger;
wenzelm
parents: 60749
diff changeset
   202
60869
878e32cf3131 more single stepping;
wenzelm
parents: 60864
diff changeset
   203
60891
89b7c84b0480 vacuous input means continue, e.g. after exit;
wenzelm
parents: 60889
diff changeset
   204
(** debugger loop **)
60857
4c18d8e4fe14 clarified debugger loop;
wenzelm
parents: 60856
diff changeset
   205
4c18d8e4fe14 clarified debugger loop;
wenzelm
parents: 60856
diff changeset
   206
local
60765
e43e71a75838 support for ML debugger;
wenzelm
parents: 60749
diff changeset
   207
60842
5510c8444bc4 protocol support for thread debugger state;
wenzelm
parents: 60834
diff changeset
   208
fun debugger_state thread_name =
5510c8444bc4 protocol support for thread debugger state;
wenzelm
parents: 60834
diff changeset
   209
  Output.protocol_message (Markup.debugger_state thread_name)
60856
eb21ae05ec43 clarified thread state;
wenzelm
parents: 60842
diff changeset
   210
   [get_debugging ()
60842
5510c8444bc4 protocol support for thread debugger state;
wenzelm
parents: 60834
diff changeset
   211
    |> map (fn st =>
62516
5732f1c31566 tuned signature -- clarified modules;
wenzelm
parents: 62505
diff changeset
   212
      (Position.properties_of (Exn_Properties.position_of_location (ML_Debugger.debug_location st)),
60842
5510c8444bc4 protocol support for thread debugger state;
wenzelm
parents: 60834
diff changeset
   213
       ML_Debugger.debug_function st))
5510c8444bc4 protocol support for thread debugger state;
wenzelm
parents: 60834
diff changeset
   214
    |> let open XML.Encode in list (pair properties string) end
5510c8444bc4 protocol support for thread debugger state;
wenzelm
parents: 60834
diff changeset
   215
    |> YXML.string_of_body];
5510c8444bc4 protocol support for thread debugger state;
wenzelm
parents: 60834
diff changeset
   216
60857
4c18d8e4fe14 clarified debugger loop;
wenzelm
parents: 60856
diff changeset
   217
fun debugger_command thread_name =
4c18d8e4fe14 clarified debugger loop;
wenzelm
parents: 60856
diff changeset
   218
  (case get_input thread_name of
60931
f4bc0400bd15 tuned signature;
wenzelm
parents: 60924
diff changeset
   219
    [] => (continue (); false)
f4bc0400bd15 tuned signature;
wenzelm
parents: 60924
diff changeset
   220
  | ["continue"] => (continue (); false)
f4bc0400bd15 tuned signature;
wenzelm
parents: 60924
diff changeset
   221
  | ["step"] => (step (); false)
f4bc0400bd15 tuned signature;
wenzelm
parents: 60924
diff changeset
   222
  | ["step_over"] => (step_over (); false)
f4bc0400bd15 tuned signature;
wenzelm
parents: 60924
diff changeset
   223
  | ["step_out"] => (step_out (); false)
60857
4c18d8e4fe14 clarified debugger loop;
wenzelm
parents: 60856
diff changeset
   224
  | ["eval", index, SML, txt1, txt2] =>
4c18d8e4fe14 clarified debugger loop;
wenzelm
parents: 60856
diff changeset
   225
     (error_wrapper (fn () =>
4c18d8e4fe14 clarified debugger loop;
wenzelm
parents: 60856
diff changeset
   226
        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
   227
  | ["print_vals", index, SML, txt] =>
7aad4be8a48e print values for stack entry;
wenzelm
parents: 60891
diff changeset
   228
     (error_wrapper (fn () =>
7aad4be8a48e print values for stack entry;
wenzelm
parents: 60891
diff changeset
   229
        print_vals thread_name (Markup.parse_int index) (Markup.parse_bool SML) txt); true)
60857
4c18d8e4fe14 clarified debugger loop;
wenzelm
parents: 60856
diff changeset
   230
  | bad =>
4c18d8e4fe14 clarified debugger loop;
wenzelm
parents: 60856
diff changeset
   231
     (Output.system_message
4c18d8e4fe14 clarified debugger loop;
wenzelm
parents: 60856
diff changeset
   232
        ("Debugger: bad input " ^ ML_Syntax.print_list ML_Syntax.print_string bad); true));
4c18d8e4fe14 clarified debugger loop;
wenzelm
parents: 60856
diff changeset
   233
60889
7f210887cc4e init/exit depending on active debugger panels;
wenzelm
parents: 60888
diff changeset
   234
in
7f210887cc4e init/exit depending on active debugger panels;
wenzelm
parents: 60888
diff changeset
   235
60842
5510c8444bc4 protocol support for thread debugger state;
wenzelm
parents: 60834
diff changeset
   236
fun debugger_loop thread_name =
60885
d8d51f956f05 report final debugger_state more robustly, e.g. after interrupt;
wenzelm
parents: 60884
diff changeset
   237
  uninterruptible (fn restore_attributes => fn () =>
d8d51f956f05 report final debugger_state more robustly, e.g. after interrupt;
wenzelm
parents: 60884
diff changeset
   238
    let
d8d51f956f05 report final debugger_state more robustly, e.g. after interrupt;
wenzelm
parents: 60884
diff changeset
   239
      fun loop () =
d8d51f956f05 report final debugger_state more robustly, e.g. after interrupt;
wenzelm
parents: 60884
diff changeset
   240
        (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
   241
      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
   242
      val _ = debugger_state thread_name;
d8d51f956f05 report final debugger_state more robustly, e.g. after interrupt;
wenzelm
parents: 60884
diff changeset
   243
    in Exn.release result end) ();
60765
e43e71a75838 support for ML debugger;
wenzelm
parents: 60749
diff changeset
   244
60857
4c18d8e4fe14 clarified debugger loop;
wenzelm
parents: 60856
diff changeset
   245
end;
4c18d8e4fe14 clarified debugger loop;
wenzelm
parents: 60856
diff changeset
   246
60765
e43e71a75838 support for ML debugger;
wenzelm
parents: 60749
diff changeset
   247
60869
878e32cf3131 more single stepping;
wenzelm
parents: 60864
diff changeset
   248
878e32cf3131 more single stepping;
wenzelm
parents: 60864
diff changeset
   249
(** protocol commands **)
60765
e43e71a75838 support for ML debugger;
wenzelm
parents: 60749
diff changeset
   250
e43e71a75838 support for ML debugger;
wenzelm
parents: 60749
diff changeset
   251
val _ =
e43e71a75838 support for ML debugger;
wenzelm
parents: 60749
diff changeset
   252
  Isabelle_Process.protocol_command "Debugger.init"
60889
7f210887cc4e init/exit depending on active debugger panels;
wenzelm
parents: 60888
diff changeset
   253
    (fn [] =>
60891
89b7c84b0480 vacuous input means continue, e.g. after exit;
wenzelm
parents: 60889
diff changeset
   254
     (init_input ();
60889
7f210887cc4e init/exit depending on active debugger panels;
wenzelm
parents: 60888
diff changeset
   255
      ML_Debugger.on_breakpoint
7f210887cc4e init/exit depending on active debugger panels;
wenzelm
parents: 60888
diff changeset
   256
        (SOME (fn (_, break) =>
60932
13ee73f57c85 allow to break running threads at next possible breakpoint (simplified version of former option, see f3039309702e);
wenzelm
parents: 60931
diff changeset
   257
          if not (is_debugging ()) andalso (! break orelse is_break () orelse is_stepping ())
13ee73f57c85 allow to break running threads at next possible breakpoint (simplified version of former option, see f3039309702e);
wenzelm
parents: 60931
diff changeset
   258
          then
61556
0d4ee4168e41 clarified modules;
wenzelm
parents: 60956
diff changeset
   259
            (case Standard_Thread.get_name () of
60889
7f210887cc4e init/exit depending on active debugger panels;
wenzelm
parents: 60888
diff changeset
   260
              SOME thread_name => debugger_loop thread_name
7f210887cc4e init/exit depending on active debugger panels;
wenzelm
parents: 60888
diff changeset
   261
            | NONE => ())
60891
89b7c84b0480 vacuous input means continue, e.g. after exit;
wenzelm
parents: 60889
diff changeset
   262
          else ()))));
60889
7f210887cc4e init/exit depending on active debugger panels;
wenzelm
parents: 60888
diff changeset
   263
7f210887cc4e init/exit depending on active debugger panels;
wenzelm
parents: 60888
diff changeset
   264
val _ =
7f210887cc4e init/exit depending on active debugger panels;
wenzelm
parents: 60888
diff changeset
   265
  Isabelle_Process.protocol_command "Debugger.exit"
60891
89b7c84b0480 vacuous input means continue, e.g. after exit;
wenzelm
parents: 60889
diff changeset
   266
    (fn [] => (ML_Debugger.on_breakpoint NONE; exit_input ()));
60765
e43e71a75838 support for ML debugger;
wenzelm
parents: 60749
diff changeset
   267
e43e71a75838 support for ML debugger;
wenzelm
parents: 60749
diff changeset
   268
val _ =
60932
13ee73f57c85 allow to break running threads at next possible breakpoint (simplified version of former option, see f3039309702e);
wenzelm
parents: 60931
diff changeset
   269
  Isabelle_Process.protocol_command "Debugger.break"
13ee73f57c85 allow to break running threads at next possible breakpoint (simplified version of former option, see f3039309702e);
wenzelm
parents: 60931
diff changeset
   270
    (fn [b] => set_break (Markup.parse_bool b));
13ee73f57c85 allow to break running threads at next possible breakpoint (simplified version of former option, see f3039309702e);
wenzelm
parents: 60931
diff changeset
   271
13ee73f57c85 allow to break running threads at next possible breakpoint (simplified version of former option, see f3039309702e);
wenzelm
parents: 60931
diff changeset
   272
val _ =
60878
1f0d2bbcf38b added action to toggle breakpoints (on editor side);
wenzelm
parents: 60871
diff changeset
   273
  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
   274
    (fn [node_name, id0, breakpoint0, breakpoint_state0] =>
60878
1f0d2bbcf38b added action to toggle breakpoints (on editor side);
wenzelm
parents: 60871
diff changeset
   275
      let
60880
fa958e24ff24 set breakpoint state on ML side, relying on stable situation within the PIDE editing queue;
wenzelm
parents: 60878
diff changeset
   276
        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
   277
        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
   278
        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
   279
fa958e24ff24 set breakpoint state on ML side, relying on stable situation within the PIDE editing queue;
wenzelm
parents: 60878
diff changeset
   280
        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
   281
      in
fa958e24ff24 set breakpoint state on ML side, relying on stable situation within the PIDE editing queue;
wenzelm
parents: 60878
diff changeset
   282
        (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
   283
          SOME (eval, _) =>
fa958e24ff24 set breakpoint state on ML side, relying on stable situation within the PIDE editing queue;
wenzelm
parents: 60878
diff changeset
   284
            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
   285
              let
fa958e24ff24 set breakpoint state on ML side, relying on stable situation within the PIDE editing queue;
wenzelm
parents: 60878
diff changeset
   286
                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
   287
                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
   288
                  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
   289
              in
fa958e24ff24 set breakpoint state on ML side, relying on stable situation within the PIDE editing queue;
wenzelm
parents: 60878
diff changeset
   290
                (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
   291
                  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
   292
                | NONE => err ())
fa958e24ff24 set breakpoint state on ML side, relying on stable situation within the PIDE editing queue;
wenzelm
parents: 60878
diff changeset
   293
              end
fa958e24ff24 set breakpoint state on ML side, relying on stable situation within the PIDE editing queue;
wenzelm
parents: 60878
diff changeset
   294
            else err ()
fa958e24ff24 set breakpoint state on ML side, relying on stable situation within the PIDE editing queue;
wenzelm
parents: 60878
diff changeset
   295
        | NONE => err ())
fa958e24ff24 set breakpoint state on ML side, relying on stable situation within the PIDE editing queue;
wenzelm
parents: 60878
diff changeset
   296
      end);
60878
1f0d2bbcf38b added action to toggle breakpoints (on editor side);
wenzelm
parents: 60871
diff changeset
   297
1f0d2bbcf38b added action to toggle breakpoints (on editor side);
wenzelm
parents: 60871
diff changeset
   298
val _ =
60765
e43e71a75838 support for ML debugger;
wenzelm
parents: 60749
diff changeset
   299
  Isabelle_Process.protocol_command "Debugger.input"
60842
5510c8444bc4 protocol support for thread debugger state;
wenzelm
parents: 60834
diff changeset
   300
    (fn thread_name :: msg => input thread_name msg);
60765
e43e71a75838 support for ML debugger;
wenzelm
parents: 60749
diff changeset
   301
60749
f727b99faaf7 skeleton for interactive debugger;
wenzelm
parents:
diff changeset
   302
end;