--- a/src/Pure/PIDE/session.scala Fri Jul 17 21:37:33 2015 +0200
+++ b/src/Pure/PIDE/session.scala Fri Jul 17 21:40:47 2015 +0200
@@ -202,9 +202,10 @@
val phase_changed = new Session.Outlet[Session.Phase](dispatcher)
val syslog_messages = new Session.Outlet[Prover.Output](dispatcher)
val raw_output_messages = new Session.Outlet[Prover.Output](dispatcher)
- val all_messages = new Session.Outlet[Prover.Message](dispatcher) // potential bottle-neck
val trace_events = new Session.Outlet[Simplifier_Trace.Event.type](dispatcher)
+ val debugger_events = new Session.Outlet[Debugger.Event.type](dispatcher)
+ val all_messages = new Session.Outlet[Prover.Message](dispatcher) // potential bottle-neck!
/** main protocol manager **/
--- a/src/Pure/Pure.thy Fri Jul 17 21:37:33 2015 +0200
+++ b/src/Pure/Pure.thy Fri Jul 17 21:40:47 2015 +0200
@@ -107,6 +107,7 @@
ML_file "Tools/find_theorems.ML"
ML_file "Tools/find_consts.ML"
ML_file "Tools/simplifier_trace.ML"
+ML_file "Tools/debugger.ML"
ML_file "Tools/named_theorems.ML"
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/Tools/debugger.ML Fri Jul 17 21:40:47 2015 +0200
@@ -0,0 +1,16 @@
+(* Title: Pure/Tools/debugger.ML
+ Author: Makarius
+
+Interactive debugger for Isabelle/ML.
+*)
+
+signature DEBUGGER =
+sig
+end;
+
+structure Debugger: DEBUGGER =
+struct
+
+val _ = Session.protocol_handler "isabelle.Debugger$Handler";
+
+end;
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/Tools/debugger.scala Fri Jul 17 21:40:47 2015 +0200
@@ -0,0 +1,44 @@
+/* Title: Pure/Tools/debugger.scala
+ Author: Makarius
+
+Interactive debugger for Isabelle/ML.
+*/
+
+package isabelle
+
+
+object Debugger
+{
+ /* GUI interaction */
+
+ case object Event
+
+
+ /* manager thread */
+
+ private lazy val manager: Consumer_Thread[Any] =
+ Consumer_Thread.fork[Any]("Debugger.manager", daemon = true)(
+ consume = (arg: Any) =>
+ {
+ // FIXME
+ true
+ },
+ finish = () =>
+ {
+ // FIXME
+ }
+ )
+
+
+ /* protocol handler */
+
+ class Handler extends Session.Protocol_Handler
+ {
+ override def stop(prover: Prover)
+ {
+ manager.shutdown()
+ }
+
+ val functions = Map.empty[String, (Prover, Prover.Protocol_Output) => Boolean] // FIXME
+ }
+}
--- a/src/Pure/build-jars Fri Jul 17 21:37:33 2015 +0200
+++ b/src/Pure/build-jars Fri Jul 17 21:40:47 2015 +0200
@@ -94,6 +94,7 @@
Tools/build_doc.scala
Tools/check_keywords.scala
Tools/check_source.scala
+ Tools/debugger.scala
Tools/doc.scala
Tools/main.scala
Tools/ml_statistics.scala
--- a/src/Tools/jEdit/lib/Tools/jedit Fri Jul 17 21:37:33 2015 +0200
+++ b/src/Tools/jEdit/lib/Tools/jedit Fri Jul 17 21:40:47 2015 +0200
@@ -12,6 +12,7 @@
"src/bibtex_jedit.scala"
"src/completion_popup.scala"
"src/context_menu.scala"
+ "src/debugger_dockable.scala"
"src/dockable.scala"
"src/document_model.scala"
"src/document_view.scala"
--- a/src/Tools/jEdit/src/Isabelle.props Fri Jul 17 21:37:33 2015 +0200
+++ b/src/Tools/jEdit/src/Isabelle.props Fri Jul 17 21:40:47 2015 +0200
@@ -30,6 +30,7 @@
#menu actions and dockables
plugin.isabelle.jedit.Plugin.menu.label=Isabelle
plugin.isabelle.jedit.Plugin.menu= \
+ isabelle-debugger \
isabelle-documentation \
isabelle-monitor \
isabelle-output \
@@ -42,6 +43,8 @@
isabelle-syslog \
isabelle-theories \
isabelle-timing
+isabelle-debugger.label=Debugger panel
+isabelle-debugger.title=Debugger
isabelle-documentation.label=Documentation panel
isabelle-documentation.title=Documentation
isabelle-graphview.label=Graphview panel
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/jEdit/src/debugger_dockable.scala Fri Jul 17 21:40:47 2015 +0200
@@ -0,0 +1,104 @@
+/* Title: Tools/jEdit/src/debugger_dockable.scala
+ Author: Makarius
+
+Dockable window for Isabelle/ML debugger.
+*/
+
+package isabelle.jedit
+
+
+import isabelle._
+
+import java.awt.BorderLayout
+import java.awt.event.{ComponentEvent, ComponentAdapter}
+
+import org.gjt.sp.jedit.View
+
+
+class Debugger_Dockable(view: View, position: String) extends Dockable(view, position)
+{
+ GUI_Thread.require {}
+
+
+ /* component state -- owned by GUI thread */
+
+ private var current_snapshot = Document.Snapshot.init
+ private var current_output: List[XML.Tree] = Nil
+
+
+ /* pretty text area */
+
+ val pretty_text_area = new Pretty_Text_Area(view)
+ set_content(pretty_text_area)
+
+ 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 {}
+
+ pretty_text_area.resize(
+ Font_Info.main(PIDE.options.real("jedit_font_scale") * zoom.factor / 100))
+ }
+
+ private def handle_update()
+ {
+ GUI_Thread.require {}
+
+ val new_snapshot = PIDE.editor.current_node_snapshot(view).getOrElse(current_snapshot)
+ val new_output = List(XML.Text("FIXME"))
+
+ if (new_output != current_output)
+ pretty_text_area.update(new_snapshot, Command.Results.empty, Pretty.separate(new_output))
+
+ current_snapshot = new_snapshot
+ current_output = new_output
+ }
+
+
+ /* main */
+
+ private val main =
+ Session.Consumer[Any](getClass.getName) {
+ case _: Session.Global_Options =>
+ GUI_Thread.later { handle_resize() }
+
+ case Debugger.Event =>
+ GUI_Thread.later { handle_update() }
+ }
+
+ override def init()
+ {
+ PIDE.session.global_options += main
+ PIDE.session.debugger_events += main
+ handle_update()
+ }
+
+ override def exit()
+ {
+ PIDE.session.global_options -= main
+ PIDE.session.debugger_events -= main
+ delay_resize.revoke()
+ }
+
+
+ /* resize */
+
+ private val delay_resize =
+ GUI_Thread.delay_first(PIDE.options.seconds("editor_update_delay")) { handle_resize() }
+
+ addComponentListener(new ComponentAdapter {
+ override def componentResized(e: ComponentEvent) { delay_resize.invoke() }
+ })
+
+
+ /* controls */
+
+ private val controls =
+ new Wrap_Panel(Wrap_Panel.Alignment.Right)(
+ pretty_text_area.search_label, pretty_text_area.search_field, zoom)
+ add(controls.peer, BorderLayout.NORTH)
+}
--- a/src/Tools/jEdit/src/dockables.xml Fri Jul 17 21:37:33 2015 +0200
+++ b/src/Tools/jEdit/src/dockables.xml Fri Jul 17 21:40:47 2015 +0200
@@ -2,6 +2,9 @@
<!DOCTYPE DOCKABLES SYSTEM "dockables.dtd">
<DOCKABLES>
+ <DOCKABLE NAME="isabelle-debugger" MOVABLE="TRUE">
+ new isabelle.jedit.Debugger_Dockable(view, position);
+ </DOCKABLE>
<DOCKABLE NAME="isabelle-documentation" MOVABLE="TRUE">
new isabelle.jedit.Documentation_Dockable(view, position);
</DOCKABLE>
--- a/src/Tools/jEdit/src/isabelle.scala Fri Jul 17 21:37:33 2015 +0200
+++ b/src/Tools/jEdit/src/isabelle.scala Fri Jul 17 21:40:47 2015 +0200
@@ -93,6 +93,12 @@
private def wm(view: View): DockableWindowManager = view.getDockableWindowManager
+ def debugger_dockable(view: View): Option[Debugger_Dockable] =
+ wm(view).getDockableWindow("isabelle-debugger") match {
+ case dockable: Debugger_Dockable => Some(dockable)
+ case _ => None
+ }
+
def documentation_dockable(view: View): Option[Documentation_Dockable] =
wm(view).getDockableWindow("isabelle-documentation") match {
case dockable: Documentation_Dockable => Some(dockable)
--- a/src/Tools/jEdit/src/jEdit.props Fri Jul 17 21:37:33 2015 +0200
+++ b/src/Tools/jEdit/src/jEdit.props Fri Jul 17 21:40:47 2015 +0200
@@ -185,6 +185,7 @@
home.shortcut=
insert-newline-indent.shortcut=
insert-newline.shortcut=ENTER
+isabelle-debugger.dock-position=floating
isabelle-documentation.dock-position=right
isabelle-output.dock-position=bottom
isabelle-output.height=174