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)) |