Quellcode-Bibliothek

^© Kompilation durch diese Firma

[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]

Datei: state_panel.scala Sprache: Scala

Original von: Isabelle^©

/*  Title:      Tools/VSCode/src/state_panel.scala
    Author:     Makarius

Show proof state.
*/

package isabelle.vscode

import isabelle._

object State_Panel
{
  private val make_id = Counter.make()
  private val instances = Synchronized(Map.empty[Counter.ID, State_Panel])

  def init(server: Language_Server)
  {
    val instance = new State_Panel(server)
    instances.change(_ + (instance.id -> instance))
    instance.init()
  }

  def exit(id: Counter.ID)
  {
    instances.change(map =>
      map.get(id) match {
        case None => map
        case Some(instance) => instance.exit(); map - id
      })
  }

  def locate(id: Counter.ID): Unit =
    instances.value.get(id).foreach(state =>
      state.server.editor.send_dispatcher(state.locate()))

  def update(id: Counter.ID): Unit =
    instances.value.get(id).foreach(state =>
      state.server.editor.send_dispatcher(state.update()))

  def auto_update(id: Counter.ID, enabled: Boolean): Unit =
    instances.value.get(id).foreach(state =>
      state.server.editor.send_dispatcher(state.auto_update(Some(enabled))))
}

class State_Panel private(val server: Language_Server)
{
  /* output */

  val id: Counter.ID = State_Panel.make_id()

  private def output(content: String): Unit =
    server.channel.write(LSP.State_Output(id, content))

  /* query operation */

  private val output_active = Synchronized(true)

  private val print_state =
    new Query_Operation(server.editor, (), "print_state", _ => (),
      (snapshot, results, body) =>
        if (output_active.value) {
          val text = server.resources.output_pretty_message(Pretty.separate(body))
          val content =
            HTML.output_document(
              List(HTML.style(HTML.fonts_css()),
                HTML.style_file(HTML.isabelle_css),
                HTML.script(controls_script)),
              List(controls, HTML.source(text)),
              css = "", structural = true)
          output(content)
        })

  def locate() { print_state.locate_query() }

  def update()
  {
    server.editor.current_node_snapshot(()) match {
      case Some(snapshot) =>
        (server.editor.current_command((), snapshot), print_state.get_location) match {
          case (Some(command1), Some(command2)) if command1.id == command2.id =>
          case _ => print_state.apply_query(Nil)
        }
      case None =>
    }
  }

  /* auto update */

  private val auto_update_enabled = Synchronized(true)

  def auto_update(set: Option[Boolean] = None)
  {
    val enabled =
      auto_update_enabled.guarded_access(a =>
        set match {
          case None => Some((a, a))
          case Some(b) => Some((b, b))
        })
    if (enabled) update()
  }

  /* controls */

  private def controls_script =
"""
const vscode = acquireVsCodeApi();

function invoke_auto_update(enabled)
{ vscode.postMessage({'command': 'auto_update', 'enabled': enabled}) }

function invoke_update()
{ vscode.postMessage({'command': 'update'}) }

function invoke_locate()
{ vscode.postMessage({'command': 'locate'}) }
"""

  private def auto_update_button: XML.Elem =
    HTML.GUI.checkbox(HTML.text("Auto update"),
      name = "auto_update",
      tooltip = "Indicate automatic update following cursor movement",
      selected = auto_update_enabled.value,
      script = "invoke_auto_update(this.checked)")

  private def update_button: XML.Elem =
    HTML.GUI.button(List(HTML.bold(HTML.text("Update"))),
      name = "update",
      tooltip = "Update display according to the command at cursor position",
      script = "invoke_update()")

  private def locate_button: XML.Elem =
    HTML.GUI.button(HTML.text("Locate"),
      name = "locate",
      tooltip = "Locate printed command within source text",
      script = "invoke_locate()")

  private def controls: XML.Elem =
    HTML.Wrap_Panel(List(auto_update_button, update_button, locate_button))

  /* main */

  private val main =
    Session.Consumer[Any](getClass.getName) {
      case changed: Session.Commands_Changed =>
        if (changed.assignment) auto_update()

      case Session.Caret_Focus =>
        auto_update()
    }

  def init()
  {
    server.session.commands_changed += main
    server.session.caret_focus += main
    server.editor.send_wait_dispatcher { print_state.activate() }
    server.editor.send_dispatcher { auto_update() }
  }

  def exit()
  {
    output_active.change(_ => false)
    server.session.commands_changed -= main
    server.session.caret_focus -= main
    server.editor.send_wait_dispatcher { print_state.deactivate() }
  }
}

¤ Dauer der Verarbeitung: 0.0 Sekunden (vorverarbeitet) ¤

Download des Quellennavigators
Download des sprechenden Kalenders
in der Quellcodebibliothek suchen

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.