Quelle debugger_dockable.scala Sprache: Scala

/*  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.KeyEvent
import javax.swing.JMenuItem
import javax.swing.event.TreeSelectionEvent
import javax.swing.tree.TreePath

import scala.collection.immutable.SortedMap
import scala.swing.Component

import org.gjt.sp.jedit.{jEdit, View}
import org.gjt.sp.jedit.menu.EnhancedMenuItem
import org.gjt.sp.jedit.textarea.JEditTextArea

object Debugger_Dockable {
  /* breakpoints */

  def get_breakpoint(text_area: JEditTextArea, offset: Text.Offset): Option[(Command, Long)] = {
    GUI_Thread.require {}

    Document_View.get(text_area) match {
      case Some(doc_view) =>
        val rendering = Document_View.rendering(doc_view)
        val range = JEdit_Lib.point_range(text_area.getBuffer, offset)
        rendering.breakpoint(range)
      case None => None
    }
  }

  /* context menu */

  def context_menu(text_area: JEditTextArea, offset: Text.Offset): List[JMenuItem] =
    if (PIDE.session.debugger.is_active() && get_breakpoint(text_area, offset).isDefined) {
      val context = jEdit.getActionContext()
      val name = "isabelle.toggle-breakpoint"
      List(new EnhancedMenuItem(context.getAction(name).getLabel, name, context))
    }
    else Nil
}

class Debugger_Dockable(view: View, position: String) extends Dockable(view, position) {
  dockable =>

  GUI_Thread.require {}

  private val debugger = PIDE.session.debugger

  /* component state -- owned by GUI thread */

  private var current_snapshot = Document.Snapshot.init
  private var current_threads: Debugger.Threads = SortedMap.empty
  private var current_output: List[XML.Tree] = Nil

  /* output area */

  private val output: Output_Area =
    new Output_Area(view, root_name = "Threads") {
      override def handle_search(search: Pretty_Text_Area.Search_Results): Unit = {}

      override def handle_tree_selection(path: TreePath): Unit = ()

      override def handle_update(): Unit = {
        val new_snapshot = PIDE.editor.current_node_snapshot(view).getOrElse(current_snapshot)
        val (new_threads, new_output) = debugger.status(tree_selection())

        if (new_threads != current_threads) update_tree(new_threads)

        if (new_output != current_output) {
          pretty_text_area.update(new_snapshot, Command.Results.empty, new_output)
        }

        current_snapshot = new_snapshot
        current_threads = new_threads
        current_output = new_output
      }

      override def handle_focus(): Unit = update_focus()
    }

  output.tree.addTreeSelectionListener({ (e: TreeSelectionEvent) =>
    update_focus()
    update_vals()
  })

  override def detach_operation: Option[() => Unit] =
    output.pretty_text_area.detach_operation

  output.setup(dockable)
  set_content(output.split_pane)

  /* tree view */

  private def tree_selection(path: TreePath = output.tree.getSelectionPath): Option[Debugger.Context] =
    output.tree.get_selection(path, { case c: Debugger.Context => c })

  private def thread_selection(): Option[String] = tree_selection().map(_.thread_name)

  private def update_tree(threads: Debugger.Threads): Unit = {
    val thread_contexts =
      (for ((a, b) <- threads.iterator)
        yield Debugger.Context(a, b)).toList

    val new_tree_selection =
      tree_selection() match {
        case Some(c) if thread_contexts.contains(c) => Some(c)
        case Some(c) if thread_contexts.exists(t => c.thread_name == t.thread_name) =>
          Some(c.reset)
        case _ => thread_contexts.headOption
      }

    output.tree.init_model {
      for (thread <- thread_contexts) {
        val thread_node = Tree_View.Node(thread)
        for ((_, i) <- thread.debug_states.zipWithIndex) {
          thread_node.add(Tree_View.Node(thread.select(i)))
        }
        output.tree.root.add(thread_node)
      }
    }

    for (i <- Range.inclusive(output.tree.getRowCount - 1, 1, -1)) output.tree.expandRow(i)

    new_tree_selection match {
      case Some(c) =>
        val i =
          (for (t <- thread_contexts.iterator.takeWhile(t => c.thread_name != t.thread_name))
            yield t.size).sum
        output.tree.addSelectionRow(i + c.index + 1)
      case None =>
    }

    output.tree.revalidate()
  }

  def update_vals(): Unit = {
    tree_selection() match {
      case Some(c) if c.stack_state.isDefined =>
        debugger.print_vals(c, sml_button.selected, context_field.getText)
      case Some(c) =>
        debugger.clear_output(c.thread_name)
      case None =>
    }
  }

  /* controls */

  private val break_button = new GUI.Check("Break", init = debugger.is_break()) {
    tooltip = "Break running threads at next possible breakpoint"
    override def clicked(state: Boolean): Unit = debugger.set_break(state)
  }

  private val continue_button = new GUI.Button("Continue") {
    tooltip = "Continue program on current thread, until next breakpoint"
    override def clicked(): Unit = thread_selection().foreach(debugger.continue)
  }

  private val step_button = new GUI.Button("Step") {
    tooltip = "Single-step in depth-first order"
    override def clicked(): Unit = thread_selection().foreach(debugger.step)
  }

  private val step_over_button = new GUI.Button("Step over") {
    tooltip = "Single-step within this function"
    override def clicked(): Unit = thread_selection().foreach(debugger.step_over)
  }

  private val step_out_button = new GUI.Button("Step out") {
    tooltip = "Single-step outside this function"
    override def clicked(): Unit = thread_selection().foreach(debugger.step_out)
  }

  private val context_tooltip = "Isabelle/ML context: type theory, Proof.context, Context.generic"
  private val context_field =
    new Completion_Popup.History_Text_Field("isabelle-debugger-context") {
      override def processKeyEvent(evt: KeyEvent): Unit = {
        if (evt.getID == KeyEvent.KEY_PRESSED && evt.getKeyCode == KeyEvent.VK_ENTER) {
          eval_expression()
        }
        super.processKeyEvent(evt)
      }
      setColumns(20)
      setToolTipText(context_tooltip)
      setFont(GUI.imitate_font(getFont, scale = 1.2))
    }
  private val context_label = new GUI.Label("Context:", context_field) {
    tooltip = context_tooltip
  }

  private val expression_tooltip = "Isabelle/ML or Standard ML expression"
  private val expression_field =
    new Completion_Popup.History_Text_Field("isabelle-debugger-expression") {
      override def processKeyEvent(evt: KeyEvent): Unit = {
        if (evt.getID == KeyEvent.KEY_PRESSED && evt.getKeyCode == KeyEvent.VK_ENTER) {
          eval_expression()
        }
        super.processKeyEvent(evt)
      }
      { val max = getPreferredSize; max.width = Int.MaxValue; setMaximumSize(max) }
      setColumns(40)
      setToolTipText(expression_tooltip)
      setFont(GUI.imitate_font(getFont, scale = 1.2))
    }
  private val expression_label = new GUI.Label("ML:", expression_field) {
    tooltip = expression_tooltip
  }

  private val eval_button =
    new GUI.Button(GUI.Style_HTML.enclose_bold("Eval")) {
      tooltip = "Evaluate ML expression within optional context"
      override def clicked(): Unit = eval_expression()
    }

  private def eval_expression(): Unit = {
    context_field.addCurrentToHistory()
    expression_field.addCurrentToHistory()
    tree_selection() match {
      case Some(c) if c.debug_index.isDefined =>
        debugger.eval(c, sml_button.selected, context_field.getText, expression_field.getText)
      case _ =>
    }
  }

  private val sml_button = new GUI.Check("SML") {
    tooltip = "Official Standard ML instead of Isabelle/ML"
  }

  private val controls =
    Wrap_Panel(
      List(
        break_button, continue_button, step_button, step_over_button, step_out_button,
        context_label, Component.wrap(context_field),
        expression_label, Component.wrap(expression_field), eval_button, sml_button) :::
      output.pretty_text_area.search_zoom_components)

  add(controls.peer, BorderLayout.NORTH)

  /* focus */

  override def focusOnDefaultComponent(): Unit = eval_button.requestFocus()

  private def update_focus(): Unit = {
    for (c <- tree_selection()) {
      debugger.set_focus(c)
      for {
        pos <- c.debug_position
        link <- PIDE.editor.hyperlink_position(current_snapshot, pos)
      } link.follow(view)
    }
    JEdit_Lib.jedit_text_areas(view.getBuffer).foreach(_.repaint())
  }

  /* main */

  private val main =
    Session.Consumer[Any](getClass.getName) {
      case _: Session.Global_Options =>
        GUI_Thread.later { output.handle_resize() }

      case Debugger.Update =>
        GUI_Thread.later {
          break_button.selected = debugger.is_break()
          output.handle_update()
        }
    }

  override def init(): Unit = {
    PIDE.session.global_options += main
    PIDE.session.debugger_updates += main
    debugger.init(dockable)
    output.init()
    jEdit.propertiesChanged()
  }

  override def exit(): Unit = {
    PIDE.session.global_options -= main
    PIDE.session.debugger_updates -= main
    output.exit()
    debugger.exit(dockable)
    jEdit.propertiesChanged()
  }
}

quality92%

¤ Dauer der Verarbeitung: 0.11 Sekunden (vorverarbeitet) ¤

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.