src/Pure/Thy/file_format.scala
changeset 75393 87ebf5a50283
parent 73367 77ef8bef0593
child 75941 4bbbbaa656f1
equal deleted inserted replaced
75388:b3ca4a6ed74b 75393:87ebf5a50283
     5 */
     5 */
     6 
     6 
     7 package isabelle
     7 package isabelle
     8 
     8 
     9 
     9 
    10 object File_Format
    10 object File_Format {
    11 {
       
    12   sealed case class Theory_Context(name: Document.Node.Name, content: String)
    11   sealed case class Theory_Context(name: Document.Node.Name, content: String)
    13 
    12 
    14 
    13 
    15   /* registry */
    14   /* registry */
    16 
    15 
    17   lazy val registry: Registry =
    16   lazy val registry: Registry =
    18     new Registry(Isabelle_System.make_services(classOf[File_Format]))
    17     new Registry(Isabelle_System.make_services(classOf[File_Format]))
    19 
    18 
    20   final class Registry private [File_Format](file_formats: List[File_Format])
    19   final class Registry private [File_Format](file_formats: List[File_Format]) {
    21   {
       
    22     override def toString: String = file_formats.mkString("File_Format.Environment(", ",", ")")
    20     override def toString: String = file_formats.mkString("File_Format.Environment(", ",", ")")
    23 
    21 
    24     def get(name: String): Option[File_Format] = file_formats.find(_.detect(name))
    22     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)
    23     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)
    24     def get_theory(name: Document.Node.Name): Option[File_Format] = get(name.theory)
    31   }
    29   }
    32 
    30 
    33 
    31 
    34   /* session */
    32   /* session */
    35 
    33 
    36   final class Session private[File_Format](agents: List[Agent])
    34   final class Session private[File_Format](agents: List[Agent]) {
    37   {
       
    38     override def toString: String =
    35     override def toString: String =
    39       agents.mkString("File_Format.Session(", ", ", ")")
    36       agents.mkString("File_Format.Session(", ", ", ")")
    40 
    37 
    41     def prover_options(options: Options): Options =
    38     def prover_options(options: Options): Options =
    42       agents.foldLeft(options) { case (opts, agent) => agent.prover_options(opts) }
    39       agents.foldLeft(options) { case (opts, agent) => agent.prover_options(opts) }
    43 
    40 
    44     def stop_session: Unit = agents.foreach(_.stop())
    41     def stop_session: Unit = agents.foreach(_.stop())
    45   }
    42   }
    46 
    43 
    47   trait Agent
    44   trait Agent {
    48   {
       
    49     def prover_options(options: Options): Options = options
    45     def prover_options(options: Options): Options = options
    50     def stop(): Unit = {}
    46     def stop(): Unit = {}
    51   }
    47   }
    52 
    48 
    53   object No_Agent extends Agent
    49   object No_Agent extends Agent
    54 }
    50 }
    55 
    51 
    56 abstract class File_Format extends Isabelle_System.Service
    52 abstract class File_Format extends Isabelle_System.Service {
    57 {
       
    58   def format_name: String
    53   def format_name: String
    59   override def toString: String = "File_Format(" + format_name + ")"
    54   override def toString: String = "File_Format(" + format_name + ")"
    60 
    55 
    61   def file_ext: String
    56   def file_ext: String
    62   def detect(name: String): Boolean = name.endsWith("." + file_ext)
    57   def detect(name: String): Boolean = name.endsWith("." + file_ext)
    65   /* implicit theory context: name and content */
    60   /* implicit theory context: name and content */
    66 
    61 
    67   def theory_suffix: String = ""
    62   def theory_suffix: String = ""
    68   def theory_content(name: String): String = ""
    63   def theory_content(name: String): String = ""
    69 
    64 
    70   def make_theory_name(resources: Resources, name: Document.Node.Name): Option[Document.Node.Name] =
    65   def make_theory_name(
    71   {
    66     resources: Resources,
       
    67     name: Document.Node.Name
       
    68   ): Option[Document.Node.Name] = {
    72     for {
    69     for {
    73       (_, thy) <- Thy_Header.split_file_name(name.node)
    70       (_, thy) <- Thy_Header.split_file_name(name.node)
    74       if detect(name.node) && theory_suffix.nonEmpty
    71       if detect(name.node) && theory_suffix.nonEmpty
    75     }
    72     }
    76     yield {
    73     yield {
    77       val thy_node = resources.append(name.node, Path.explode(theory_suffix))
    74       val thy_node = resources.append(name.node, Path.explode(theory_suffix))
    78       Document.Node.Name(thy_node, name.master_dir, thy)
    75       Document.Node.Name(thy_node, name.master_dir, thy)
    79     }
    76     }
    80   }
    77   }
    81 
    78 
    82   def make_theory_content(resources: Resources, thy_name: Document.Node.Name): Option[String] =
    79   def make_theory_content(resources: Resources, thy_name: Document.Node.Name): Option[String] = {
    83   {
       
    84     for {
    80     for {
    85       (prefix, suffix) <- Thy_Header.split_file_name(thy_name.node)
    81       (prefix, suffix) <- Thy_Header.split_file_name(thy_name.node)
    86       if detect(prefix) && suffix == theory_suffix
    82       if detect(prefix) && suffix == theory_suffix
    87       (_, thy) <- Thy_Header.split_file_name(prefix)
    83       (_, thy) <- Thy_Header.split_file_name(prefix)
    88       s <- proper_string(theory_content(thy))
    84       s <- proper_string(theory_content(thy))