Quelle query_operation.scala Sprache: Scala

/*  Title:      Pure/PIDE/query_operation.scala
    Author:     Makarius

One-shot query operations via asynchronous print functions and temporary
document overlays.
*/

package isabelle

object Query_Operation {
  enum Status { case waiting, running, finished }

  object State {
    val empty: State = State()

    def make(command: Command, query: List[String]): State =
      State(instance = Document_ID.make().toString,
        location = Some(command),
        query = query,
        status = Status.waiting)
  }

  sealed case class State(
    instance: String = Document_ID.none.toString,
    location: Option[Command] = None,
    query: List[String] = Nil,
    update_pending: Boolean = false,
    output: List[XML.Tree] = Nil,
    status: Status = Status.finished,
    exec_id: Document_ID.Exec = Document_ID.none)
}

class Query_Operation(
  editor: Editor,
  editor_context: editor.Context,
  operation_name: String,
  consume_status: Query_Operation.Status => Unit,
  consume_output: Editor.Output => Unit
) {
  private val print_function = operation_name + "_query"

  /* implicit state -- owned by editor thread */

  private val current_state = Synchronized(Query_Operation.State.empty)

  def get_location: Option[Command] = current_state.value.location

  private def remove_overlay(): Unit = {
    val state = current_state.value
    for (command <- state.location) {
      editor.remove_overlay(command, print_function, state.instance :: state.query)
    }
  }

  /* content update */

  private def content_update(): Unit = {
    editor.require_dispatcher {}

    /* snapshot */

    val state0 = current_state.value

    val (output, removed) =
      state0.location match {
        case Some(cmd) =>
          val snapshot = editor.node_snapshot(cmd.node_name)
          val results = snapshot.command_results(cmd)
          val messages =
            List.from(
              for {
                case (_, msg@XML.Elem(Markup(Markup.RESULT, props@Markup.Instance(instance)), _))
                  <- results.iterator
                if instance == state0.instance
              } yield msg)
          val removed = !snapshot.get_node(cmd.node_name).commands.contains(cmd)
          (Editor.Output(snapshot, results, messages), removed)
        case None => (Editor.Output.init, true)
      }

    /* resolve sendback: static command id */

    def resolve_sendback(body: XML.Body): XML.Body = {
      state0.location match {
        case None => body
        case Some(command) =>
          def resolve(body: XML.Body): XML.Body =
            body map {
              case XML.Wrapped_Elem(m, b1, b2) => XML.Wrapped_Elem(m, resolve(b1), resolve(b2))
              case XML.Elem(Markup(Markup.SENDBACK, props), b) =>
                val props1 =
                  props.map({
                    case (Markup.ID, Value.Long(id)) if id == state0.exec_id =>
                      (Markup.ID, Value.Long(command.id))
                    case p => p
                  })
                XML.Elem(Markup(Markup.SENDBACK, props1), resolve(b))
              case XML.Elem(m, b) => XML.Elem(m, resolve(b))
              case t => t
            }
          resolve(body)
      }
    }

    /* output */

    val new_output =
      for {
        case XML.Elem(_, List(XML.Elem(markup, body))) <- output.messages
        if Markup.messages.contains(markup.name)
        body1 = resolve_sendback(body)
      } yield Protocol.make_message(body1, markup.name, props = markup.properties)

    /* status */

    def get_status(name: String, status: Query_Operation.Status): Option[Query_Operation.Status] =
      output.messages.collectFirst(
        { case XML.Elem(_, List(elem: XML.Elem)) if elem.name == name => status })

    val new_status =
      if (removed) Query_Operation.Status.finished
      else
        get_status(Markup.FINISHED, Query_Operation.Status.finished) orElse
        get_status(Markup.RUNNING, Query_Operation.Status.running) getOrElse
        Query_Operation.Status.waiting

    /* state update */

    if (new_status == Query_Operation.Status.running)
      output.messages.collectFirst(
      {
        case XML.Elem(Markup(_, Position.Id(id)), List(elem: XML.Elem))
        if elem.name == Markup.RUNNING => id
      }).foreach(id => current_state.change(_.copy(exec_id = id)))

    if (state0.output != new_output || state0.status != new_status) {
      if (output.snapshot.is_outdated) {
        current_state.change(_.copy(update_pending = true))
      }
      else {
        current_state.change(_.copy(update_pending = false))
        if (state0.output != new_output && !removed) {
          current_state.change(_.copy(output = new_output))
          consume_output(output.copy(messages = new_output))
        }
        if (state0.status != new_status) {
          current_state.change(_.copy(status = new_status))
          consume_status(new_status)
          if (new_status == Query_Operation.Status.finished)
            remove_overlay()
        }
      }
    }
  }

  /* query operations */

  def cancel_query(): Unit =
    editor.require_dispatcher { editor.session.cancel_exec(current_state.value.exec_id) }

  def apply_query(query: List[String]): Unit = {
    editor.require_dispatcher {}

    editor.current_node_snapshot(editor_context) match {
      case Some(snapshot) =>
        remove_overlay()
        current_state.change(_ => Query_Operation.State.empty)
        consume_output(Editor.Output.init)

        editor.current_command(editor_context, snapshot) match {
          case Some(command) =>
            val state = Query_Operation.State.make(command, query)
            current_state.change(_ => state)
            editor.insert_overlay(command, print_function, state.instance :: query)
          case None =>
        }

        consume_status(current_state.value.status)
        editor.flush()
      case None =>
    }
  }

  def query_command(): Option[(Document.Snapshot, Command)] =
    editor.require_dispatcher {
      val state = current_state.value
      for {
        command <- state.location
        snapshot = editor.node_snapshot(command.node_name) if !snapshot.is_outdated
      } yield (snapshot, command)
    }

  def locate_query(): Unit =
    for {
      (snapshot, command) <- query_command()
      link <- editor.hyperlink_command(snapshot, command.id, focus = true)
    } link.follow(editor_context)

  /* main */

  private val main =
    Session.Consumer[Session.Commands_Changed](getClass.getName) {
      case changed =>
        val state = current_state.value
        state.location match {
          case Some(command)
          if state.update_pending ||
            (state.status != Query_Operation.Status.finished &&
              changed.commands.contains(command)) =>
            editor.send_dispatcher { content_update() }
          case _ =>
        }
    }

  def activate(): Unit = {
    editor.session.commands_changed += main
  }

  def deactivate(): Unit = {
    editor.session.commands_changed -= main
    remove_overlay()
    current_state.change(_ => Query_Operation.State.empty)
    consume_output(Editor.Output.init)
    consume_status(Query_Operation.Status.finished)
  }
}

quality90%

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