Quelle editor.scala Sprache: Scala

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

General editor operations.
*/

package isabelle

object Editor {
  /* output messages */

  object Output {
    val none: Output = Output(defined = false)
    val init: Output = Output()
  }

  sealed case class Output(
    snapshot: Document.Snapshot = Document.Snapshot.init,
    results: Command.Results = Command.Results.empty,
    messages: List[XML.Elem] = Nil,
    defined: Boolean = true
  ) {
    def proper: Boolean = messages.nonEmpty && defined
  }
}

abstract class Editor {
  type Context

  /* PIDE session and document model */

  def session: Session
  def flush(): Unit
  def invoke(): Unit
  def revoke(): Unit

  def get_models(): Iterable[Document.Model]

  /* document editor */

  protected val document_editor: Synchronized[Document_Editor.State] =
    Synchronized(Document_Editor.State())

  protected def document_state(): Document_Editor.State = document_editor.value

  protected def document_state_changed(): Unit = {}
  private def document_state_change(f: Document_Editor.State => Document_Editor.State): Unit = {
    val changed =
      document_editor.change_result { st =>
        val st1 = f(st)
        val changed =
          st.active_document_theories != st1.active_document_theories ||
          st.selection != st1.selection
        (changed, st1)
      }
    if (changed) document_state_changed()
  }

  def document_session(): Document_Editor.Session =
    document_state().session(session)

  def document_required(): List[Document.Node.Name] = {
    val st = document_state()
    if (st.is_active) {
      for {
        a <- st.all_document_theories
        b = session.resources.migrate_name(a)
        if st.selection(b.theory)
      } yield b
    }
    else Nil
  }

  def document_node_required(name: Document.Node.Name): Boolean = {
    val st = document_state()
    st.is_active &&
    st.selection.contains(name.theory) &&
    st.all_document_theories.exists(a => a.theory == name.theory)
  }

  def document_theories(): List[Document.Node.Name] =
    document_state().active_document_theories.map(session.resources.migrate_name)

  def document_selection(): Set[String] = document_state().selection

  def document_setup(background: Option[Sessions.Background]): Unit =
    document_state_change(_.copy(session_background = background))

  def document_select(
    theories: Iterable[String],
    set: Boolean = false,
    toggle: Boolean = false
  ): Unit = document_state_change(_.select(theories, set = set, toggle = toggle))

  def document_select_all(set: Boolean = false): Unit =
    document_state_change(st =>
      st.select(st.active_document_theories.map(_.theory), set = set))

  def document_init(id: AnyRef): Unit = document_state_change(_.register_view(id))
  def document_exit(id: AnyRef): Unit = document_state_change(_.unregister_view(id))

  /* current situation */

  def current_node(context: Context): Option[Document.Node.Name]
  def current_node_snapshot(context: Context): Option[Document.Snapshot]
  def node_snapshot(name: Document.Node.Name): Document.Snapshot
  def current_command(context: Context, snapshot: Document.Snapshot): Option[Command]

  /* output messages */

  def output_state(): Boolean

  def output(
    snapshot: Document.Snapshot,
    caret_offset: Text.Offset,
    restriction: Option[Set[Command]] = None
  ): Editor.Output = {
    if (snapshot.is_outdated) Editor.Output.none
    else {
      val thy_command_range = snapshot.loaded_theory_command(caret_offset)
      val thy_command = thy_command_range.map(_._1)

      def filter(msg: XML.Elem): Boolean =
        (for {
          (command, command_range) <- thy_command_range
          msg_offset <- Position.Offset.unapply(msg.markup.properties)
        } yield command_range.contains(command.chunk.decode(msg_offset))) getOrElse true

      thy_command orElse snapshot.current_command(snapshot.node_name, caret_offset) match {
        case None => Editor.Output.init
        case Some(command) =>
          if (thy_command.isDefined || restriction.isEmpty || restriction.get.contains(command)) {
            val results = snapshot.command_results(command)
            val messages = {
              val (states, other) = {
                List.from(
                  for ((_, msg) <- results.iterator if !Protocol.is_result(msg) && filter(msg))
                    yield msg).partition(Protocol.is_state)
              }
              val (urgent, regular) = other.partition(Protocol.is_urgent)
              urgent ::: (if (output_state()) states else Nil) ::: regular
            }
            Editor.Output(snapshot = snapshot, results = results, messages = messages)
          }
          else Editor.Output.none
      }
    }
  }

  /* overlays */

  def node_overlays(name: Document.Node.Name): Document.Node.Overlays
  def insert_overlay(command: Command, fn: String, args: List[String]): Unit
  def remove_overlay(command: Command, fn: String, args: List[String]): Unit

  /* hyperlinks */

  abstract class Hyperlink {
    def external: Boolean = false
    def follow(context: Context): Unit
  }

  def hyperlink_command(
    snapshot: Document.Snapshot,
    id: Document_ID.Generic,
    offset: Symbol.Offset = 0,
    focus: Boolean = false): Option[Hyperlink]

  /* dispatcher thread */

  def assert_dispatcher[A](body: => A): A
  def require_dispatcher[A](body: => A): A
  def send_dispatcher(body: => Unit): Unit
  def send_wait_dispatcher(body: => Unit): Unit
}

quality94%

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