support for ML debugger;
authorwenzelm
Tue Jul 21 19:04:36 2015 +0200 (2015-07-21)
changeset 60765e43e71a75838
parent 60764 b610ba36e02c
child 60766 76560ce8dead
support for ML debugger;
etc/options
src/Pure/Tools/debugger.ML
src/Pure/Tools/debugger.scala
     1.1 --- a/etc/options	Tue Jul 21 14:12:45 2015 +0200
     1.2 +++ b/etc/options	Tue Jul 21 19:04:36 2015 +0200
     1.3 @@ -104,6 +104,12 @@
     1.4  public option ML_debugger : bool = false
     1.5    -- "ML debugger instrumentation for newly compiled code"
     1.6  
     1.7 +public option ML_debugger_active : bool = false
     1.8 +  -- "ML debugger active at run-time, for code compiled with debugger instrumentation"
     1.9 +
    1.10 +public option ML_debugger_stepping : bool = false
    1.11 +  -- "ML debugger in single-step mode"
    1.12 +
    1.13  public option ML_statistics : bool = true
    1.14    -- "ML runtime system statistics"
    1.15  
     2.1 --- a/src/Pure/Tools/debugger.ML	Tue Jul 21 14:12:45 2015 +0200
     2.2 +++ b/src/Pure/Tools/debugger.ML	Tue Jul 21 19:04:36 2015 +0200
     2.3 @@ -4,13 +4,103 @@
     2.4  Interactive debugger for Isabelle/ML.
     2.5  *)
     2.6  
     2.7 -signature DEBUGGER =
     2.8 -sig
     2.9 +structure Debugger: sig end =
    2.10 +struct
    2.11 +
    2.12 +(* global state *)
    2.13 +
    2.14 +datatype state =
    2.15 +  State of {
    2.16 +    threads: Thread.thread Symtab.table,  (*thread identification ~> thread*)
    2.17 +    input: string list Queue.T Symtab.table  (*thread identification ~> input queue*)
    2.18 +  };
    2.19 +
    2.20 +fun make_state (threads, input) = State {threads = threads, input = input};
    2.21 +val init_state = make_state (Symtab.empty, Symtab.empty);
    2.22 +fun map_state f (State {threads, input}) = make_state (f (threads, input));
    2.23 +
    2.24 +val global_state = Synchronized.var "Debugger.state" init_state;
    2.25 +
    2.26 +fun cancel id =
    2.27 +  Synchronized.change global_state (tap (fn State {threads, ...} =>
    2.28 +    (case Symtab.lookup threads id of
    2.29 +      NONE => ()
    2.30 +    | SOME thread => Simple_Thread.interrupt_unsynchronized thread)));
    2.31 +
    2.32 +fun input id msg =
    2.33 +  Synchronized.change global_state (map_state (fn (threads, input) =>
    2.34 +    let val input' = Symtab.map_default (id, Queue.empty) (Queue.enqueue msg) input;
    2.35 +    in (threads, input') end));
    2.36 +
    2.37 +fun get_input id =
    2.38 +  Synchronized.guarded_access global_state (fn State {threads, input} =>
    2.39 +    (case Symtab.lookup input id of
    2.40 +      NONE => NONE
    2.41 +    | SOME queue =>
    2.42 +        let
    2.43 +          val (msg, queue') = Queue.dequeue queue;
    2.44 +          val input' =
    2.45 +            if Queue.is_empty queue' then Symtab.delete_safe id input
    2.46 +            else Symtab.update (id, queue') input;
    2.47 +        in SOME (msg, make_state (threads, input')) end));
    2.48 +
    2.49 +
    2.50 +(* thread data *)
    2.51 +
    2.52 +local val tag = Universal.tag () : ML_Debugger.state list Universal.tag in
    2.53 +
    2.54 +fun get_data () = the_default [] (Thread.getLocal tag);
    2.55 +fun setmp_data data f x = setmp_thread_data tag (get_data ()) data f x;
    2.56 +
    2.57  end;
    2.58  
    2.59 -structure Debugger: DEBUGGER =
    2.60 -struct
    2.61 +val debugging = not o null o get_data;
    2.62 +fun with_debugging e = setmp_data (ML_Debugger.state (Thread.self ())) e ();
    2.63 +
    2.64 +
    2.65 +(* protocol messages *)
    2.66  
    2.67  val _ = Session.protocol_handler "isabelle.Debugger$Handler";
    2.68  
    2.69 +
    2.70 +(* main entry point *)
    2.71 +
    2.72 +fun debug_loop id =
    2.73 +  (case get_input id of
    2.74 +    ["continue"] => ()
    2.75 +  | bad =>
    2.76 +     (Output.system_message
    2.77 +        ("Debugger: bad input " ^ ML_Syntax.print_list ML_Syntax.print_string bad);
    2.78 +      debug_loop id));
    2.79 +
    2.80 +fun debugger cond =
    2.81 +  if debugging () orelse not (cond ()) orelse
    2.82 +    not (Options.default_bool @{system_option ML_debugger_active})
    2.83 +  then ()
    2.84 +  else
    2.85 +    with_debugging (fn () =>
    2.86 +      (case Simple_Thread.identification () of
    2.87 +        NONE => ()
    2.88 +      | SOME id => debug_loop id));
    2.89 +
    2.90 +fun init () =
    2.91 +  ML_Debugger.on_breakpoint
    2.92 +    (SOME (fn (_, b) =>
    2.93 +      debugger (fn () => ! b orelse Options.default_bool @{system_option ML_debugger_stepping})));
    2.94 +
    2.95 +
    2.96 +(* protocol commands *)
    2.97 +
    2.98 +val _ =
    2.99 +  Isabelle_Process.protocol_command "Debugger.init"
   2.100 +    (fn [] => init ());
   2.101 +
   2.102 +val _ =
   2.103 +  Isabelle_Process.protocol_command "Debugger.cancel"
   2.104 +    (fn [id] => cancel id);
   2.105 +
   2.106 +val _ =
   2.107 +  Isabelle_Process.protocol_command "Debugger.input"
   2.108 +    (fn id :: msg => input id msg);
   2.109 +
   2.110  end;
     3.1 --- a/src/Pure/Tools/debugger.scala	Tue Jul 21 14:12:45 2015 +0200
     3.2 +++ b/src/Pure/Tools/debugger.scala	Tue Jul 21 19:04:36 2015 +0200
     3.3 @@ -41,4 +41,16 @@
     3.4  
     3.5      val functions = Map.empty[String, (Prover, Prover.Protocol_Output) => Boolean]  // FIXME
     3.6    }
     3.7 +
     3.8 +
     3.9 +  /* protocol commands */
    3.10 +
    3.11 +  def init(session: Session): Unit =
    3.12 +    session.protocol_command("Debugger.init")
    3.13 +
    3.14 +  def cancel(session: Session, id: String): Unit =
    3.15 +    session.protocol_command("Debugger.cancel", id)
    3.16 +
    3.17 +  def input(session: Session, id: String, msg: String*): Unit =
    3.18 +    session.protocol_command("Debugger.input", (id :: msg.toList):_*)
    3.19  }