author | wenzelm |
Sun, 21 Aug 2022 11:48:14 +0200 | |
changeset 75939 | 87f0adcb7e10 |
parent 75393 | 87ebf5a50283 |
child 75941 | 4bbbbaa656f1 |
permissions | -rw-r--r-- |
69255
800b1ce96fce
more general support for Isabelle/PIDE file formats -- less hardwired Bibtex operations;
wenzelm
parents:
diff
changeset
|
1 |
/* Title: Pure/Thy/file_format.scala |
800b1ce96fce
more general support for Isabelle/PIDE file formats -- less hardwired Bibtex operations;
wenzelm
parents:
diff
changeset
|
2 |
Author: Makarius |
800b1ce96fce
more general support for Isabelle/PIDE file formats -- less hardwired Bibtex operations;
wenzelm
parents:
diff
changeset
|
3 |
|
73130 | 4 |
Support for user-defined file formats, associated with active session. |
69255
800b1ce96fce
more general support for Isabelle/PIDE file formats -- less hardwired Bibtex operations;
wenzelm
parents:
diff
changeset
|
5 |
*/ |
800b1ce96fce
more general support for Isabelle/PIDE file formats -- less hardwired Bibtex operations;
wenzelm
parents:
diff
changeset
|
6 |
|
800b1ce96fce
more general support for Isabelle/PIDE file formats -- less hardwired Bibtex operations;
wenzelm
parents:
diff
changeset
|
7 |
package isabelle |
800b1ce96fce
more general support for Isabelle/PIDE file formats -- less hardwired Bibtex operations;
wenzelm
parents:
diff
changeset
|
8 |
|
800b1ce96fce
more general support for Isabelle/PIDE file formats -- less hardwired Bibtex operations;
wenzelm
parents:
diff
changeset
|
9 |
|
75393 | 10 |
object File_Format { |
69488
b05c0bb47f6d
support for File_Format.Session, e.g. server process accessible via prover options;
wenzelm
parents:
69277
diff
changeset
|
11 |
sealed case class Theory_Context(name: Document.Node.Name, content: String) |
b05c0bb47f6d
support for File_Format.Session, e.g. server process accessible via prover options;
wenzelm
parents:
69277
diff
changeset
|
12 |
|
b05c0bb47f6d
support for File_Format.Session, e.g. server process accessible via prover options;
wenzelm
parents:
69277
diff
changeset
|
13 |
|
71733 | 14 |
/* registry */ |
69488
b05c0bb47f6d
support for File_Format.Session, e.g. server process accessible via prover options;
wenzelm
parents:
69277
diff
changeset
|
15 |
|
71733 | 16 |
lazy val registry: Registry = |
72159
40b5ee5889d2
clarified management of services: static declarations vs. dynamic instances (e.g. relevant for stateful Session.Protocol_Handler, notably Scala.Handler and session "System");
wenzelm
parents:
71738
diff
changeset
|
17 |
new Registry(Isabelle_System.make_services(classOf[File_Format])) |
69255
800b1ce96fce
more general support for Isabelle/PIDE file formats -- less hardwired Bibtex operations;
wenzelm
parents:
diff
changeset
|
18 |
|
75393 | 19 |
final class Registry private [File_Format](file_formats: List[File_Format]) { |
69255
800b1ce96fce
more general support for Isabelle/PIDE file formats -- less hardwired Bibtex operations;
wenzelm
parents:
diff
changeset
|
20 |
override def toString: String = file_formats.mkString("File_Format.Environment(", ",", ")") |
800b1ce96fce
more general support for Isabelle/PIDE file formats -- less hardwired Bibtex operations;
wenzelm
parents:
diff
changeset
|
21 |
|
800b1ce96fce
more general support for Isabelle/PIDE file formats -- less hardwired Bibtex operations;
wenzelm
parents:
diff
changeset
|
22 |
def get(name: String): Option[File_Format] = file_formats.find(_.detect(name)) |
800b1ce96fce
more general support for Isabelle/PIDE file formats -- less hardwired Bibtex operations;
wenzelm
parents:
diff
changeset
|
23 |
def get(name: Document.Node.Name): Option[File_Format] = get(name.node) |
800b1ce96fce
more general support for Isabelle/PIDE file formats -- less hardwired Bibtex operations;
wenzelm
parents:
diff
changeset
|
24 |
def get_theory(name: Document.Node.Name): Option[File_Format] = get(name.theory) |
800b1ce96fce
more general support for Isabelle/PIDE file formats -- less hardwired Bibtex operations;
wenzelm
parents:
diff
changeset
|
25 |
def is_theory(name: Document.Node.Name): Boolean = get_theory(name).isDefined |
69488
b05c0bb47f6d
support for File_Format.Session, e.g. server process accessible via prover options;
wenzelm
parents:
69277
diff
changeset
|
26 |
|
b05c0bb47f6d
support for File_Format.Session, e.g. server process accessible via prover options;
wenzelm
parents:
69277
diff
changeset
|
27 |
def start_session(session: isabelle.Session): Session = |
69493 | 28 |
new Session(file_formats.map(_.start(session)).filterNot(_ == No_Agent)) |
69255
800b1ce96fce
more general support for Isabelle/PIDE file formats -- less hardwired Bibtex operations;
wenzelm
parents:
diff
changeset
|
29 |
} |
800b1ce96fce
more general support for Isabelle/PIDE file formats -- less hardwired Bibtex operations;
wenzelm
parents:
diff
changeset
|
30 |
|
69488
b05c0bb47f6d
support for File_Format.Session, e.g. server process accessible via prover options;
wenzelm
parents:
69277
diff
changeset
|
31 |
|
b05c0bb47f6d
support for File_Format.Session, e.g. server process accessible via prover options;
wenzelm
parents:
69277
diff
changeset
|
32 |
/* session */ |
b05c0bb47f6d
support for File_Format.Session, e.g. server process accessible via prover options;
wenzelm
parents:
69277
diff
changeset
|
33 |
|
75393 | 34 |
final class Session private[File_Format](agents: List[Agent]) { |
69488
b05c0bb47f6d
support for File_Format.Session, e.g. server process accessible via prover options;
wenzelm
parents:
69277
diff
changeset
|
35 |
override def toString: String = |
b05c0bb47f6d
support for File_Format.Session, e.g. server process accessible via prover options;
wenzelm
parents:
69277
diff
changeset
|
36 |
agents.mkString("File_Format.Session(", ", ", ")") |
b05c0bb47f6d
support for File_Format.Session, e.g. server process accessible via prover options;
wenzelm
parents:
69277
diff
changeset
|
37 |
|
b05c0bb47f6d
support for File_Format.Session, e.g. server process accessible via prover options;
wenzelm
parents:
69277
diff
changeset
|
38 |
def prover_options(options: Options): Options = |
73359 | 39 |
agents.foldLeft(options) { case (opts, agent) => agent.prover_options(opts) } |
69488
b05c0bb47f6d
support for File_Format.Session, e.g. server process accessible via prover options;
wenzelm
parents:
69277
diff
changeset
|
40 |
|
73367 | 41 |
def stop_session: Unit = agents.foreach(_.stop()) |
69488
b05c0bb47f6d
support for File_Format.Session, e.g. server process accessible via prover options;
wenzelm
parents:
69277
diff
changeset
|
42 |
} |
b05c0bb47f6d
support for File_Format.Session, e.g. server process accessible via prover options;
wenzelm
parents:
69277
diff
changeset
|
43 |
|
75393 | 44 |
trait Agent { |
69488
b05c0bb47f6d
support for File_Format.Session, e.g. server process accessible via prover options;
wenzelm
parents:
69277
diff
changeset
|
45 |
def prover_options(options: Options): Options = options |
73367 | 46 |
def stop(): Unit = {} |
69488
b05c0bb47f6d
support for File_Format.Session, e.g. server process accessible via prover options;
wenzelm
parents:
69277
diff
changeset
|
47 |
} |
b05c0bb47f6d
support for File_Format.Session, e.g. server process accessible via prover options;
wenzelm
parents:
69277
diff
changeset
|
48 |
|
69493 | 49 |
object No_Agent extends Agent |
69255
800b1ce96fce
more general support for Isabelle/PIDE file formats -- less hardwired Bibtex operations;
wenzelm
parents:
diff
changeset
|
50 |
} |
800b1ce96fce
more general support for Isabelle/PIDE file formats -- less hardwired Bibtex operations;
wenzelm
parents:
diff
changeset
|
51 |
|
75393 | 52 |
abstract class File_Format extends Isabelle_System.Service { |
69255
800b1ce96fce
more general support for Isabelle/PIDE file formats -- less hardwired Bibtex operations;
wenzelm
parents:
diff
changeset
|
53 |
def format_name: String |
71738 | 54 |
override def toString: String = "File_Format(" + format_name + ")" |
69255
800b1ce96fce
more general support for Isabelle/PIDE file formats -- less hardwired Bibtex operations;
wenzelm
parents:
diff
changeset
|
55 |
|
69257 | 56 |
def file_ext: String |
57 |
def detect(name: String): Boolean = name.endsWith("." + file_ext) |
|
58 |
||
59 |
||
60 |
/* implicit theory context: name and content */ |
|
61 |
||
62 |
def theory_suffix: String = "" |
|
69259 | 63 |
def theory_content(name: String): String = "" |
69255
800b1ce96fce
more general support for Isabelle/PIDE file formats -- less hardwired Bibtex operations;
wenzelm
parents:
diff
changeset
|
64 |
|
75393 | 65 |
def make_theory_name( |
66 |
resources: Resources, |
|
67 |
name: Document.Node.Name |
|
68 |
): Option[Document.Node.Name] = { |
|
69257 | 69 |
for { |
72839
a597300290de
clarified File_Format.detect: needs to operate on full node name;
wenzelm
parents:
72652
diff
changeset
|
70 |
(_, thy) <- Thy_Header.split_file_name(name.node) |
a597300290de
clarified File_Format.detect: needs to operate on full node name;
wenzelm
parents:
72652
diff
changeset
|
71 |
if detect(name.node) && theory_suffix.nonEmpty |
69257 | 72 |
} |
73 |
yield { |
|
74 |
val thy_node = resources.append(name.node, Path.explode(theory_suffix)) |
|
72839
a597300290de
clarified File_Format.detect: needs to operate on full node name;
wenzelm
parents:
72652
diff
changeset
|
75 |
Document.Node.Name(thy_node, name.master_dir, thy) |
69257 | 76 |
} |
77 |
} |
|
69255
800b1ce96fce
more general support for Isabelle/PIDE file formats -- less hardwired Bibtex operations;
wenzelm
parents:
diff
changeset
|
78 |
|
75393 | 79 |
def make_theory_content(resources: Resources, thy_name: Document.Node.Name): Option[String] = { |
69257 | 80 |
for { |
72839
a597300290de
clarified File_Format.detect: needs to operate on full node name;
wenzelm
parents:
72652
diff
changeset
|
81 |
(prefix, suffix) <- Thy_Header.split_file_name(thy_name.node) |
a597300290de
clarified File_Format.detect: needs to operate on full node name;
wenzelm
parents:
72652
diff
changeset
|
82 |
if detect(prefix) && suffix == theory_suffix |
a597300290de
clarified File_Format.detect: needs to operate on full node name;
wenzelm
parents:
72652
diff
changeset
|
83 |
(_, thy) <- Thy_Header.split_file_name(prefix) |
a597300290de
clarified File_Format.detect: needs to operate on full node name;
wenzelm
parents:
72652
diff
changeset
|
84 |
s <- proper_string(theory_content(thy)) |
69257 | 85 |
} yield s |
86 |
} |
|
69255
800b1ce96fce
more general support for Isabelle/PIDE file formats -- less hardwired Bibtex operations;
wenzelm
parents:
diff
changeset
|
87 |
|
72957 | 88 |
def html_document(snapshot: Document.Snapshot): Option[Presentation.HTML_Document] = None |
69488
b05c0bb47f6d
support for File_Format.Session, e.g. server process accessible via prover options;
wenzelm
parents:
69277
diff
changeset
|
89 |
|
b05c0bb47f6d
support for File_Format.Session, e.g. server process accessible via prover options;
wenzelm
parents:
69277
diff
changeset
|
90 |
|
69489 | 91 |
/* PIDE session agent */ |
69488
b05c0bb47f6d
support for File_Format.Session, e.g. server process accessible via prover options;
wenzelm
parents:
69277
diff
changeset
|
92 |
|
69493 | 93 |
def start(session: isabelle.Session): File_Format.Agent = File_Format.No_Agent |
69255
800b1ce96fce
more general support for Isabelle/PIDE file formats -- less hardwired Bibtex operations;
wenzelm
parents:
diff
changeset
|
94 |
} |