src/Tools/jEdit/src/debugger_dockable.scala
author wenzelm
Mon Aug 10 16:05:41 2015 +0200 (2015-08-10)
changeset 60876 52edced9cce5
parent 60875 ee23c1d21ac3
child 60878 1f0d2bbcf38b
permissions -rw-r--r--
rendering for debugger/breakpoint active state;
     1 /*  Title:      Tools/jEdit/src/debugger_dockable.scala
     2     Author:     Makarius
     3 
     4 Dockable window for Isabelle/ML debugger.
     5 */
     6 
     7 package isabelle.jedit
     8 
     9 
    10 import isabelle._
    11 
    12 import java.awt.{BorderLayout, Dimension}
    13 import java.awt.event.{ComponentEvent, ComponentAdapter, KeyEvent, MouseEvent, MouseAdapter,
    14   FocusAdapter, FocusEvent}
    15 import javax.swing.{JTree, JScrollPane}
    16 import javax.swing.tree.{DefaultMutableTreeNode, DefaultTreeModel, TreeSelectionModel}
    17 import javax.swing.event.{TreeSelectionEvent, TreeSelectionListener}
    18 
    19 import scala.swing.{Button, Label, Component, SplitPane, Orientation, CheckBox}
    20 import scala.swing.event.ButtonClicked
    21 
    22 import org.gjt.sp.jedit.{jEdit, View}
    23 
    24 
    25 object Debugger_Dockable
    26 {
    27   sealed case class Thread_Entry(thread_name: String, debug_states: List[Debugger.Debug_State])
    28   {
    29     override def toString: String = thread_name
    30   }
    31 
    32   sealed case class Stack_Entry(debug_state: Debugger.Debug_State, index: Int)
    33   {
    34     override def toString: String = debug_state.function
    35   }
    36 }
    37 
    38 class Debugger_Dockable(view: View, position: String) extends Dockable(view, position)
    39 {
    40   GUI_Thread.require {}
    41 
    42 
    43   /* component state -- owned by GUI thread */
    44 
    45   private var current_snapshot = Document.Snapshot.init
    46   private var current_threads: Map[String, List[Debugger.Debug_State]] = Map.empty
    47   private var current_output: List[XML.Tree] = Nil
    48 
    49 
    50   /* pretty text area */
    51 
    52   val pretty_text_area = new Pretty_Text_Area(view)
    53 
    54   override def detach_operation = pretty_text_area.detach_operation
    55 
    56   private def handle_resize()
    57   {
    58     GUI_Thread.require {}
    59 
    60     pretty_text_area.resize(
    61       Font_Info.main(PIDE.options.real("jedit_font_scale") * zoom.factor / 100))
    62   }
    63 
    64   private def handle_update()
    65   {
    66     GUI_Thread.require {}
    67 
    68     val new_state = Debugger.current_state()
    69 
    70     val new_snapshot = PIDE.editor.current_node_snapshot(view).getOrElse(current_snapshot)
    71     val new_threads = new_state.threads
    72     val new_output =
    73     {
    74       val current_thread_selection = thread_selection()
    75       (for {
    76         (thread_name, results) <- new_state.output
    77         if current_thread_selection.isEmpty || current_thread_selection.get == thread_name
    78         (_, tree) <- results.iterator
    79       } yield tree).toList
    80     }
    81 
    82     if (new_threads != current_threads) {
    83       val thread_entries =
    84         (for ((a, b) <- new_threads.iterator)
    85           yield Debugger_Dockable.Thread_Entry(a, b)).toList.sortBy(_.thread_name)
    86       update_tree(thread_entries)
    87     }
    88 
    89     if (new_output != current_output)
    90       pretty_text_area.update(new_snapshot, Command.Results.empty, Pretty.separate(new_output))
    91 
    92     current_snapshot = new_snapshot
    93     current_threads = new_threads
    94     current_output = new_output
    95   }
    96 
    97 
    98   /* tree view */
    99 
   100   private val root = new DefaultMutableTreeNode("Threads")
   101 
   102   val tree = new JTree(root)
   103   tree.setRowHeight(0)
   104   tree.getSelectionModel.setSelectionMode(TreeSelectionModel.SINGLE_TREE_SELECTION)
   105 
   106   def tree_selection(): Option[(Debugger_Dockable.Thread_Entry, Option[Int])] =
   107     tree.getSelectionPath match {
   108       case null => None
   109       case path =>
   110         path.getPath.toList.map(n => n.asInstanceOf[DefaultMutableTreeNode].getUserObject) match {
   111           case List(_, t: Debugger_Dockable.Thread_Entry) =>
   112             Some((t, None))
   113           case List(_, t: Debugger_Dockable.Thread_Entry, s: Debugger_Dockable.Stack_Entry) =>
   114             Some((t, Some(s.index)))
   115           case _ => None
   116         }
   117     }
   118 
   119   def thread_selection(): Option[String] = tree_selection().map(sel => sel._1.thread_name)
   120 
   121   def focus_selection(): Option[Position.T] =
   122     tree_selection() match {
   123       case Some((t, opt_index)) =>
   124         val i = opt_index getOrElse 0
   125         if (i < t.debug_states.length) Some(t.debug_states(i).pos) else None
   126       case _ => None
   127     }
   128 
   129   private def update_tree(thread_entries: List[Debugger_Dockable.Thread_Entry])
   130   {
   131     val old_thread_selection = thread_selection()
   132 
   133     tree.clearSelection
   134     root.removeAllChildren
   135 
   136     for (thread_entry <- thread_entries) {
   137       val thread_node = new DefaultMutableTreeNode(thread_entry)
   138       for ((debug_state, i) <- thread_entry.debug_states.zipWithIndex) {
   139         val stack_node =
   140           new DefaultMutableTreeNode(Debugger_Dockable.Stack_Entry(debug_state, i))
   141         thread_node.add(stack_node)
   142       }
   143       root.add(thread_node)
   144     }
   145 
   146     tree.getModel.asInstanceOf[DefaultTreeModel].reload(root)
   147 
   148     old_thread_selection match {
   149       case Some(thread_name) if thread_entries.exists(t => t.thread_name == thread_name) =>
   150         val i =
   151           (for (t <- thread_entries.iterator.takeWhile(t => t.thread_name != thread_name))
   152             yield 1 + t.debug_states.length).sum
   153         tree.addSelectionRow(i + 1)
   154       case _ =>
   155     }
   156     for (i <- 0 until tree.getRowCount) tree.expandRow(i)
   157 
   158     tree.revalidate()
   159   }
   160 
   161   tree.addTreeSelectionListener(
   162     new TreeSelectionListener {
   163       override def valueChanged(e: TreeSelectionEvent) { update_focus(focus_selection()) }
   164     })
   165 
   166   tree.addMouseListener(new MouseAdapter {
   167     override def mouseClicked(e: MouseEvent)
   168     {
   169       val click = tree.getPathForLocation(e.getX, e.getY)
   170       if (click != null && e.getClickCount == 1) {
   171         (click.getLastPathComponent, tree.getLastSelectedPathComponent) match {
   172           case (node: DefaultMutableTreeNode, node1: DefaultMutableTreeNode) if node == node1 =>
   173             handle_update()
   174           case _ =>
   175         }
   176       }
   177     }
   178   })
   179 
   180   val tree_view = new JScrollPane(tree)
   181   tree_view.setMinimumSize(new Dimension(200, 50))
   182 
   183 
   184   /* controls */
   185 
   186   private val context_label = new Label("Context:") {
   187     tooltip = "Isabelle/ML context: type theory, Proof.context, Context.generic"
   188   }
   189   private val context_field =
   190     new Completion_Popup.History_Text_Field("isabelle-debugger-context")
   191     {
   192       setColumns(20)
   193       setToolTipText(context_label.tooltip)
   194       setFont(GUI.imitate_font(getFont, Font_Info.main_family(), 1.2))
   195     }
   196 
   197   private val expression_label = new Label("ML:") {
   198     tooltip = "Isabelle/ML or Standard ML expression"
   199   }
   200   private val expression_field =
   201     new Completion_Popup.History_Text_Field("isabelle-debugger-expression")
   202     {
   203       override def processKeyEvent(evt: KeyEvent)
   204       {
   205         if (evt.getID == KeyEvent.KEY_PRESSED && evt.getKeyCode == KeyEvent.VK_ENTER)
   206           eval_expression()
   207         super.processKeyEvent(evt)
   208       }
   209       { val max = getPreferredSize; max.width = Integer.MAX_VALUE; setMaximumSize(max) }
   210       setColumns(40)
   211       setToolTipText(expression_label.tooltip)
   212       setFont(GUI.imitate_font(getFont, Font_Info.main_family(), 1.2))
   213     }
   214 
   215   private val sml_button = new CheckBox("SML") {
   216     tooltip = "Official Standard ML instead of Isabelle/ML"
   217     selected = false
   218   }
   219 
   220   private val eval_button = new Button("<html><b>Eval</b></html>") {
   221       tooltip = "Evaluate ML expression within optional context"
   222       reactions += { case ButtonClicked(_) => eval_expression() }
   223     }
   224 
   225   private def eval_expression()
   226   {
   227     context_field.addCurrentToHistory()
   228     expression_field.addCurrentToHistory()
   229     tree_selection() match {
   230       case Some((t, opt_index)) if t.debug_states.nonEmpty =>
   231         Debugger.eval(t.thread_name, opt_index getOrElse 0,
   232           sml_button.selected, context_field.getText, expression_field.getText)
   233       case _ =>
   234     }
   235   }
   236 
   237   private val step_button = new Button("Step") {
   238     tooltip = "Single-step in depth-first order"
   239     reactions += { case ButtonClicked(_) => thread_selection().map(Debugger.step(_)) }
   240   }
   241 
   242   private val step_over_button = new Button("Step over") {
   243     tooltip = "Single-step within this function"
   244     reactions += { case ButtonClicked(_) => thread_selection().map(Debugger.step_over(_)) }
   245   }
   246 
   247   private val step_out_button = new Button("Step out") {
   248     tooltip = "Single-step outside this function"
   249     reactions += { case ButtonClicked(_) => thread_selection().map(Debugger.step_out(_)) }
   250   }
   251 
   252   private val continue_button = new Button("Continue") {
   253     tooltip = "Continue program on current thread, until next breakpoint"
   254     reactions += { case ButtonClicked(_) => thread_selection().map(Debugger.continue(_)) }
   255   }
   256 
   257   private val cancel_button = new Button("Cancel") {
   258     tooltip = "Interrupt program on current thread"
   259     reactions += { case ButtonClicked(_) => thread_selection().map(Debugger.cancel(_)) }
   260   }
   261 
   262   private val debugger_active =
   263     new JEdit_Options.Check_Box("ML_debugger_active", "Active", "Enable debugger at run-time")
   264 
   265   private val debugger_stepping =
   266     new JEdit_Options.Check_Box("ML_debugger_stepping", "Stepping", "Enable single-step mode")
   267 
   268   private val zoom = new Font_Info.Zoom_Box { def changed = handle_resize() }
   269 
   270   private val controls =
   271     new Wrap_Panel(Wrap_Panel.Alignment.Right)(
   272       step_button, step_over_button, step_out_button, continue_button, cancel_button,
   273       context_label, Component.wrap(context_field),
   274       expression_label, Component.wrap(expression_field),
   275       sml_button, eval_button,
   276       pretty_text_area.search_label, pretty_text_area.search_field,
   277       debugger_stepping, debugger_active, zoom)
   278   add(controls.peer, BorderLayout.NORTH)
   279 
   280 
   281   /* focus */
   282 
   283   override def focusOnDefaultComponent { eval_button.requestFocus }
   284 
   285   addFocusListener(new FocusAdapter {
   286     override def focusGained(e: FocusEvent) { update_focus(focus_selection()) }
   287     override def focusLost(e: FocusEvent) { update_focus(None) }
   288   })
   289 
   290   private def update_focus(focus: Option[Position.T])
   291   {
   292     if (Debugger.focus(focus) && focus.isDefined)
   293       PIDE.editor.hyperlink_position(current_snapshot, focus.get).foreach(_.follow(view))
   294   }
   295 
   296 
   297   /* main panel */
   298 
   299   val main_panel = new SplitPane(Orientation.Vertical) {
   300     oneTouchExpandable = true
   301     leftComponent = Component.wrap(tree_view)
   302     rightComponent = Component.wrap(pretty_text_area)
   303   }
   304   set_content(main_panel)
   305 
   306 
   307   /* main */
   308 
   309   private val main =
   310     Session.Consumer[Any](getClass.getName) {
   311       case _: Session.Global_Options =>
   312         Debugger.init(PIDE.session)
   313         GUI_Thread.later {
   314           debugger_active.load()
   315           debugger_stepping.load()
   316           handle_resize()
   317         }
   318 
   319       case _: Debugger.Update =>
   320         GUI_Thread.later { handle_update() }
   321     }
   322 
   323   override def init()
   324   {
   325     PIDE.session.global_options += main
   326     PIDE.session.debugger_updates += main
   327     Debugger.init(PIDE.session)
   328     Debugger.inc_active()
   329     handle_update()
   330     jEdit.propertiesChanged()
   331   }
   332 
   333   override def exit()
   334   {
   335     PIDE.session.global_options -= main
   336     PIDE.session.debugger_updates -= main
   337     delay_resize.revoke()
   338     update_focus(None)
   339     Debugger.dec_active()
   340     jEdit.propertiesChanged()
   341   }
   342 
   343 
   344   /* resize */
   345 
   346   private val delay_resize =
   347     GUI_Thread.delay_first(PIDE.options.seconds("editor_update_delay")) { handle_resize() }
   348 
   349   addComponentListener(new ComponentAdapter {
   350     override def componentResized(e: ComponentEvent) { delay_resize.invoke() }
   351     override def componentShown(e: ComponentEvent) { delay_resize.invoke() }
   352   })
   353 }