Quelle active.scala Sprache: Scala

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

Active areas within the document.
*/

package isabelle.jedit

import isabelle._
import org.gjt.sp.jedit.{ServiceManager, View}

object Active {
  abstract class Handler {
    def handle(
      view: View, text: String, elem: XML.Elem,
      doc_view: Document_View, snapshot: Document.Snapshot): Boolean
  }

  def handlers: List[Handler] =
    ServiceManager.getServiceNames(classOf[Handler]).toList
      .map(ServiceManager.getService(classOf[Handler], _))

  def action(view: View, text: String, elem: XML.Elem): Unit = {
    GUI_Thread.require {}

    Document_View.get(view.getTextArea) match {
      case Some(doc_view) =>
        doc_view.rich_text_area.robust_body(()) {
          val snapshot = Document_Model.snapshot(doc_view.model)
          if (!snapshot.is_outdated) {
            handlers.find(_.handle(view, text, elem, doc_view, snapshot))
          }
        }
      case None =>
    }
  }

  class Misc_Handler extends Active.Handler {
    override def handle(
      view: View, text: String, elem: XML.Elem,
      doc_view: Document_View, snapshot: Document.Snapshot
    ): Boolean = {
      val text_area = doc_view.text_area
      val model = doc_view.model
      val buffer = model.buffer

      elem match {
        case XML.Elem(Markup(Markup.BROWSER, _), body) =>
          Isabelle_Thread.fork(name = "browser") {
            val graph_file = Isabelle_System.tmp_file("graph")
            File.write(graph_file, XML.content(body))
            Isabelle_System.bash("isabelle browser -c " + File.bash_path(graph_file) + " &")
          }
          true

        case XML.Elem(Markup(Markup.THEORY_EXPORTS, props), _) =>
          GUI_Thread.later {
            val name = Markup.Name.unapply(props) getOrElse ""
            PIDE.editor.hyperlink_file(Isabelle_Export.vfs_prefix + name, focus = true).follow(view)
          }
          true

        case XML.Elem(Markup(Markup.JEDIT_ACTION, _), body) =>
          GUI_Thread.later {
            view.getInputHandler.invokeAction(XML.content(body))
          }
          true

        case XML.Elem(Markup(Markup.SIMP_TRACE_PANEL, props), _) =>
          val link =
            props match {
              case Position.Id(id) => PIDE.editor.hyperlink_command(snapshot, id, focus = true)
              case _ => None
            }
          GUI_Thread.later {
            link.foreach(_.follow(view))
            view.getDockableWindowManager.showDockableWindow("isabelle-simplifier-trace")
          }
          true

        case XML.Elem(Markup(Markup.SENDBACK, props), _) =>
          if (buffer.isEditable) {
            props match {
              case Position.Id(id) =>
                Isabelle.edit_command(snapshot, text_area,
                  props.contains(Markup.PADDING_COMMAND), id, text)
              case _ =>
                if (props.contains(Markup.PADDING_LINE)) {
                  Isabelle.insert_line_padding(text_area, text)
                }
                else text_area.setSelectedText(text)
            }
            text_area.requestFocus()
          }
          true

        case Protocol.Dialog(id, serial, result) =>
          model.session.dialog_result(id, serial, result)
          true

        case _ => false
      }
    }
  }
}

quality100%

¤ 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.