author | wenzelm |
Sun, 14 Nov 2021 15:42:38 +0100 | |
changeset 74783 | 47f565849e71 |
parent 73367 | 77ef8bef0593 |
child 75393 | 87ebf5a50283 |
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 |
|
800b1ce96fce
more general support for Isabelle/PIDE file formats -- less hardwired Bibtex operations;
wenzelm
parents:
diff
changeset
|
10 |
object File_Format |
800b1ce96fce
more general support for Isabelle/PIDE file formats -- less hardwired Bibtex operations;
wenzelm
parents:
diff
changeset
|
11 |
{ |
69488
b05c0bb47f6d
support for File_Format.Session, e.g. server process accessible via prover options;
wenzelm
parents:
69277
diff
changeset
|
12 |
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
|
13 |
|
b05c0bb47f6d
support for File_Format.Session, e.g. server process accessible via prover options;
wenzelm
parents:
69277
diff
changeset
|
14 |
|
71733 | 15 |
/* registry */ |
69488
b05c0bb47f6d
support for File_Format.Session, e.g. server process accessible via prover options;
wenzelm
parents:
69277
diff
changeset
|
16 |
|
71733 | 17 |
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
|
18 |
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
|
19 |
|
71733 | 20 |
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
|
21 |
{ |
800b1ce96fce
more general support for Isabelle/PIDE file formats -- less hardwired Bibtex operations;
wenzelm
parents:
diff
changeset
|
22 |
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
|
23 |
|
800b1ce96fce
more general support for Isabelle/PIDE file formats -- less hardwired Bibtex operations;
wenzelm
parents:
diff
changeset
|
24 |
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
|
25 |
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
|
26 |
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
|
27 |
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
|
28 |
|
b05c0bb47f6d
support for File_Format.Session, e.g. server process accessible via prover options;
wenzelm
parents:
69277
diff
changeset
|
29 |
def start_session(session: isabelle.Session): Session = |
69493 | 30 |
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
|
31 |
} |
800b1ce96fce
more general support for Isabelle/PIDE file formats -- less hardwired Bibtex operations;
wenzelm
parents:
diff
changeset
|
32 |
|
69488
b05c0bb47f6d
support for File_Format.Session, e.g. server process accessible via prover options;
wenzelm
parents:
69277
diff
changeset
|
33 |
|
b05c0bb47f6d
support for File_Format.Session, e.g. server process accessible via prover options;
wenzelm
parents:
69277
diff
changeset
|
34 |
/* session */ |
b05c0bb47f6d
support for File_Format.Session, e.g. server process accessible via prover options;
wenzelm
parents:
69277
diff
changeset
|
35 |
|
b05c0bb47f6d
support for File_Format.Session, e.g. server process accessible via prover options;
wenzelm
parents:
69277
diff
changeset
|
36 |
final class Session private[File_Format](agents: List[Agent]) |
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 |
override def toString: String = |
b05c0bb47f6d
support for File_Format.Session, e.g. server process accessible via prover options;
wenzelm
parents:
69277
diff
changeset
|
39 |
agents.mkString("File_Format.Session(", ", ", ")") |
b05c0bb47f6d
support for File_Format.Session, e.g. server process accessible via prover options;
wenzelm
parents:
69277
diff
changeset
|
40 |
|
b05c0bb47f6d
support for File_Format.Session, e.g. server process accessible via prover options;
wenzelm
parents:
69277
diff
changeset
|
41 |
def prover_options(options: Options): Options = |
73359 | 42 |
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
|
43 |
|
73367 | 44 |
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
|
45 |
} |
b05c0bb47f6d
support for File_Format.Session, e.g. server process accessible via prover options;
wenzelm
parents:
69277
diff
changeset
|
46 |
|
b05c0bb47f6d
support for File_Format.Session, e.g. server process accessible via prover options;
wenzelm
parents:
69277
diff
changeset
|
47 |
trait Agent |
b05c0bb47f6d
support for File_Format.Session, e.g. server process accessible via prover options;
wenzelm
parents:
69277
diff
changeset
|
48 |
{ |
b05c0bb47f6d
support for File_Format.Session, e.g. server process accessible via prover options;
wenzelm
parents:
69277
diff
changeset
|
49 |
def prover_options(options: Options): Options = options |
73367 | 50 |
def stop(): Unit = {} |
69488
b05c0bb47f6d
support for File_Format.Session, e.g. server process accessible via prover options;
wenzelm
parents:
69277
diff
changeset
|
51 |
} |
b05c0bb47f6d
support for File_Format.Session, e.g. server process accessible via prover options;
wenzelm
parents:
69277
diff
changeset
|
52 |
|
69493 | 53 |
object No_Agent extends Agent |
69255
800b1ce96fce
more general support for Isabelle/PIDE file formats -- less hardwired Bibtex operations;
wenzelm
parents:
diff
changeset
|
54 |
} |
800b1ce96fce
more general support for Isabelle/PIDE file formats -- less hardwired Bibtex operations;
wenzelm
parents:
diff
changeset
|
55 |
|
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
|
56 |
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
|
57 |
{ |
800b1ce96fce
more general support for Isabelle/PIDE file formats -- less hardwired Bibtex operations;
wenzelm
parents:
diff
changeset
|
58 |
def format_name: String |
71738 | 59 |
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
|
60 |
|
69257 | 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 = "" |
|
69259 | 68 |
def theory_content(name: String): String = "" |
69255
800b1ce96fce
more general support for Isabelle/PIDE file formats -- less hardwired Bibtex operations;
wenzelm
parents:
diff
changeset
|
69 |
|
69257 | 70 |
def make_theory_name(resources: Resources, name: Document.Node.Name): Option[Document.Node.Name] = |
71 |
{ |
|
72 |
for { |
|
72839
a597300290de
clarified File_Format.detect: needs to operate on full node name;
wenzelm
parents:
72652
diff
changeset
|
73 |
(_, 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
|
74 |
if detect(name.node) && theory_suffix.nonEmpty |
69257 | 75 |
} |
76 |
yield { |
|
77 |
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
|
78 |
Document.Node.Name(thy_node, name.master_dir, thy) |
69257 | 79 |
} |
80 |
} |
|
69255
800b1ce96fce
more general support for Isabelle/PIDE file formats -- less hardwired Bibtex operations;
wenzelm
parents:
diff
changeset
|
81 |
|
69257 | 82 |
def make_theory_content(resources: Resources, thy_name: Document.Node.Name): Option[String] = |
83 |
{ |
|
84 |
for { |
|
72839
a597300290de
clarified File_Format.detect: needs to operate on full node name;
wenzelm
parents:
72652
diff
changeset
|
85 |
(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
|
86 |
if detect(prefix) && suffix == theory_suffix |
a597300290de
clarified File_Format.detect: needs to operate on full node name;
wenzelm
parents:
72652
diff
changeset
|
87 |
(_, thy) <- Thy_Header.split_file_name(prefix) |
a597300290de
clarified File_Format.detect: needs to operate on full node name;
wenzelm
parents:
72652
diff
changeset
|
88 |
s <- proper_string(theory_content(thy)) |
69257 | 89 |
} yield s |
90 |
} |
|
69255
800b1ce96fce
more general support for Isabelle/PIDE file formats -- less hardwired Bibtex operations;
wenzelm
parents:
diff
changeset
|
91 |
|
72957 | 92 |
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
|
93 |
|
b05c0bb47f6d
support for File_Format.Session, e.g. server process accessible via prover options;
wenzelm
parents:
69277
diff
changeset
|
94 |
|
69489 | 95 |
/* PIDE session agent */ |
69488
b05c0bb47f6d
support for File_Format.Session, e.g. server process accessible via prover options;
wenzelm
parents:
69277
diff
changeset
|
96 |
|
69493 | 97 |
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
|
98 |
} |