src/Pure/Thy/file_format.scala

clarified signature: uniform master_dir instead of separate field;

/*  Title:      Pure/Thy/file_format.scala
    Author:     Makarius

Support for user-defined file formats, associated with active session.
*/

package isabelle


object File_Format {
  object No_Data extends AnyRef {
    override def toString: String = "File_Format.No_Data"
  }

  sealed case class Theory_Context(name: Document.Node.Name, content: String)


  /* registry */

  lazy val registry: Registry =
    new Registry(Isabelle_System.make_services(classOf[File_Format]))

  final class Registry private [File_Format](file_formats: List[File_Format]) {
    override def toString: String = file_formats.mkString("File_Format.Environment(", ",", ")")

    def get(name: String): Option[File_Format] = file_formats.find(_.detect(name))
    def get(name: Document.Node.Name): Option[File_Format] = get(name.node)
    def get_theory(name: Document.Node.Name): Option[File_Format] = get(name.theory)
    def is_theory(name: Document.Node.Name): Boolean = get_theory(name).isDefined

    def theory_excluded(name: String): Boolean = file_formats.exists(_.theory_excluded(name))

    def parse_data(name: String, text: String): AnyRef =
      get(name) match {
        case Some(file_format) => file_format.parse_data(name, text)
        case None => No_Data
      }
    def parse_data(name: Document.Node.Name, text: String): AnyRef = parse_data(name.node, text)

    def start_session(session: isabelle.Session): Session =
      new Session(file_formats.map(_.start(session)).filterNot(_ == No_Agent))
  }


  /* session */

  final class Session private[File_Format](agents: List[Agent]) {
    override def toString: String =
      agents.mkString("File_Format.Session(", ", ", ")")

    def prover_options(options: Options): Options =
      agents.foldLeft(options) { case (opts, agent) => agent.prover_options(opts) }

    def stop_session(): Unit = agents.foreach(_.stop())
  }

  trait Agent {
    def prover_options(options: Options): Options = options
    def stop(): Unit = {}
  }

  object No_Agent extends Agent
}

abstract class File_Format extends Isabelle_System.Service {
  def format_name: String
  override def toString: String = "File_Format(" + format_name + ")"

  def file_ext: String
  def detect(name: String): Boolean = name.endsWith("." + file_ext)

  def parse_data(name: String, text: String): AnyRef = File_Format.No_Data


  /* implicit theory context: name and content */

  def theory_suffix: String = ""
  def theory_content(name: String): String = ""
  def theory_excluded(name: String): Boolean = false

  def make_theory_name(
    resources: Resources,
    name: Document.Node.Name
  ): Option[Document.Node.Name] = {
    for {
      theory <- Url.get_base_name(name.node)
      if detect(name.node) && theory_suffix.nonEmpty
    }
    yield {
      val node = resources.append_path(name.node, Path.explode(theory_suffix))
      Document.Node.Name(node, theory = theory)
    }
  }

  def make_theory_content(resources: Resources, thy_name: Document.Node.Name): Option[String] = {
    for {
      prefix <- Url.strip_base_name(thy_name.node)
      suffix <- Url.get_base_name(thy_name.node)
      if detect(prefix) && suffix == theory_suffix
      thy <- Url.get_base_name(prefix)
      s <- proper_string(theory_content(thy))
    } yield s
  }

  def html_document(snapshot: Document.Snapshot): Option[Browser_Info.HTML_Document] = None


  /* PIDE session agent */

  def start(session: isabelle.Session): File_Format.Agent = File_Format.No_Agent
}