src/Pure/Tools/debugger.ML
author wenzelm
Tue Jul 21 19:04:36 2015 +0200 (2015-07-21)
changeset 60765 e43e71a75838
parent 60749 f727b99faaf7
child 60829 4b16b778ce0d
permissions -rw-r--r--
support for ML debugger;
wenzelm@60749
     1
(*  Title:      Pure/Tools/debugger.ML
wenzelm@60749
     2
    Author:     Makarius
wenzelm@60749
     3
wenzelm@60749
     4
Interactive debugger for Isabelle/ML.
wenzelm@60749
     5
*)
wenzelm@60749
     6
wenzelm@60765
     7
structure Debugger: sig end =
wenzelm@60765
     8
struct
wenzelm@60765
     9
wenzelm@60765
    10
(* global state *)
wenzelm@60765
    11
wenzelm@60765
    12
datatype state =
wenzelm@60765
    13
  State of {
wenzelm@60765
    14
    threads: Thread.thread Symtab.table,  (*thread identification ~> thread*)
wenzelm@60765
    15
    input: string list Queue.T Symtab.table  (*thread identification ~> input queue*)
wenzelm@60765
    16
  };
wenzelm@60765
    17
wenzelm@60765
    18
fun make_state (threads, input) = State {threads = threads, input = input};
wenzelm@60765
    19
val init_state = make_state (Symtab.empty, Symtab.empty);
wenzelm@60765
    20
fun map_state f (State {threads, input}) = make_state (f (threads, input));
wenzelm@60765
    21
wenzelm@60765
    22
val global_state = Synchronized.var "Debugger.state" init_state;
wenzelm@60765
    23
wenzelm@60765
    24
fun cancel id =
wenzelm@60765
    25
  Synchronized.change global_state (tap (fn State {threads, ...} =>
wenzelm@60765
    26
    (case Symtab.lookup threads id of
wenzelm@60765
    27
      NONE => ()
wenzelm@60765
    28
    | SOME thread => Simple_Thread.interrupt_unsynchronized thread)));
wenzelm@60765
    29
wenzelm@60765
    30
fun input id msg =
wenzelm@60765
    31
  Synchronized.change global_state (map_state (fn (threads, input) =>
wenzelm@60765
    32
    let val input' = Symtab.map_default (id, Queue.empty) (Queue.enqueue msg) input;
wenzelm@60765
    33
    in (threads, input') end));
wenzelm@60765
    34
wenzelm@60765
    35
fun get_input id =
wenzelm@60765
    36
  Synchronized.guarded_access global_state (fn State {threads, input} =>
wenzelm@60765
    37
    (case Symtab.lookup input id of
wenzelm@60765
    38
      NONE => NONE
wenzelm@60765
    39
    | SOME queue =>
wenzelm@60765
    40
        let
wenzelm@60765
    41
          val (msg, queue') = Queue.dequeue queue;
wenzelm@60765
    42
          val input' =
wenzelm@60765
    43
            if Queue.is_empty queue' then Symtab.delete_safe id input
wenzelm@60765
    44
            else Symtab.update (id, queue') input;
wenzelm@60765
    45
        in SOME (msg, make_state (threads, input')) end));
wenzelm@60765
    46
wenzelm@60765
    47
wenzelm@60765
    48
(* thread data *)
wenzelm@60765
    49
wenzelm@60765
    50
local val tag = Universal.tag () : ML_Debugger.state list Universal.tag in
wenzelm@60765
    51
wenzelm@60765
    52
fun get_data () = the_default [] (Thread.getLocal tag);
wenzelm@60765
    53
fun setmp_data data f x = setmp_thread_data tag (get_data ()) data f x;
wenzelm@60765
    54
wenzelm@60749
    55
end;
wenzelm@60749
    56
wenzelm@60765
    57
val debugging = not o null o get_data;
wenzelm@60765
    58
fun with_debugging e = setmp_data (ML_Debugger.state (Thread.self ())) e ();
wenzelm@60765
    59
wenzelm@60765
    60
wenzelm@60765
    61
(* protocol messages *)
wenzelm@60749
    62
wenzelm@60749
    63
val _ = Session.protocol_handler "isabelle.Debugger$Handler";
wenzelm@60749
    64
wenzelm@60765
    65
wenzelm@60765
    66
(* main entry point *)
wenzelm@60765
    67
wenzelm@60765
    68
fun debug_loop id =
wenzelm@60765
    69
  (case get_input id of
wenzelm@60765
    70
    ["continue"] => ()
wenzelm@60765
    71
  | bad =>
wenzelm@60765
    72
     (Output.system_message
wenzelm@60765
    73
        ("Debugger: bad input " ^ ML_Syntax.print_list ML_Syntax.print_string bad);
wenzelm@60765
    74
      debug_loop id));
wenzelm@60765
    75
wenzelm@60765
    76
fun debugger cond =
wenzelm@60765
    77
  if debugging () orelse not (cond ()) orelse
wenzelm@60765
    78
    not (Options.default_bool @{system_option ML_debugger_active})
wenzelm@60765
    79
  then ()
wenzelm@60765
    80
  else
wenzelm@60765
    81
    with_debugging (fn () =>
wenzelm@60765
    82
      (case Simple_Thread.identification () of
wenzelm@60765
    83
        NONE => ()
wenzelm@60765
    84
      | SOME id => debug_loop id));
wenzelm@60765
    85
wenzelm@60765
    86
fun init () =
wenzelm@60765
    87
  ML_Debugger.on_breakpoint
wenzelm@60765
    88
    (SOME (fn (_, b) =>
wenzelm@60765
    89
      debugger (fn () => ! b orelse Options.default_bool @{system_option ML_debugger_stepping})));
wenzelm@60765
    90
wenzelm@60765
    91
wenzelm@60765
    92
(* protocol commands *)
wenzelm@60765
    93
wenzelm@60765
    94
val _ =
wenzelm@60765
    95
  Isabelle_Process.protocol_command "Debugger.init"
wenzelm@60765
    96
    (fn [] => init ());
wenzelm@60765
    97
wenzelm@60765
    98
val _ =
wenzelm@60765
    99
  Isabelle_Process.protocol_command "Debugger.cancel"
wenzelm@60765
   100
    (fn [id] => cancel id);
wenzelm@60765
   101
wenzelm@60765
   102
val _ =
wenzelm@60765
   103
  Isabelle_Process.protocol_command "Debugger.input"
wenzelm@60765
   104
    (fn id :: msg => input id msg);
wenzelm@60765
   105
wenzelm@60749
   106
end;