src/Pure/PIDE/document_editor.scala

tuned proofs;

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

Central resources and configuration for interactive document preparation.
*/

package isabelle


import scala.collection.immutable.SortedSet


object Document_Editor {
  /* document output */

  def document_name: String = "document"
  def document_output_dir(): Path = Path.explode("$ISABELLE_HOME_USER/document_output")
  def document_output(name: String): Path = document_output_dir() + Path.basic(name)

  object Meta_Info {
    def read(name: String = document_name): Option[Meta_Info] = {
      val json_path = document_output(name).json
      if (json_path.is_file) {
        val json = JSON.parse(File.read(json_path))
        for {
          selection <- JSON.list(json, "selection", JSON.Value.String.unapply)
          sources <- JSON.string(json, "sources")
          log <- JSON.string(json, "log")
          pdf <- JSON.string(json, "pdf")
        } yield {
          Meta_Info(name,
            SortedSet.from(selection),
            SHA1.fake_digest(sources),
            SHA1.fake_digest(log),
            SHA1.fake_digest(pdf))
        }
      }
      else None
    }

    def write(
      selection: SortedSet[String],
      doc: Document_Build.Document_Output,
      name: String = document_name
    ): Unit = {
      val json =
        JSON.Object(
          "selection" -> selection.toList,
          "sources" -> doc.sources.toString,
          "log" -> SHA1.digest(doc.log).toString,
          "pdf" -> SHA1.digest(doc.pdf).toString)
      File.write(document_output(name).json, JSON.Format.pretty_print(json))
    }
  }

  sealed case class Meta_Info(
    name: String,
    selection: SortedSet[String],
    sources: SHA1.Digest,
    log: SHA1.Digest,
    pdf: SHA1.Digest
  ) {
    def check_files(): Boolean = {
      val path = document_output(name)
      path.log.is_file &&
      path.pdf.is_file &&
      log == SHA1.digest(File.read(path.log)) &&
      pdf == SHA1.digest(path.pdf)
    }
  }

  def write_document(
    selection: SortedSet[String],
    doc: Document_Build.Document_Output,
    name: String = document_name
  ): Unit = {
    val output = document_output(name)
    File.write(output.log, doc.log)
    Bytes.write(output.pdf, doc.pdf)
    Meta_Info.write(selection, doc, name = name)
  }

  def view_document(name: String = document_name): Unit = {
    val path = document_output(name).pdf
    if (path.is_file) Isabelle_System.pdf_viewer(path)
  }


  /* configuration state */

  sealed case class Session(
    background: Option[Sessions.Background],
    selection: SortedSet[String],
    snapshot: Option[Document.Snapshot]
  ) {
    def is_vacuous: Boolean = background.isEmpty
    def is_pending: Boolean = snapshot.isEmpty
    def is_ready: Boolean = background.isDefined && snapshot.isDefined

    def get_background: Sessions.Background = background.get
    def get_variant: Document_Build.Document_Variant = get_background.info.documents.head
    def get_snapshot: Document.Snapshot = snapshot.get
  }

  sealed case class State(
    session_background: Option[Sessions.Background] = None,
    selection: SortedSet[String] = SortedSet.empty,
    views: Set[AnyRef] = Set.empty,
  ) {
    def is_active: Boolean = session_background.isDefined && views.nonEmpty

    def all_document_theories: List[Document.Node.Name] =
      session_background match {
        case Some(background) => background.base.all_document_theories
        case None => Nil
      }

    def active_document_theories: List[Document.Node.Name] =
      if (is_active) all_document_theories else Nil

    def select(
      theories: Iterable[String],
      set: Boolean = false,
      toggle: Boolean = false
    ): State = {
      copy(selection =
        theories.foldLeft(selection) {
          case (sel, theory) =>
            val b = if (toggle) !selection(theory) else set
            if (b) sel + theory else sel - theory
        })
    }

    def register_view(id: AnyRef): State = copy(views = views + id)
    def unregister_view(id: AnyRef): State = copy(views = views - id)

    def session(pide_session: isabelle.Session): Session = {
      val background = session_background.filter(_.info.documents.nonEmpty)
      val snapshot =
        if (background.isEmpty) None
        else {
          val snapshot = pide_session.snapshot()
          def document_ready(theory: String): Boolean =
            pide_session.resources.session_base.loaded_theory(theory) ||
            snapshot.theory_consolidated(theory)
          if (snapshot.is_outdated || !selection.forall(document_ready)) None
          else Some(snapshot)
        }
      Session(background, selection, snapshot)
    }
  }


  /* build */

  def build(
    session_context: Export.Session_Context,
    document_session: Document_Editor.Session,
    progress: Progress
  ): Unit = {
    val session_background = document_session.get_background
    val context =
      Document_Build.context(session_context,
        document_session = Some(session_background.base),
        document_selection = document_session.selection,
        progress = progress)

    Isabelle_System.make_directory(document_output_dir())
    Isabelle_System.with_tmp_dir("document") { tmp_dir =>
      val engine = context.get_engine()
      val variant = document_session.get_variant
      val directory = engine.prepare_directory(context, tmp_dir, variant, verbose = true)
      val ok =
        Meta_Info.read() match {
          case Some(meta_info) =>
            meta_info.check_files() && meta_info.sources == directory.sources
          case None => false
        }
      if (!ok) {
        write_document(document_session.selection,
          engine.build_document(context, directory, verbose = true))
      }
    }
  }
}