# HG changeset patch # User wenzelm # Date 1437162047 -7200 # Node ID f727b99faaf7c18972be001fdc86439f282988b7 # Parent 6d718fda8215d63cfecaec7dc9756f3de42cde23 skeleton for interactive debugger; diff -r 6d718fda8215 -r f727b99faaf7 src/Pure/PIDE/session.scala --- 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 **/ diff -r 6d718fda8215 -r f727b99faaf7 src/Pure/Pure.thy --- 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" diff -r 6d718fda8215 -r f727b99faaf7 src/Pure/Tools/debugger.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; diff -r 6d718fda8215 -r f727b99faaf7 src/Pure/Tools/debugger.scala --- /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 + } +} diff -r 6d718fda8215 -r f727b99faaf7 src/Pure/build-jars --- 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 diff -r 6d718fda8215 -r f727b99faaf7 src/Tools/jEdit/lib/Tools/jedit --- 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" diff -r 6d718fda8215 -r f727b99faaf7 src/Tools/jEdit/src/Isabelle.props --- 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 diff -r 6d718fda8215 -r f727b99faaf7 src/Tools/jEdit/src/debugger_dockable.scala --- /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) +} diff -r 6d718fda8215 -r f727b99faaf7 src/Tools/jEdit/src/dockables.xml --- 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 @@ + + new isabelle.jedit.Debugger_Dockable(view, position); + new isabelle.jedit.Documentation_Dockable(view, position); diff -r 6d718fda8215 -r f727b99faaf7 src/Tools/jEdit/src/isabelle.scala --- 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) diff -r 6d718fda8215 -r f727b99faaf7 src/Tools/jEdit/src/jEdit.props --- 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