1/*  Title:      Pure/Thy/file_format.scala
2    Author:     Makarius
3
4Support for user-defined file formats.
5*/
6
7package isabelle
8
9
10object File_Format
11{
12  sealed case class Theory_Context(name: Document.Node.Name, content: String)
13
14
15  /* environment */
16
17  def environment(): Environment =
18    new Environment(Isabelle_System.init_classes[File_Format]("ISABELLE_FILE_FORMATS"))
19
20  final class Environment private [File_Format](file_formats: List[File_Format])
21  {
22    override def toString: String = file_formats.mkString("File_Format.Environment(", ",", ")")
23
24    def get(name: String): Option[File_Format] = file_formats.find(_.detect(name))
25    def get(name: Document.Node.Name): Option[File_Format] = get(name.node)
26    def get_theory(name: Document.Node.Name): Option[File_Format] = get(name.theory)
27    def is_theory(name: Document.Node.Name): Boolean = get_theory(name).isDefined
28
29    def start_session(session: isabelle.Session): Session =
30      new Session(file_formats.map(_.start(session)).filterNot(_ == No_Agent))
31  }
32
33
34  /* session */
35
36  final class Session private[File_Format](agents: List[Agent])
37  {
38    override def toString: String =
39      agents.mkString("File_Format.Session(", ", ", ")")
40
41    def prover_options(options: Options): Options =
42      (options /: agents)({ case (opts, agent) => agent.prover_options(opts) })
43
44    def stop_session { agents.foreach(_.stop) }
45  }
46
47  trait Agent
48  {
49    def prover_options(options: Options): Options = options
50    def stop {}
51  }
52
53  object No_Agent extends Agent
54}
55
56trait File_Format
57{
58  def format_name: String
59  override def toString = format_name
60
61  def file_ext: String
62  def detect(name: String): Boolean = name.endsWith("." + file_ext)
63
64
65  /* implicit theory context: name and content */
66
67  def theory_suffix: String = ""
68  def theory_content(name: String): String = ""
69
70  def make_theory_name(resources: Resources, name: Document.Node.Name): Option[Document.Node.Name] =
71  {
72    for {
73      (_, ext_name) <- Thy_Header.split_file_name(name.node)
74      if detect(ext_name) && theory_suffix.nonEmpty
75    }
76    yield {
77      val thy_node = resources.append(name.node, Path.explode(theory_suffix))
78      Document.Node.Name(thy_node, name.master_dir, ext_name)
79    }
80  }
81
82  def make_theory_content(resources: Resources, thy_name: Document.Node.Name): Option[String] =
83  {
84    for {
85      (prefix, suffix) <- Thy_Header.split_file_name(thy_name.node) if suffix == theory_suffix
86      (_, ext_name) <- Thy_Header.split_file_name(prefix) if detect(ext_name)
87      s <- proper_string(theory_content(ext_name))
88    } yield s
89  }
90
91  def make_preview(snapshot: Document.Snapshot): Option[Present.Preview] = None
92
93
94  /* PIDE session agent */
95
96  def start(session: isabelle.Session): File_Format.Agent = File_Format.No_Agent
97}
98