Ziele Untersuchung
mit Columbo Integrität von
Datenbanken Interaktion und
Portierbarkeit Ergonomie der
Schnittstellen

Angebot Produkte Projekt Beratung

Mittel Analytik Modellierung Sprachen Algebra Logik Hardware Denken Kreativität

Zusammenhänge Gesellschaft Wirtschaft Branche Firma


products/Sources/formale Sprachen/Isabelle/Tools/jEdit/src/ (Beweissystem Isabelle Version 2025-1^©) Datei vom 16.11.2025 mit Größe 3 kB

Quelle state_dockable.scala Sprache: Scala

/*  Title:      Tools/jEdit/src/state_dockable.scala
    Author:     Makarius

Dockable window for proof state output.
*/

package isabelle.jedit

import isabelle._

import java.awt.BorderLayout

import org.gjt.sp.jedit.View

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

  GUI_Thread.require {}

  /* output text area */

  private val output: Output_Area =
    new Output_Area(view) {
      override def handle_shown(): Unit = split_pane_layout()
    }

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

  private val print_state =
    new Query_Operation(PIDE.editor, view, "print_state", _ => (),
      output.pretty_text_area.update_output)

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

  /* update */

  def update_request(): Unit =
    GUI_Thread.require { print_state.apply_query(Nil) }

  def update(): Unit = {
    GUI_Thread.require {}

    PIDE.editor.current_node_snapshot(view) match {
      case Some(snapshot) =>
        (PIDE.editor.current_command(view, snapshot), print_state.get_location) match {
          case (Some(command1), Some(command2)) if command1.id == command2.id =>
          case _ => update_request()
        }
      case None =>
    }
  }

  /* auto update */

  private var auto_update_enabled = true

  private def auto_update(): Unit =
    GUI_Thread.require { if (auto_update_enabled) update() }

  /* controls */

  private val auto_update_button = new GUI.Check("Auto update", init = auto_update_enabled) {
    tooltip = "Indicate automatic update following cursor movement"
    override def clicked(state: Boolean): Unit = {
      auto_update_enabled = state
      auto_update()
    }
  }

  private val auto_hovering_button = new JEdit_Options.auto_hovering.GUI

  private val update_button = new GUI.Button(GUI.Style_HTML.enclose_bold("Update")) {
    tooltip = "Update display according to the command at cursor position"
    override def clicked(): Unit = update_request()
  }

  private val locate_button = new GUI.Button("Locate") {
    tooltip = "Locate printed command within source text"
    override def clicked(): Unit = print_state.locate_query()
  }

  private val controls =
    Wrap_Panel(
      List(auto_hovering_button, auto_update_button, update_button, locate_button) :::
      output.pretty_text_area.search_zoom_components)

  add(controls.peer, BorderLayout.NORTH)

  /* main */

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

      case changed: Session.Commands_Changed =>
        if (changed.assignment) GUI_Thread.later { auto_update() }

      case Session.Caret_Focus =>
        GUI_Thread.later { auto_update() }
    }

  override def init(): Unit = {
    PIDE.session.global_options += main
    PIDE.session.commands_changed += main
    PIDE.session.caret_focus += main
    output.init()
    print_state.activate()
    auto_update()
  }

  override def exit(): Unit = {
    print_state.deactivate()
    PIDE.session.caret_focus -= main
    PIDE.session.global_options -= main
    PIDE.session.commands_changed -= main
    output.exit()
  }
}

quality100%

¤ Dauer der Verarbeitung: 0.1 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.