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