src/Pure/Tools/debugger.ML
changeset 60765 e43e71a75838
parent 60749 f727b99faaf7
child 60829 4b16b778ce0d
     1.1 --- a/src/Pure/Tools/debugger.ML	Tue Jul 21 14:12:45 2015 +0200
     1.2 +++ b/src/Pure/Tools/debugger.ML	Tue Jul 21 19:04:36 2015 +0200
     1.3 @@ -4,13 +4,103 @@
     1.4  Interactive debugger for Isabelle/ML.
     1.5  *)
     1.6  
     1.7 -signature DEBUGGER =
     1.8 -sig
     1.9 +structure Debugger: sig end =
    1.10 +struct
    1.11 +
    1.12 +(* global state *)
    1.13 +
    1.14 +datatype state =
    1.15 +  State of {
    1.16 +    threads: Thread.thread Symtab.table,  (*thread identification ~> thread*)
    1.17 +    input: string list Queue.T Symtab.table  (*thread identification ~> input queue*)
    1.18 +  };
    1.19 +
    1.20 +fun make_state (threads, input) = State {threads = threads, input = input};
    1.21 +val init_state = make_state (Symtab.empty, Symtab.empty);
    1.22 +fun map_state f (State {threads, input}) = make_state (f (threads, input));
    1.23 +
    1.24 +val global_state = Synchronized.var "Debugger.state" init_state;
    1.25 +
    1.26 +fun cancel id =
    1.27 +  Synchronized.change global_state (tap (fn State {threads, ...} =>
    1.28 +    (case Symtab.lookup threads id of
    1.29 +      NONE => ()
    1.30 +    | SOME thread => Simple_Thread.interrupt_unsynchronized thread)));
    1.31 +
    1.32 +fun input id msg =
    1.33 +  Synchronized.change global_state (map_state (fn (threads, input) =>
    1.34 +    let val input' = Symtab.map_default (id, Queue.empty) (Queue.enqueue msg) input;
    1.35 +    in (threads, input') end));
    1.36 +
    1.37 +fun get_input id =
    1.38 +  Synchronized.guarded_access global_state (fn State {threads, input} =>
    1.39 +    (case Symtab.lookup input id of
    1.40 +      NONE => NONE
    1.41 +    | SOME queue =>
    1.42 +        let
    1.43 +          val (msg, queue') = Queue.dequeue queue;
    1.44 +          val input' =
    1.45 +            if Queue.is_empty queue' then Symtab.delete_safe id input
    1.46 +            else Symtab.update (id, queue') input;
    1.47 +        in SOME (msg, make_state (threads, input')) end));
    1.48 +
    1.49 +
    1.50 +(* thread data *)
    1.51 +
    1.52 +local val tag = Universal.tag () : ML_Debugger.state list Universal.tag in
    1.53 +
    1.54 +fun get_data () = the_default [] (Thread.getLocal tag);
    1.55 +fun setmp_data data f x = setmp_thread_data tag (get_data ()) data f x;
    1.56 +
    1.57  end;
    1.58  
    1.59 -structure Debugger: DEBUGGER =
    1.60 -struct
    1.61 +val debugging = not o null o get_data;
    1.62 +fun with_debugging e = setmp_data (ML_Debugger.state (Thread.self ())) e ();
    1.63 +
    1.64 +
    1.65 +(* protocol messages *)
    1.66  
    1.67  val _ = Session.protocol_handler "isabelle.Debugger$Handler";
    1.68  
    1.69 +
    1.70 +(* main entry point *)
    1.71 +
    1.72 +fun debug_loop id =
    1.73 +  (case get_input id of
    1.74 +    ["continue"] => ()
    1.75 +  | bad =>
    1.76 +     (Output.system_message
    1.77 +        ("Debugger: bad input " ^ ML_Syntax.print_list ML_Syntax.print_string bad);
    1.78 +      debug_loop id));
    1.79 +
    1.80 +fun debugger cond =
    1.81 +  if debugging () orelse not (cond ()) orelse
    1.82 +    not (Options.default_bool @{system_option ML_debugger_active})
    1.83 +  then ()
    1.84 +  else
    1.85 +    with_debugging (fn () =>
    1.86 +      (case Simple_Thread.identification () of
    1.87 +        NONE => ()
    1.88 +      | SOME id => debug_loop id));
    1.89 +
    1.90 +fun init () =
    1.91 +  ML_Debugger.on_breakpoint
    1.92 +    (SOME (fn (_, b) =>
    1.93 +      debugger (fn () => ! b orelse Options.default_bool @{system_option ML_debugger_stepping})));
    1.94 +
    1.95 +
    1.96 +(* protocol commands *)
    1.97 +
    1.98 +val _ =
    1.99 +  Isabelle_Process.protocol_command "Debugger.init"
   1.100 +    (fn [] => init ());
   1.101 +
   1.102 +val _ =
   1.103 +  Isabelle_Process.protocol_command "Debugger.cancel"
   1.104 +    (fn [id] => cancel id);
   1.105 +
   1.106 +val _ =
   1.107 +  Isabelle_Process.protocol_command "Debugger.input"
   1.108 +    (fn id :: msg => input id msg);
   1.109 +
   1.110  end;