--- 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);
--- 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)
--- 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";
--- 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"
--- 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],
--- 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!
--- 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;
--- 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):_*)
}
--- 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)
}
--- 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()
}
}
-
--- 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() }