skeleton for interactive debugger;
authorwenzelm
Fri Jul 17 21:40:47 2015 +0200 (2015-07-17)
changeset 60749f727b99faaf7
parent 60748 6d718fda8215
child 60750 7694aa52ad56
skeleton for interactive debugger;
src/Pure/PIDE/session.scala
src/Pure/Pure.thy
src/Pure/Tools/debugger.ML
src/Pure/Tools/debugger.scala
src/Pure/build-jars
src/Tools/jEdit/lib/Tools/jedit
src/Tools/jEdit/src/Isabelle.props
src/Tools/jEdit/src/debugger_dockable.scala
src/Tools/jEdit/src/dockables.xml
src/Tools/jEdit/src/isabelle.scala
src/Tools/jEdit/src/jEdit.props
     1.1 --- a/src/Pure/PIDE/session.scala	Fri Jul 17 21:37:33 2015 +0200
     1.2 +++ b/src/Pure/PIDE/session.scala	Fri Jul 17 21:40:47 2015 +0200
     1.3 @@ -202,9 +202,10 @@
     1.4    val phase_changed = new Session.Outlet[Session.Phase](dispatcher)
     1.5    val syslog_messages = new Session.Outlet[Prover.Output](dispatcher)
     1.6    val raw_output_messages = new Session.Outlet[Prover.Output](dispatcher)
     1.7 -  val all_messages = new Session.Outlet[Prover.Message](dispatcher)  // potential bottle-neck
     1.8    val trace_events = new Session.Outlet[Simplifier_Trace.Event.type](dispatcher)
     1.9 +  val debugger_events = new Session.Outlet[Debugger.Event.type](dispatcher)
    1.10  
    1.11 +  val all_messages = new Session.Outlet[Prover.Message](dispatcher)  // potential bottle-neck!
    1.12  
    1.13  
    1.14    /** main protocol manager **/
     2.1 --- a/src/Pure/Pure.thy	Fri Jul 17 21:37:33 2015 +0200
     2.2 +++ b/src/Pure/Pure.thy	Fri Jul 17 21:40:47 2015 +0200
     2.3 @@ -107,6 +107,7 @@
     2.4  ML_file "Tools/find_theorems.ML"
     2.5  ML_file "Tools/find_consts.ML"
     2.6  ML_file "Tools/simplifier_trace.ML"
     2.7 +ML_file "Tools/debugger.ML"
     2.8  ML_file "Tools/named_theorems.ML"
     2.9  
    2.10  
     3.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.2 +++ b/src/Pure/Tools/debugger.ML	Fri Jul 17 21:40:47 2015 +0200
     3.3 @@ -0,0 +1,16 @@
     3.4 +(*  Title:      Pure/Tools/debugger.ML
     3.5 +    Author:     Makarius
     3.6 +
     3.7 +Interactive debugger for Isabelle/ML.
     3.8 +*)
     3.9 +
    3.10 +signature DEBUGGER =
    3.11 +sig
    3.12 +end;
    3.13 +
    3.14 +structure Debugger: DEBUGGER =
    3.15 +struct
    3.16 +
    3.17 +val _ = Session.protocol_handler "isabelle.Debugger$Handler";
    3.18 +
    3.19 +end;
     4.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     4.2 +++ b/src/Pure/Tools/debugger.scala	Fri Jul 17 21:40:47 2015 +0200
     4.3 @@ -0,0 +1,44 @@
     4.4 +/*  Title:      Pure/Tools/debugger.scala
     4.5 +    Author:     Makarius
     4.6 +
     4.7 +Interactive debugger for Isabelle/ML.
     4.8 +*/
     4.9 +
    4.10 +package isabelle
    4.11 +
    4.12 +
    4.13 +object Debugger
    4.14 +{
    4.15 +  /* GUI interaction */
    4.16 +
    4.17 +  case object Event
    4.18 +
    4.19 +
    4.20 +  /* manager thread */
    4.21 +
    4.22 +  private lazy val manager: Consumer_Thread[Any] =
    4.23 +    Consumer_Thread.fork[Any]("Debugger.manager", daemon = true)(
    4.24 +      consume = (arg: Any) =>
    4.25 +      {
    4.26 +        // FIXME
    4.27 +        true
    4.28 +      },
    4.29 +      finish = () =>
    4.30 +      {
    4.31 +        // FIXME
    4.32 +      }
    4.33 +    )
    4.34 +
    4.35 +
    4.36 +  /* protocol handler */
    4.37 +
    4.38 +  class Handler extends Session.Protocol_Handler
    4.39 +  {
    4.40 +    override def stop(prover: Prover)
    4.41 +    {
    4.42 +      manager.shutdown()
    4.43 +    }
    4.44 +
    4.45 +    val functions = Map.empty[String, (Prover, Prover.Protocol_Output) => Boolean]  // FIXME
    4.46 +  }
    4.47 +}
     5.1 --- a/src/Pure/build-jars	Fri Jul 17 21:37:33 2015 +0200
     5.2 +++ b/src/Pure/build-jars	Fri Jul 17 21:40:47 2015 +0200
     5.3 @@ -94,6 +94,7 @@
     5.4    Tools/build_doc.scala
     5.5    Tools/check_keywords.scala
     5.6    Tools/check_source.scala
     5.7 +  Tools/debugger.scala
     5.8    Tools/doc.scala
     5.9    Tools/main.scala
    5.10    Tools/ml_statistics.scala
     6.1 --- a/src/Tools/jEdit/lib/Tools/jedit	Fri Jul 17 21:37:33 2015 +0200
     6.2 +++ b/src/Tools/jEdit/lib/Tools/jedit	Fri Jul 17 21:40:47 2015 +0200
     6.3 @@ -12,6 +12,7 @@
     6.4    "src/bibtex_jedit.scala"
     6.5    "src/completion_popup.scala"
     6.6    "src/context_menu.scala"
     6.7 +  "src/debugger_dockable.scala"
     6.8    "src/dockable.scala"
     6.9    "src/document_model.scala"
    6.10    "src/document_view.scala"
     7.1 --- a/src/Tools/jEdit/src/Isabelle.props	Fri Jul 17 21:37:33 2015 +0200
     7.2 +++ b/src/Tools/jEdit/src/Isabelle.props	Fri Jul 17 21:40:47 2015 +0200
     7.3 @@ -30,6 +30,7 @@
     7.4  #menu actions and dockables
     7.5  plugin.isabelle.jedit.Plugin.menu.label=Isabelle
     7.6  plugin.isabelle.jedit.Plugin.menu= \
     7.7 +  isabelle-debugger \
     7.8    isabelle-documentation \
     7.9    isabelle-monitor \
    7.10    isabelle-output \
    7.11 @@ -42,6 +43,8 @@
    7.12    isabelle-syslog \
    7.13    isabelle-theories \
    7.14    isabelle-timing
    7.15 +isabelle-debugger.label=Debugger panel
    7.16 +isabelle-debugger.title=Debugger
    7.17  isabelle-documentation.label=Documentation panel
    7.18  isabelle-documentation.title=Documentation
    7.19  isabelle-graphview.label=Graphview panel
     8.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     8.2 +++ b/src/Tools/jEdit/src/debugger_dockable.scala	Fri Jul 17 21:40:47 2015 +0200
     8.3 @@ -0,0 +1,104 @@
     8.4 +/*  Title:      Tools/jEdit/src/debugger_dockable.scala
     8.5 +    Author:     Makarius
     8.6 +
     8.7 +Dockable window for Isabelle/ML debugger.
     8.8 +*/
     8.9 +
    8.10 +package isabelle.jedit
    8.11 +
    8.12 +
    8.13 +import isabelle._
    8.14 +
    8.15 +import java.awt.BorderLayout
    8.16 +import java.awt.event.{ComponentEvent, ComponentAdapter}
    8.17 +
    8.18 +import org.gjt.sp.jedit.View
    8.19 +
    8.20 +
    8.21 +class Debugger_Dockable(view: View, position: String) extends Dockable(view, position)
    8.22 +{
    8.23 +  GUI_Thread.require {}
    8.24 +
    8.25 +
    8.26 +  /* component state -- owned by GUI thread */
    8.27 +
    8.28 +  private var current_snapshot = Document.Snapshot.init
    8.29 +  private var current_output: List[XML.Tree] = Nil
    8.30 +
    8.31 +
    8.32 +  /* pretty text area */
    8.33 +
    8.34 +  val pretty_text_area = new Pretty_Text_Area(view)
    8.35 +  set_content(pretty_text_area)
    8.36 +
    8.37 +  override def detach_operation = pretty_text_area.detach_operation
    8.38 +
    8.39 +
    8.40 +  private val zoom = new Font_Info.Zoom_Box { def changed = handle_resize() }
    8.41 +
    8.42 +  private def handle_resize()
    8.43 +  {
    8.44 +    GUI_Thread.require {}
    8.45 +
    8.46 +    pretty_text_area.resize(
    8.47 +      Font_Info.main(PIDE.options.real("jedit_font_scale") * zoom.factor / 100))
    8.48 +  }
    8.49 +
    8.50 +  private def handle_update()
    8.51 +  {
    8.52 +    GUI_Thread.require {}
    8.53 +
    8.54 +    val new_snapshot = PIDE.editor.current_node_snapshot(view).getOrElse(current_snapshot)
    8.55 +    val new_output = List(XML.Text("FIXME"))
    8.56 +
    8.57 +    if (new_output != current_output)
    8.58 +      pretty_text_area.update(new_snapshot, Command.Results.empty, Pretty.separate(new_output))
    8.59 +
    8.60 +    current_snapshot = new_snapshot
    8.61 +    current_output = new_output
    8.62 +  }
    8.63 +
    8.64 +
    8.65 +  /* main */
    8.66 +
    8.67 +  private val main =
    8.68 +    Session.Consumer[Any](getClass.getName) {
    8.69 +      case _: Session.Global_Options =>
    8.70 +        GUI_Thread.later { handle_resize() }
    8.71 +
    8.72 +      case Debugger.Event =>
    8.73 +        GUI_Thread.later { handle_update() }
    8.74 +    }
    8.75 +
    8.76 +  override def init()
    8.77 +  {
    8.78 +    PIDE.session.global_options += main
    8.79 +    PIDE.session.debugger_events += main
    8.80 +    handle_update()
    8.81 +  }
    8.82 +
    8.83 +  override def exit()
    8.84 +  {
    8.85 +    PIDE.session.global_options -= main
    8.86 +    PIDE.session.debugger_events -= main
    8.87 +    delay_resize.revoke()
    8.88 +  }
    8.89 +
    8.90 +
    8.91 +  /* resize */
    8.92 +
    8.93 +  private val delay_resize =
    8.94 +    GUI_Thread.delay_first(PIDE.options.seconds("editor_update_delay")) { handle_resize() }
    8.95 +
    8.96 +  addComponentListener(new ComponentAdapter {
    8.97 +    override def componentResized(e: ComponentEvent) { delay_resize.invoke() }
    8.98 +  })
    8.99 +
   8.100 +
   8.101 +  /* controls */
   8.102 +
   8.103 +  private val controls =
   8.104 +    new Wrap_Panel(Wrap_Panel.Alignment.Right)(
   8.105 +      pretty_text_area.search_label, pretty_text_area.search_field, zoom)
   8.106 +  add(controls.peer, BorderLayout.NORTH)
   8.107 +}
     9.1 --- a/src/Tools/jEdit/src/dockables.xml	Fri Jul 17 21:37:33 2015 +0200
     9.2 +++ b/src/Tools/jEdit/src/dockables.xml	Fri Jul 17 21:40:47 2015 +0200
     9.3 @@ -2,6 +2,9 @@
     9.4  <!DOCTYPE DOCKABLES SYSTEM "dockables.dtd">
     9.5  
     9.6  <DOCKABLES>
     9.7 +	<DOCKABLE NAME="isabelle-debugger" MOVABLE="TRUE">
     9.8 +		new isabelle.jedit.Debugger_Dockable(view, position);
     9.9 +	</DOCKABLE>
    9.10  	<DOCKABLE NAME="isabelle-documentation" MOVABLE="TRUE">
    9.11  		new isabelle.jedit.Documentation_Dockable(view, position);
    9.12  	</DOCKABLE>
    10.1 --- a/src/Tools/jEdit/src/isabelle.scala	Fri Jul 17 21:37:33 2015 +0200
    10.2 +++ b/src/Tools/jEdit/src/isabelle.scala	Fri Jul 17 21:40:47 2015 +0200
    10.3 @@ -93,6 +93,12 @@
    10.4  
    10.5    private def wm(view: View): DockableWindowManager = view.getDockableWindowManager
    10.6  
    10.7 +  def debugger_dockable(view: View): Option[Debugger_Dockable] =
    10.8 +    wm(view).getDockableWindow("isabelle-debugger") match {
    10.9 +      case dockable: Debugger_Dockable => Some(dockable)
   10.10 +      case _ => None
   10.11 +    }
   10.12 +
   10.13    def documentation_dockable(view: View): Option[Documentation_Dockable] =
   10.14      wm(view).getDockableWindow("isabelle-documentation") match {
   10.15        case dockable: Documentation_Dockable => Some(dockable)
    11.1 --- a/src/Tools/jEdit/src/jEdit.props	Fri Jul 17 21:37:33 2015 +0200
    11.2 +++ b/src/Tools/jEdit/src/jEdit.props	Fri Jul 17 21:40:47 2015 +0200
    11.3 @@ -185,6 +185,7 @@
    11.4  home.shortcut=
    11.5  insert-newline-indent.shortcut=
    11.6  insert-newline.shortcut=ENTER
    11.7 +isabelle-debugger.dock-position=floating
    11.8  isabelle-documentation.dock-position=right
    11.9  isabelle-output.dock-position=bottom
   11.10  isabelle-output.height=174