Quellcode-Bibliothek

^© Kompilation durch diese Firma

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

Datei: document_model.scala Sprache: Scala

Original von: Isabelle^©

/*  Title:      Tools/jEdit/src/document_model.scala
    Author:     Fabian Immler, TU Munich
    Author:     Makarius

Document model connected to jEdit buffer or external file: content of theory
node or auxiliary file (blob).
*/

package isabelle.jedit

import isabelle._

import java.io.{File => JFile}

import scala.collection.mutable
import scala.annotation.tailrec

import org.gjt.sp.jedit.View
import org.gjt.sp.jedit.Buffer
import org.gjt.sp.jedit.buffer.{BufferAdapter, BufferListener, JEditBuffer}

object Document_Model
{
  /* document models */

  sealed case class State(
    models: Map[Document.Node.Name, Document_Model] = Map.empty,
    buffer_models: Map[JEditBuffer, Buffer_Model] = Map.empty,
    overlays: Document.Overlays = Document.Overlays.empty)
  {
    def file_models_iterator: Iterator[(Document.Node.Name, File_Model)] =
      for {
        (node_name, model) <- models.iterator
        if model.isInstanceOf[File_Model]
      } yield (node_name, model.asInstanceOf[File_Model])

    def document_blobs: Document.Blobs =
      Document.Blobs(
        (for {
          (node_name, model) <- models.iterator
          blob <- model.get_blob
        } yield (node_name -> blob)).toMap)

    def open_buffer(session: Session, node_name: Document.Node.Name, buffer: Buffer)
      : (Buffer_Model, State) =
    {
      val old_model =
        models.get(node_name) match {
          case Some(file_model: File_Model) => Some(file_model)
          case Some(buffer_model: Buffer_Model) => Some(buffer_model.exit())
          case _ => None
        }
      val buffer_model = Buffer_Model(session, node_name, buffer).init(old_model)
      (buffer_model,
        copy(models = models + (node_name -> buffer_model),
          buffer_models = buffer_models + (buffer -> buffer_model)))
    }

    def close_buffer(buffer: JEditBuffer): State =
    {
      buffer_models.get(buffer) match {
        case None => this
        case Some(buffer_model) =>
          val file_model = buffer_model.exit()
          copy(models = models + (file_model.node_name -> file_model),
            buffer_models = buffer_models - buffer)
      }
    }

    def provide_file(session: Session, node_name: Document.Node.Name, text: String): State =
      if (models.isDefinedAt(node_name)) this
      else {
        val edit = Text.Edit.insert(0, text)
        val model = File_Model.init(session, node_name, text, pending_edits = List(edit))
        copy(models = models + (node_name -> model))
      }
  }

  private val state = Synchronized(State())  // owned by GUI thread

  def get_models(): Map[Document.Node.Name, Document_Model] = state.value.models
  def get(name: Document.Node.Name): Option[Document_Model] = get_models().get(name)
  def get(buffer: JEditBuffer): Option[Buffer_Model] = state.value.buffer_models.get(buffer)

  def document_blobs(): Document.Blobs = state.value.document_blobs

  /* bibtex */

  def bibtex_entries_iterator(): Iterator[Text.Info[(String, Document_Model)]] =
    Bibtex.entries_iterator(state.value.models)

  def bibtex_completion(history: Completion.History, rendering: Rendering, caret: Text.Offset)
      : Option[Completion.Result] =
    Bibtex.completion(history, rendering, caret, state.value.models)

  /* overlays */

  def node_overlays(name: Document.Node.Name): Document.Node.Overlays =
    state.value.overlays(name)

  def insert_overlay(command: Command, fn: String, args: List[String]): Unit =
    state.change(st => st.copy(overlays = st.overlays.insert(command, fn, args)))

  def remove_overlay(command: Command, fn: String, args: List[String]): Unit =
    state.change(st => st.copy(overlays = st.overlays.remove(command, fn, args)))

  /* sync external files */

  def sync_files(changed_files: Set[JFile]): Boolean =
  {
    state.change_result(st =>
      {
        val changed_models =
          (for {
            (node_name, model) <- st.file_models_iterator
            file <- model.file if changed_files(file)
            text <- PIDE.resources.read_file_content(node_name)
            if model.content.text != text
          } yield {
            val content = Document_Model.File_Content(text)
            val edits = Text.Edit.replace(0, model.content.text, text)
            (node_name, model.copy(content = content, pending_edits = model.pending_edits ::: edits))
          }).toList
        if (changed_models.isEmpty) (false, st)
        else (true, st.copy(models = (st.models /: changed_models)(_ + _)))
      })
  }

  /* syntax */

  def syntax_changed(names: List[Document.Node.Name])
  {
    GUI_Thread.require {}

    val models = state.value.models
    for (name <- names.iterator; model <- models.get(name)) {
      model match { case buffer_model: Buffer_Model => buffer_model.syntax_changed() case _ => }
    }
  }

  /* init and exit */

  def init(session: Session, node_name: Document.Node.Name, buffer: Buffer): Buffer_Model =
  {
    GUI_Thread.require {}
    state.change_result(st =>
      st.buffer_models.get(buffer) match {
        case Some(buffer_model) if buffer_model.node_name == node_name =>
          buffer_model.init_token_marker()
          (buffer_model, st)
        case _ =>
          val res = st.close_buffer(buffer).open_buffer(session, node_name, buffer)
          buffer.propertiesChanged()
          res
      })
  }

  def exit(buffer: Buffer)
  {
    GUI_Thread.require {}
    state.change(st =>
      if (st.buffer_models.isDefinedAt(buffer)) {
        val res = st.close_buffer(buffer)
        buffer.propertiesChanged()
        res
      }
      else st)
  }

  def provide_files(session: Session, files: List[(Document.Node.Name, String)])
  {
    GUI_Thread.require {}
    state.change(st =>
      (st /: files) { case (st1, (node_name, text)) => st1.provide_file(session, node_name, text) })
  }

  /* required nodes */

  def required_nodes(): Set[Document.Node.Name] =
    (for {
      (node_name, model) <- state.value.models.iterator
      if model.node_required
    } yield node_name).toSet

  def node_required(name: Document.Node.Name, toggle: Boolean = false, set: Boolean = false)
  {
    GUI_Thread.require {}

    val changed =
      state.change_result(st =>
        st.models.get(name) match {
          case None => (false, st)
          case Some(model) =>
            val required = if (toggle) !model.node_required else set
            model match {
              case model1: File_Model if required != model1.node_required =>
                (true, st.copy(models = st.models + (name -> model1.copy(node_required = required))))
              case model1: Buffer_Model if required != model1.node_required =>
                model1.set_node_required(required); (true, st)
              case _ => (false, st)
            }
        })
    if (changed) {
      PIDE.plugin.options_changed()
      PIDE.editor.flush()
    }
  }

  def view_node_required(view: View, toggle: Boolean = false, set: Boolean = false): Unit =
    Document_Model.get(view.getBuffer).foreach(model =>
      node_required(model.node_name, toggle = toggle, set = set))

  /* flushed edits */

  def flush_edits(hidden: Boolean, purge: Boolean): (Document.Blobs, List[Document.Edit_Text]) =
  {
    GUI_Thread.require {}

    state.change_result(st =>
      {
        val doc_blobs = st.document_blobs

        val buffer_edits =
          (for {
            (_, model) <- st.buffer_models.iterator
            edit <- model.flush_edits(doc_blobs, hidden).iterator
          } yield edit).toList

        val file_edits =
          (for {
            (node_name, model) <- st.file_models_iterator
            (edits, model1) <- model.flush_edits(doc_blobs, hidden)
          } yield (edits, node_name -> model1)).toList

        val model_edits = buffer_edits ::: file_edits.flatMap(_._1)

        val purge_edits =
          if (purge) {
            val purged =
              (for ((node_name, model) <- st.file_models_iterator)
               yield (node_name -> model.purge_edits(doc_blobs))).toList

            val imports =
            {
              val open_nodes =
                (for ((_, model) <- st.buffer_models.iterator) yield model.node_name).toList
              val touched_nodes = model_edits.map(_._1)
              val pending_nodes = for ((node_name, None) <- purged) yield node_name
              (open_nodes ::: touched_nodes ::: pending_nodes).map((_, Position.none))
            }
            val retain = PIDE.resources.dependencies(imports).theories.toSet

            for ((node_name, Some(edits)) <- purged if !retain(node_name); edit <- edits)
              yield edit
          }
          else Nil

        val st1 = st.copy(models = st.models ++ file_edits.map(_._2) -- purge_edits.map(_._1))
        PIDE.plugin.file_watcher.purge(
          (for {
            (_, model) <- st1.file_models_iterator
            file <- model.file
          } yield file.getParentFile).toSet)

        ((doc_blobs, model_edits ::: purge_edits), st1)
      })
  }

  /* file content */

  sealed case class File_Content(text: String)
  {
    lazy val bytes: Bytes = Bytes(Symbol.encode(text))
    lazy val chunk: Symbol.Text_Chunk = Symbol.Text_Chunk(text)
    lazy val bibtex_entries: List[Text.Info[String]] =
      try { Bibtex.entries(text) }
      catch { case ERROR(_) => Nil }
  }

  /* HTTP preview */

  private val plain_text_prefix = "plain_text="

  def open_preview(view: View, plain_text: Boolean)
  {
    Document_Model.get(view.getBuffer) match {
      case Some(model) =>
        val name = model.node_name
        val url =
          PIDE.plugin.http_server.url + PIDE.plugin.http_root + "/preview?" +
            (if (plain_text) plain_text_prefix else "") + Url.encode(name.node)
        PIDE.editor.hyperlink_url(url).follow(view)
      case _ =>
    }
  }

  def http_handlers(http_root: String): List[HTTP.Handler] =
  {
    val fonts_root = http_root + "/fonts"
    val preview_root = http_root + "/preview"

    val html =
      HTTP.get(preview_root, arg =>
        for {
          query <- Library.try_unprefix(preview_root + "?", arg.uri.toString).map(Url.decode)
          name = Library.perhaps_unprefix(plain_text_prefix, query)
          model <- get(PIDE.resources.node_name(name))
        }
        yield {
          val snapshot = model.await_stable_snapshot()
          val html_context = Presentation.html_context(fonts_url = HTML.fonts_dir(fonts_root))
          val document =
            Presentation.html_document(
              PIDE.resources, snapshot, html_context, Presentation.elements2,
              plain_text = query.startsWith(plain_text_prefix))
          HTTP.Response.html(document.content)
        })

    List(HTTP.fonts(fonts_root), html)
  }
}

sealed abstract class Document_Model extends Document.Model
{
  /* perspective */

  def document_view_ranges(snapshot: Document.Snapshot): List[Text.Range] = Nil

  def node_perspective(
    doc_blobs: Document.Blobs, hidden: Boolean): (Boolean, Document.Node.Perspective_Text) =
  {
    GUI_Thread.require {}

    if (Isabelle.continuous_checking && is_theory) {
      val snapshot = this.snapshot()

      val reparse = snapshot.node.load_commands_changed(doc_blobs)
      val perspective =
        if (hidden) Text.Perspective.empty
        else {
          val view_ranges = document_view_ranges(snapshot)
          val load_ranges = snapshot.commands_loading_ranges(PIDE.editor.visible_node)
          Text.Perspective(view_ranges ::: load_ranges)
        }
      val overlays = PIDE.editor.node_overlays(node_name)

      (reparse, Document.Node.Perspective(node_required, perspective, overlays))
    }
    else (false, Document.Node.no_perspective_text)
  }

  /* snapshot */

  @tailrec final def await_stable_snapshot(): Document.Snapshot =
  {
    val snapshot = this.snapshot()
    if (snapshot.is_outdated) {
      PIDE.options.seconds("editor_output_delay").sleep
      await_stable_snapshot()
    }
    else snapshot
  }
}

object File_Model
{
  def empty(session: Session): File_Model =
    File_Model(session, Document.Node.Name.empty, None, Document_Model.File_Content(""),
      false, Document.Node.no_perspective_text, Nil)

  def init(session: Session,
    node_name: Document.Node.Name,
    text: String,
    node_required: Boolean = false,
    last_perspective: Document.Node.Perspective_Text = Document.Node.no_perspective_text,
    pending_edits: List[Text.Edit] = Nil): File_Model =
  {
    val file = JEdit_Lib.check_file(node_name.node)
    file.foreach(PIDE.plugin.file_watcher.register_parent(_))

    val content = Document_Model.File_Content(text)
    val node_required1 = node_required || File_Format.registry.is_theory(node_name)
    File_Model(session, node_name, file, content, node_required1, last_perspective, pending_edits)
  }
}

case class File_Model(
  session: Session,
  node_name: Document.Node.Name,
  file: Option[JFile],
  content: Document_Model.File_Content,
  node_required: Boolean,
  last_perspective: Document.Node.Perspective_Text,
  pending_edits: List[Text.Edit]) extends Document_Model
{
  /* text */

  def get_text(range: Text.Range): Option[String] =
    range.try_substring(content.text)

  /* header */

  def node_header: Document.Node.Header =
    PIDE.resources.special_header(node_name) getOrElse
      PIDE.resources.check_thy(node_name, Scan.char_reader(content.text), strict = false)

  /* content */

  def node_position(offset: Text.Offset): Line.Node_Position =
    Line.Node_Position(node_name.node,
      Line.Position.zero.advance(content.text.substring(0, offset)))

  def get_blob: Option[Document.Blob] =
    if (is_theory) None
    else Some(Document.Blob(content.bytes, content.text, content.chunk, pending_edits.nonEmpty))

  def bibtex_entries: List[Text.Info[String]] =
    if (Bibtex.is_bibtex(node_name.node)) content.bibtex_entries else Nil

  /* edits */

  def update_text(text: String): Option[File_Model] =
    Text.Edit.replace(0, content.text, text) match {
      case Nil => None
      case edits =>
        val content1 = Document_Model.File_Content(text)
        val pending_edits1 = pending_edits ::: edits
        Some(copy(content = content1, pending_edits = pending_edits1))
    }

  def flush_edits(doc_blobs: Document.Blobs, hidden: Boolean)
    : Option[(List[Document.Edit_Text], File_Model)] =
  {
    val (reparse, perspective) = node_perspective(doc_blobs, hidden)
    if (reparse || pending_edits.nonEmpty || last_perspective != perspective) {
      val edits = node_edits(node_header, pending_edits, perspective)
      Some((edits, copy(last_perspective = perspective, pending_edits = Nil)))
    }
    else None
  }

  def purge_edits(doc_blobs: Document.Blobs): Option[List[Document.Edit_Text]] =
    if (pending_edits.nonEmpty ||
        !File_Format.registry.is_theory(node_name) &&
          (node_required || !Document.Node.is_no_perspective_text(last_perspective))) None
    else {
      val text_edits = List(Text.Edit.remove(0, content.text))
      Some(node_edits(Document.Node.no_header, text_edits, Document.Node.no_perspective_text))
    }

  /* snapshot */

  def is_stable: Boolean = pending_edits.isEmpty
  def snapshot(): Document.Snapshot = session.snapshot(node_name, pending_edits)
}

case class Buffer_Model(session: Session, node_name: Document.Node.Name, buffer: Buffer)
  extends Document_Model
{
  /* text */

  def get_text(range: Text.Range): Option[String] =
    JEdit_Lib.get_text(buffer, range)

  /* header */

  def node_header(): Document.Node.Header =
  {
    GUI_Thread.require {}

    PIDE.resources.special_header(node_name) getOrElse
      JEdit_Lib.buffer_lock(buffer) {
        PIDE.resources.check_thy(node_name, JEdit_Lib.buffer_reader(buffer), strict = false)
      }
  }

  /* perspective */

  // owned by GUI thread
  private var _node_required = false
  def node_required: Boolean = _node_required
  def set_node_required(b: Boolean) { GUI_Thread.require { _node_required = b } }

  def document_view_iterator: Iterator[Document_View] =
    for {
      text_area <- JEdit_Lib.jedit_text_areas(buffer)
      doc_view <- Document_View.get(text_area)
    } yield doc_view

  override def document_view_ranges(snapshot: Document.Snapshot): List[Text.Range] =
  {
    GUI_Thread.require {}

    (for {
      doc_view <- document_view_iterator
      range <- doc_view.perspective(snapshot).ranges.iterator
    } yield range).toList
  }

  /* blob */

  // owned by GUI thread
  private var _blob: Option[(Bytes, String, Symbol.Text_Chunk)] = None

  private def reset_blob(): Unit = GUI_Thread.require { _blob = None }

  def get_blob: Option[Document.Blob] =
    GUI_Thread.require {
      if (is_theory) None
      else {
        val (bytes, text, chunk) =
          _blob match {
            case Some(x) => x
            case None =>
              val bytes = PIDE.resources.make_file_content(buffer)
              val text = buffer.getText(0, buffer.getLength)
              val chunk = Symbol.Text_Chunk(text)
              val x = (bytes, text, chunk)
              _blob = Some(x)
              x
          }
        val changed = pending_edits.nonEmpty
        Some(Document.Blob(bytes, text, chunk, changed))
      }
    }

  /* bibtex entries */

  // owned by GUI thread
  private var _bibtex_entries: Option[List[Text.Info[String]]] = None

  private def reset_bibtex_entries(): Unit = GUI_Thread.require { _bibtex_entries = None }

  def bibtex_entries: List[Text.Info[String]] =
    GUI_Thread.require {
      if (Bibtex.is_bibtex(node_name.node)) {
        _bibtex_entries match {
          case Some(entries) => entries
          case None =>
            val text = JEdit_Lib.buffer_text(buffer)
            val entries =
              try { Bibtex.entries(text) }
              catch { case ERROR(msg) => Output.warning(msg); Nil }
            _bibtex_entries = Some(entries)
            entries
        }
      }
      else Nil
    }

  /* pending edits */

  private object pending_edits
  {
    private val pending = new mutable.ListBuffer[Text.Edit]
    private var last_perspective = Document.Node.no_perspective_text

    def nonEmpty: Boolean = synchronized { pending.nonEmpty }
    def get_edits: List[Text.Edit] = synchronized { pending.toList }
    def get_last_perspective: Document.Node.Perspective_Text = synchronized { last_perspective }
    def set_last_perspective(perspective: Document.Node.Perspective_Text): Unit =
      synchronized { last_perspective = perspective }

    def flush_edits(doc_blobs: Document.Blobs, hidden: Boolean): List[Document.Edit_Text] =
      synchronized {
        GUI_Thread.require {}

        val edits = get_edits
        val (reparse, perspective) = node_perspective(doc_blobs, hidden)
        if (reparse || edits.nonEmpty || last_perspective != perspective) {
          pending.clear
          last_perspective = perspective
          node_edits(node_header(), edits, perspective)
        }
        else Nil
      }

    def edit(edits: List[Text.Edit]): Unit = synchronized
    {
      GUI_Thread.require {}

      reset_blob()
      reset_bibtex_entries()

      for (doc_view <- document_view_iterator)
        doc_view.rich_text_area.active_reset()

      pending ++= edits
      PIDE.editor.invoke()
    }
  }

  def is_stable: Boolean = !pending_edits.nonEmpty
  def snapshot(): Document.Snapshot = session.snapshot(node_name, pending_edits.get_edits)

  def flush_edits(doc_blobs: Document.Blobs, hidden: Boolean): List[Document.Edit_Text] =
    pending_edits.flush_edits(doc_blobs, hidden)

  /* buffer listener */

  private val buffer_listener: BufferListener = new BufferAdapter
  {
    override def contentInserted(buffer: JEditBuffer,
      start_line: Int, offset: Int, num_lines: Int, length: Int)
    {
      pending_edits.edit(List(Text.Edit.insert(offset, buffer.getText(offset, length))))
    }

    override def preContentRemoved(buffer: JEditBuffer,
      start_line: Int, offset: Int, num_lines: Int, removed_length: Int)
    {
      pending_edits.edit(List(Text.Edit.remove(offset, buffer.getText(offset, removed_length))))
    }
  }

  /* syntax */

  def syntax_changed()
  {
    JEdit_Lib.buffer_line_manager(buffer).setFirstInvalidLineContext(0)
    for (text_area <- JEdit_Lib.jedit_text_areas(buffer))
      Untyped.method(Class.forName("org.gjt.sp.jedit.textarea.TextArea"), "foldStructureChanged").
        invoke(text_area)
    buffer.invalidateCachedFoldLevels()
  }

  def init_token_marker()
  {
    Isabelle.buffer_token_marker(buffer) match {
      case Some(marker) if marker != buffer.getTokenMarker =>
        buffer.setTokenMarker(marker)
        syntax_changed()
      case _ =>
    }
  }

  /* init */

  def init(old_model: Option[File_Model]): Buffer_Model =
  {
    GUI_Thread.require {}

    old_model match {
      case None =>
        pending_edits.edit(List(Text.Edit.insert(0, JEdit_Lib.buffer_text(buffer))))
      case Some(file_model) =>
        set_node_required(file_model.node_required)
        pending_edits.set_last_perspective(file_model.last_perspective)
        pending_edits.edit(
          file_model.pending_edits :::
            Text.Edit.replace(0, file_model.content.text, JEdit_Lib.buffer_text(buffer)))
    }

    buffer.addBufferListener(buffer_listener)
    init_token_marker()

    this
  }

  /* exit */

  def exit(): File_Model =
  {
    GUI_Thread.require {}

    buffer.removeBufferListener(buffer_listener)
    init_token_marker()

    File_Model.init(session, node_name, JEdit_Lib.buffer_text(buffer), node_required,
      pending_edits.get_last_perspective, pending_edits.get_edits)
  }
}

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