# HG changeset patch
# User wenzelm
# Date 1438286179 -7200
# Node ID c5db501da8e4675fde05e708e604967237f02393
# Parent  e9e272fa8daf97e1a75a1c76c33c0108d1cacff9# Parent  6512bb0b1ff40fd68dad8a9aee9e184c4d9252af
merged

diff -r e9e272fa8daf -r c5db501da8e4 src/Pure/Concurrent/simple_thread.ML
--- a/src/Pure/Concurrent/simple_thread.ML	Thu Jul 30 09:49:43 2015 +0200
+++ b/src/Pure/Concurrent/simple_thread.ML	Thu Jul 30 21:56:19 2015 +0200
@@ -7,7 +7,8 @@
 signature SIMPLE_THREAD =
 sig
   val is_self: Thread.thread -> bool
-  val identification: unit -> string option
+  val get_name: unit -> string option
+  val the_name: unit -> string
   type params = {name: string, stack_limit: int option, interrupts: bool}
   val attributes: params -> Thread.threadAttribute list
   val fork: params -> (unit -> unit) -> Thread.thread
@@ -23,17 +24,22 @@
 fun is_self thread = Thread.equal (Thread.self (), thread);
 
 
-(* identification *)
+(* unique name *)
 
 local
   val tag = Universal.tag () : string Universal.tag;
   val count = Counter.make ();
 in
 
-fun identification () = Thread.getLocal tag;
+fun get_name () = Thread.getLocal tag;
 
-fun set_identification name =
-  Thread.setLocal (tag, name ^ ":" ^ string_of_int (count ()));
+fun the_name () =
+  (case get_name () of
+    NONE => raise Fail "Unknown thread name"
+  | SOME name => name);
+
+fun set_name base =
+  Thread.setLocal (tag, base ^ "/" ^ string_of_int (count ()));
 
 end;
 
@@ -49,7 +55,7 @@
 fun fork (params: params) body =
   Thread.fork (fn () =>
     print_exception_trace General.exnMessage tracing (fn () =>
-      (set_identification (#name params); body ())
+      (set_name (#name params); body ())
         handle exn => if Exn.is_interrupt exn then () (*sic!*) else reraise exn),
     attributes params);
 
diff -r e9e272fa8daf -r c5db501da8e4 src/Pure/General/bytes.scala
--- a/src/Pure/General/bytes.scala	Thu Jul 30 09:49:43 2015 +0200
+++ b/src/Pure/General/bytes.scala	Thu Jul 30 21:56:19 2015 +0200
@@ -59,7 +59,7 @@
 final class Bytes private(
   protected val bytes: Array[Byte],
   protected val offset: Int,
-  val length: Int)
+  val length: Int) extends CharSequence
 {
   /* equality */
 
@@ -107,6 +107,19 @@
     }
 
 
+  /* CharSequence operations */
+
+  def charAt(i: Int): Char =
+    if (0 <= i && i < length) (bytes(offset + i).asInstanceOf[Int] & 0xFF).asInstanceOf[Char]
+    else throw new IndexOutOfBoundsException
+
+  def subSequence(i: Int, j: Int): Bytes =
+  {
+    if (0 <= i && i <= j && j <= length) new Bytes(bytes, offset + i, j - i)
+    else throw new IndexOutOfBoundsException
+  }
+
+
   /* write */
 
   def write(stream: OutputStream): Unit = stream.write(bytes, offset, length)
diff -r e9e272fa8daf -r c5db501da8e4 src/Pure/PIDE/markup.ML
--- a/src/Pure/PIDE/markup.ML	Thu Jul 30 09:49:43 2015 +0200
+++ b/src/Pure/PIDE/markup.ML	Thu Jul 30 21:56:19 2015 +0200
@@ -191,6 +191,7 @@
   val build_theories_result: string -> Properties.T
   val print_operationsN: string
   val print_operations: Properties.T
+  val debugger_output: string -> Properties.T
   val simp_trace_panelN: string
   val simp_trace_logN: string
   val simp_trace_stepN: string
@@ -611,6 +612,11 @@
 val print_operations = [(functionN, print_operationsN)];
 
 
+(* debugger *)
+
+fun debugger_output name = [(functionN, "debugger_output"), (nameN, name)];
+
+
 (* simplifier trace *)
 
 val simp_trace_panelN = "simp_trace_panel";
diff -r e9e272fa8daf -r c5db501da8e4 src/Pure/PIDE/markup.scala
--- a/src/Pure/PIDE/markup.scala	Thu Jul 30 09:49:43 2015 +0200
+++ b/src/Pure/PIDE/markup.scala	Thu Jul 30 21:56:19 2015 +0200
@@ -485,7 +485,7 @@
   {
     def unapply(props: Properties.T): Option[String] =
       props match {
-        case List((FUNCTION, BUILD_THEORIES_RESULT), ("id", id)) => Some(id)
+        case List((FUNCTION, BUILD_THEORIES_RESULT), (ID, id)) => Some(id)
         case _ => None
       }
   }
@@ -493,6 +493,19 @@
   val PRINT_OPERATIONS = "print_operations"
 
 
+  /* debugger output */
+
+  val DEBUGGER_OUTPUT = "debugger_output"
+  object Debugger_Output
+  {
+    def unapply(props: Properties.T): Option[String] =
+      props match {
+        case List((FUNCTION, DEBUGGER_OUTPUT), (NAME, name)) => Some(name)
+        case _ => None
+      }
+  }
+
+
   /* simplifier trace */
 
   val SIMP_TRACE_PANEL = "simp_trace_panel"
diff -r e9e272fa8daf -r c5db501da8e4 src/Pure/PIDE/resources.scala
--- a/src/Pure/PIDE/resources.scala	Thu Jul 30 09:49:43 2015 +0200
+++ b/src/Pure/PIDE/resources.scala	Thu Jul 30 21:56:19 2015 +0200
@@ -16,9 +16,10 @@
 object Resources
 {
   def thy_path(path: Path): Path = path.ext("thy")
+
+  val empty: Resources = new Resources(Set.empty, Map.empty, Outer_Syntax.empty)
 }
 
-
 class Resources(
   val loaded_theories: Set[String],
   val known_theories: Map[String, Document.Node.Name],
diff -r e9e272fa8daf -r c5db501da8e4 src/Pure/PIDE/session.scala
--- a/src/Pure/PIDE/session.scala	Thu Jul 30 09:49:43 2015 +0200
+++ b/src/Pure/PIDE/session.scala	Thu Jul 30 21:56:19 2015 +0200
@@ -203,7 +203,7 @@
   val syslog_messages = new Session.Outlet[Prover.Output](dispatcher)
   val raw_output_messages = new Session.Outlet[Prover.Output](dispatcher)
   val trace_events = new Session.Outlet[Simplifier_Trace.Event.type](dispatcher)
-  val debugger_events = new Session.Outlet[Debugger.Event.type](dispatcher)
+  val debugger_updates = new Session.Outlet[Debugger.Update](dispatcher)
 
   val all_messages = new Session.Outlet[Prover.Message](dispatcher)  // potential bottle-neck!
 
diff -r e9e272fa8daf -r c5db501da8e4 src/Pure/Tools/debugger.ML
--- a/src/Pure/Tools/debugger.ML	Thu Jul 30 09:49:43 2015 +0200
+++ b/src/Pure/Tools/debugger.ML	Thu Jul 30 21:56:19 2015 +0200
@@ -4,15 +4,34 @@
 Interactive debugger for Isabelle/ML.
 *)
 
-structure Debugger: sig end =
+signature DEBUGGER =
+sig
+  val writeln_message: string -> unit
+  val warning_message: string -> unit
+  val error_message: string -> unit
+end;
+
+structure Debugger: DEBUGGER =
 struct
 
+(* messages *)
+
+fun output_message kind msg =
+  Output.protocol_message
+    (Markup.debugger_output (Simple_Thread.the_name ()))
+    [Markup.markup (kind, Markup.serial_properties (serial ())) msg];
+
+val writeln_message = output_message Markup.writelnN;
+val warning_message = output_message Markup.warningN;
+val error_message = output_message Markup.errorN;
+
+
 (* global state *)
 
 datatype state =
   State of {
-    threads: Thread.thread Symtab.table,  (*thread identification ~> thread*)
-    input: string list Queue.T Symtab.table  (*thread identification ~> input queue*)
+    threads: Thread.thread Symtab.table,  (*thread name ~> thread*)
+    input: string list Queue.T Symtab.table  (*thread name ~> input queue*)
   };
 
 fun make_state (threads, input) = State {threads = threads, input = input};
@@ -21,27 +40,27 @@
 
 val global_state = Synchronized.var "Debugger.state" init_state;
 
-fun cancel id =
+fun cancel name =
   Synchronized.change global_state (tap (fn State {threads, ...} =>
-    (case Symtab.lookup threads id of
+    (case Symtab.lookup threads name of
       NONE => ()
     | SOME thread => Simple_Thread.interrupt_unsynchronized thread)));
 
-fun input id msg =
+fun input name msg =
   Synchronized.change global_state (map_state (fn (threads, input) =>
-    let val input' = Symtab.map_default (id, Queue.empty) (Queue.enqueue msg) input;
+    let val input' = Symtab.map_default (name, Queue.empty) (Queue.enqueue msg) input;
     in (threads, input') end));
 
-fun get_input id =
+fun get_input name =
   Synchronized.guarded_access global_state (fn State {threads, input} =>
-    (case Symtab.lookup input id of
+    (case Symtab.lookup input name of
       NONE => NONE
     | SOME queue =>
         let
           val (msg, queue') = Queue.dequeue queue;
           val input' =
-            if Queue.is_empty queue' then Symtab.delete_safe id input
-            else Symtab.update (id, queue') input;
+            if Queue.is_empty queue' then Symtab.delete_safe name input
+            else Symtab.update (name, queue') input;
         in SOME (msg, make_state (threads, input')) end));
 
 
@@ -65,13 +84,13 @@
 
 (* main entry point *)
 
-fun debug_loop id =
-  (case get_input id of
+fun debug_loop name =
+  (case get_input name of
     ["continue"] => ()
   | bad =>
      (Output.system_message
         ("Debugger: bad input " ^ ML_Syntax.print_list ML_Syntax.print_string bad);
-      debug_loop id));
+      debug_loop name));
 
 fun debugger cond =
   if debugging () orelse not (cond ()) orelse
@@ -79,9 +98,9 @@
   then ()
   else
     with_debugging (fn () =>
-      (case Simple_Thread.identification () of
+      (case Simple_Thread.get_name () of
         NONE => ()
-      | SOME id => debug_loop id));
+      | SOME name => debug_loop name));
 
 fun init () =
   ML_Debugger.on_breakpoint
@@ -97,10 +116,10 @@
 
 val _ =
   Isabelle_Process.protocol_command "Debugger.cancel"
-    (fn [id] => cancel id);
+    (fn [name] => cancel name);
 
 val _ =
   Isabelle_Process.protocol_command "Debugger.input"
-    (fn id :: msg => input id msg);
+    (fn name :: msg => input name msg);
 
 end;
diff -r e9e272fa8daf -r c5db501da8e4 src/Pure/Tools/debugger.scala
--- a/src/Pure/Tools/debugger.scala	Thu Jul 30 09:49:43 2015 +0200
+++ b/src/Pure/Tools/debugger.scala	Thu Jul 30 21:56:19 2015 +0200
@@ -9,48 +9,73 @@
 
 object Debugger
 {
-  /* GUI interaction */
-
-  case object Event
-
-
-  /* manager thread */
+  /* global state */
 
-  private lazy val manager: Consumer_Thread[Any] =
-    Consumer_Thread.fork[Any]("Debugger.manager", daemon = true)(
-      consume = (arg: Any) =>
-      {
-        // FIXME
-        true
-      },
-      finish = () =>
-      {
-        // FIXME
-      }
-    )
+  sealed case class State(
+    session: Session = new Session(Resources.empty),
+    output: Map[String, Command.Results] = Map.empty)  // thread name ~> output messages
+  {
+    def add_output(name: String, entry: Command.Results.Entry): State =
+      copy(output = output + (name -> (output.getOrElse(name, Command.Results.empty) + entry)))
+  }
+
+  private val global_state = Synchronized(State())
+  def current_state(): State = global_state.value
 
 
   /* protocol handler */
 
+  sealed case class Update(thread_names: Set[String])
+
   class Handler extends Session.Protocol_Handler
   {
-    override def stop(prover: Prover)
+    private var updated = Set.empty[String]
+    private val delay_update =
+      Simple_Thread.delay_first(current_state().session.output_delay) {
+        current_state().session.debugger_updates.post(Update(updated))
+        updated = Set.empty
+      }
+    private def update(name: String)
     {
-      manager.shutdown()
+      updated += name
+      delay_update.invoke()
     }
 
-    val functions = Map.empty[String, (Prover, Prover.Protocol_Output) => Boolean]  // FIXME
+    private def debugger_output(prover: Prover, msg: Prover.Protocol_Output): Boolean =
+    {
+      msg.properties match {
+        case Markup.Debugger_Output(thread_name) =>
+          val msg_body =
+            prover.xml_cache.body(
+              YXML.parse_body_failsafe(UTF8.decode_permissive(msg.bytes)))
+          msg_body match {
+            case List(XML.Elem(Markup(name, props @ Markup.Serial(i)), body)) =>
+              val message = XML.Elem(Markup(Markup.message(name), props), body)
+              global_state.change(_.add_output(thread_name, i -> message))
+              update(thread_name)
+              true
+            case _ => false
+          }
+        case _ => false
+      }
+    }
+
+    val functions =
+      Map(Markup.DEBUGGER_OUTPUT -> debugger_output _)
   }
 
 
   /* protocol commands */
 
-  def init(session: Session): Unit =
-    session.protocol_command("Debugger.init")
+  def init(new_session: Session)
+  {
+    global_state.change(_.copy(session = new_session))
+    current_state().session.protocol_command("Debugger.init")
+  }
 
-  def cancel(session: Session, id: String): Unit =
-    session.protocol_command("Debugger.cancel", id)
+  def cancel(name: String): Unit =
+    current_state().session.protocol_command("Debugger.cancel", name)
 
-  def input(session: Session, id: String, msg: String*): Unit =
-    session.protocol_command("Debugger.input", (id :: msg.toList):_*)
+  def input(name: String, msg: String*): Unit =
+    current_state().session.protocol_command("Debugger.input", (name :: msg.toList):_*)
 }
diff -r e9e272fa8daf -r c5db501da8e4 src/Tools/jEdit/src/debugger_dockable.scala
--- a/src/Tools/jEdit/src/debugger_dockable.scala	Thu Jul 30 09:49:43 2015 +0200
+++ b/src/Tools/jEdit/src/debugger_dockable.scala	Thu Jul 30 21:56:19 2015 +0200
@@ -10,7 +10,10 @@
 import isabelle._
 
 import java.awt.BorderLayout
-import java.awt.event.{ComponentEvent, ComponentAdapter}
+import java.awt.event.{ComponentEvent, ComponentAdapter, KeyEvent}
+
+import scala.swing.{Button, Label, Component}
+import scala.swing.event.ButtonClicked
 
 import org.gjt.sp.jedit.View
 
@@ -26,6 +29,48 @@
   private var current_output: List[XML.Tree] = Nil
 
 
+  /* common GUI components */
+
+  private val context_label = new Label("Context:") { tooltip = "Isabelle/ML context (optional)" }
+  private val context_field =
+    new Completion_Popup.History_Text_Field("isabelle-debugger-context")
+    {
+      setColumns(20)
+      setToolTipText(context_label.tooltip)
+      setFont(GUI.imitate_font(getFont, Font_Info.main_family(), 1.2))
+    }
+
+  private val expression_label = new Label("ML:") { tooltip = "Isabelle/ML expression" }
+  private val expression_field =
+    new Completion_Popup.History_Text_Field("isabelle-debugger-expression")
+    {
+      override def processKeyEvent(evt: KeyEvent)
+      {
+        if (evt.getID == KeyEvent.KEY_PRESSED && evt.getKeyCode == KeyEvent.VK_ENTER)
+          eval_expression()
+        super.processKeyEvent(evt)
+      }
+      { val max = getPreferredSize; max.width = Integer.MAX_VALUE; setMaximumSize(max) }
+      setColumns(40)
+      setToolTipText(expression_label.tooltip)
+      setFont(GUI.imitate_font(getFont, Font_Info.main_family(), 1.2))
+    }
+
+  private val eval_button = new Button("<html><b>Eval</b></html>") {
+      tooltip = "Evaluate Isabelle/ML expression within optional context"
+      reactions += { case ButtonClicked(_) => eval_expression() }
+    }
+
+  private def eval_expression()
+  {
+    // FIXME
+    Output.writeln("eval context = " + quote(context_field.getText) + " expression = " +
+      quote(expression_field.getText))
+  }
+
+  private val zoom = new Font_Info.Zoom_Box { def changed = handle_resize() }
+
+
   /* pretty text area */
 
   val pretty_text_area = new Pretty_Text_Area(view)
@@ -34,8 +79,6 @@
   override def detach_operation = pretty_text_area.detach_operation
 
 
-  private val zoom = new Font_Info.Zoom_Box { def changed = handle_resize() }
-
   private def handle_resize()
   {
     GUI_Thread.require {}
@@ -49,7 +92,9 @@
     GUI_Thread.require {}
 
     val new_snapshot = PIDE.editor.current_node_snapshot(view).getOrElse(current_snapshot)
-    val new_output = List(XML.Text("FIXME"))
+    val new_output =  // FIXME select by thread name
+      (for ((_, results) <- Debugger.current_state.output; (_, tree) <- results.iterator)
+        yield tree).toList
 
     if (new_output != current_output)
       pretty_text_area.update(new_snapshot, Command.Results.empty, Pretty.separate(new_output))
@@ -64,23 +109,25 @@
   private val main =
     Session.Consumer[Any](getClass.getName) {
       case _: Session.Global_Options =>
+        Debugger.init(PIDE.session)
         GUI_Thread.later { handle_resize() }
 
-      case Debugger.Event =>
+      case _: Debugger.Update =>
         GUI_Thread.later { handle_update() }
     }
 
   override def init()
   {
     PIDE.session.global_options += main
-    PIDE.session.debugger_events += main
+    PIDE.session.debugger_updates += main
+    Debugger.init(PIDE.session)
     handle_update()
   }
 
   override def exit()
   {
     PIDE.session.global_options -= main
-    PIDE.session.debugger_events -= main
+    PIDE.session.debugger_updates -= main
     delay_resize.revoke()
   }
 
@@ -100,6 +147,8 @@
 
   private val controls =
     new Wrap_Panel(Wrap_Panel.Alignment.Right)(
+      context_label, Component.wrap(context_field),
+      expression_label, Component.wrap(expression_field), eval_button,
       pretty_text_area.search_label, pretty_text_area.search_field, zoom)
   add(controls.peer, BorderLayout.NORTH)
 }
diff -r e9e272fa8daf -r c5db501da8e4 src/Tools/jEdit/src/jedit_resources.scala
--- a/src/Tools/jEdit/src/jedit_resources.scala	Thu Jul 30 09:49:43 2015 +0200
+++ b/src/Tools/jEdit/src/jedit_resources.scala	Thu Jul 30 21:56:19 2015 +0200
@@ -21,6 +21,12 @@
 import org.gjt.sp.jedit.bufferio.BufferIORequest
 
 
+object JEdit_Resources
+{
+  val empty: JEdit_Resources =
+    new JEdit_Resources(Set.empty, Map.empty, Outer_Syntax.empty)
+}
+
 class JEdit_Resources(
     loaded_theories: Set[String],
     known_theories: Map[String, Document.Node.Name],
@@ -119,4 +125,3 @@
     if (change.deps_changed && PIDE.options.bool("jedit_auto_load")) PIDE.deps_changed()
   }
 }
-
diff -r e9e272fa8daf -r c5db501da8e4 src/Tools/jEdit/src/plugin.scala
--- a/src/Tools/jEdit/src/plugin.scala	Thu Jul 30 09:49:43 2015 +0200
+++ b/src/Tools/jEdit/src/plugin.scala	Thu Jul 30 21:56:19 2015 +0200
@@ -36,8 +36,7 @@
   @volatile var startup_notified = false
 
   @volatile var plugin: Plugin = null
-  @volatile var session: Session =
-    new Session(new JEdit_Resources(Set.empty, Map.empty, Outer_Syntax.empty))
+  @volatile var session: Session = new Session(JEdit_Resources.empty)
 
   def options_changed() { plugin.options_changed() }
   def deps_changed() { plugin.deps_changed() }