separate channel for debugger output;
authorwenzelm
Wed Jul 29 13:34:04 2015 +0200 (2015-07-29)
changeset 60830f56e189350b2
parent 60829 4b16b778ce0d
child 60831 5b99a334fd4c
separate channel for debugger output;
clarified thread name;
src/Pure/Concurrent/simple_thread.ML
src/Pure/PIDE/markup.ML
src/Pure/PIDE/markup.scala
src/Pure/Tools/debugger.ML
src/Pure/Tools/debugger.scala
     1.1 --- a/src/Pure/Concurrent/simple_thread.ML	Wed Jul 29 11:41:26 2015 +0200
     1.2 +++ b/src/Pure/Concurrent/simple_thread.ML	Wed Jul 29 13:34:04 2015 +0200
     1.3 @@ -7,7 +7,8 @@
     1.4  signature SIMPLE_THREAD =
     1.5  sig
     1.6    val is_self: Thread.thread -> bool
     1.7 -  val name: unit -> string option
     1.8 +  val get_name: unit -> string option
     1.9 +  val the_name: unit -> string
    1.10    type params = {name: string, stack_limit: int option, interrupts: bool}
    1.11    val attributes: params -> Thread.threadAttribute list
    1.12    val fork: params -> (unit -> unit) -> Thread.thread
    1.13 @@ -30,8 +31,15 @@
    1.14    val count = Counter.make ();
    1.15  in
    1.16  
    1.17 -fun name () = Thread.getLocal tag;
    1.18 -fun set_name base = Thread.setLocal (tag, base ^ "/" ^ string_of_int (count ()));
    1.19 +fun get_name () = Thread.getLocal tag;
    1.20 +
    1.21 +fun the_name () =
    1.22 +  (case get_name () of
    1.23 +    NONE => raise Fail "Unknown thread name"
    1.24 +  | SOME name => name);
    1.25 +
    1.26 +fun set_name base =
    1.27 +  Thread.setLocal (tag, base ^ "/" ^ string_of_int (count ()));
    1.28  
    1.29  end;
    1.30  
     2.1 --- a/src/Pure/PIDE/markup.ML	Wed Jul 29 11:41:26 2015 +0200
     2.2 +++ b/src/Pure/PIDE/markup.ML	Wed Jul 29 13:34:04 2015 +0200
     2.3 @@ -191,6 +191,7 @@
     2.4    val build_theories_result: string -> Properties.T
     2.5    val print_operationsN: string
     2.6    val print_operations: Properties.T
     2.7 +  val debugger_output: string -> serial -> Properties.T
     2.8    val simp_trace_panelN: string
     2.9    val simp_trace_logN: string
    2.10    val simp_trace_stepN: string
    2.11 @@ -611,6 +612,12 @@
    2.12  val print_operations = [(functionN, print_operationsN)];
    2.13  
    2.14  
    2.15 +(* debugger *)
    2.16 +
    2.17 +fun debugger_output name i =
    2.18 +  [(functionN, "debugger_output"), (nameN, name), (serialN, print_int i)];
    2.19 +
    2.20 +
    2.21  (* simplifier trace *)
    2.22  
    2.23  val simp_trace_panelN = "simp_trace_panel";
     3.1 --- a/src/Pure/PIDE/markup.scala	Wed Jul 29 11:41:26 2015 +0200
     3.2 +++ b/src/Pure/PIDE/markup.scala	Wed Jul 29 13:34:04 2015 +0200
     3.3 @@ -493,6 +493,20 @@
     3.4    val PRINT_OPERATIONS = "print_operations"
     3.5  
     3.6  
     3.7 +  /* debugger output */
     3.8 +
     3.9 +  val DEBUGGER_OUTPUT = "debugger_output"
    3.10 +  object Debugger_Output
    3.11 +  {
    3.12 +    def unapply(props: Properties.T): Option[(String, Long)] =
    3.13 +      props match {
    3.14 +        case List((FUNCTION, DEBUGGER_OUTPUT), (NAME, name), (SERIAL, Properties.Value.Long(i))) =>
    3.15 +          Some((name, i))
    3.16 +        case _ => None
    3.17 +      }
    3.18 +  }
    3.19 +
    3.20 +
    3.21    /* simplifier trace */
    3.22  
    3.23    val SIMP_TRACE_PANEL = "simp_trace_panel"
     4.1 --- a/src/Pure/Tools/debugger.ML	Wed Jul 29 11:41:26 2015 +0200
     4.2 +++ b/src/Pure/Tools/debugger.ML	Wed Jul 29 13:34:04 2015 +0200
     4.3 @@ -4,9 +4,21 @@
     4.4  Interactive debugger for Isabelle/ML.
     4.5  *)
     4.6  
     4.7 -structure Debugger: sig end =
     4.8 +signature DEBUGGER =
     4.9 +sig
    4.10 +  val output: string -> unit
    4.11 +end;
    4.12 +
    4.13 +structure Debugger: DEBUGGER =
    4.14  struct
    4.15  
    4.16 +(* messages *)
    4.17 +
    4.18 +fun output msg =
    4.19 +  Output.protocol_message
    4.20 +    (Markup.debugger_output (Simple_Thread.the_name ()) (serial ())) [msg];
    4.21 +
    4.22 +
    4.23  (* global state *)
    4.24  
    4.25  datatype state =
    4.26 @@ -79,7 +91,7 @@
    4.27    then ()
    4.28    else
    4.29      with_debugging (fn () =>
    4.30 -      (case Simple_Thread.name () of
    4.31 +      (case Simple_Thread.get_name () of
    4.32          NONE => ()
    4.33        | SOME name => debug_loop name));
    4.34  
     5.1 --- a/src/Pure/Tools/debugger.scala	Wed Jul 29 11:41:26 2015 +0200
     5.2 +++ b/src/Pure/Tools/debugger.scala	Wed Jul 29 13:34:04 2015 +0200
     5.3 @@ -34,12 +34,24 @@
     5.4  
     5.5    class Handler extends Session.Protocol_Handler
     5.6    {
     5.7 +    private def debugger_output(prover: Prover, msg: Prover.Protocol_Output): Boolean =
     5.8 +    {
     5.9 +      msg.properties match {
    5.10 +        case Markup.Debugger_Output(name, serial) =>
    5.11 +          // FIXME
    5.12 +          Output.writeln("debugger_output " + name + " " + serial + "\n" + msg.text)
    5.13 +          true
    5.14 +        case _ => false
    5.15 +      }
    5.16 +    }
    5.17 +
    5.18      override def stop(prover: Prover)
    5.19      {
    5.20        manager.shutdown()
    5.21      }
    5.22  
    5.23 -    val functions = Map.empty[String, (Prover, Prover.Protocol_Output) => Boolean]  // FIXME
    5.24 +    val functions =
    5.25 +      Map(Markup.DEBUGGER_OUTPUT -> debugger_output _)
    5.26    }
    5.27  
    5.28