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