author | wenzelm |
Fri, 27 Mar 2020 22:01:27 +0100 | |
changeset 71601 | 97ccf48c2f0c |
parent 69493 | 6fa742b03107 |
child 71733 | 6c470c918aad |
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 |
|
800b1ce96fce
more general support for Isabelle/PIDE file formats -- less hardwired Bibtex operations;
wenzelm
parents:
diff
changeset
|
4 |
Support for user-defined file formats. |
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 |
|
b05c0bb47f6d
support for File_Format.Session, e.g. server process accessible via prover options;
wenzelm
parents:
69277
diff
changeset
|
15 |
/* environment */ |
b05c0bb47f6d
support for File_Format.Session, e.g. server process accessible via prover options;
wenzelm
parents:
69277
diff
changeset
|
16 |
|
69255
800b1ce96fce
more general support for Isabelle/PIDE file formats -- less hardwired Bibtex operations;
wenzelm
parents:
diff
changeset
|
17 |
def environment(): Environment = |
69277
258bef08b31e
support for user-defined Isabelle/Scala command-line tools;
wenzelm
parents:
69259
diff
changeset
|
18 |
new Environment(Isabelle_System.init_classes[File_Format]("ISABELLE_FILE_FORMATS")) |
69255
800b1ce96fce
more general support for Isabelle/PIDE file formats -- less hardwired Bibtex operations;
wenzelm
parents:
diff
changeset
|
19 |
|
800b1ce96fce
more general support for Isabelle/PIDE file formats -- less hardwired Bibtex operations;
wenzelm
parents:
diff
changeset
|
20 |
final class Environment private [File_Format](file_formats: List[File_Format]) |
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 = |
b05c0bb47f6d
support for File_Format.Session, e.g. server process accessible via prover options;
wenzelm
parents:
69277
diff
changeset
|
42 |
(options /: agents)({ case (opts, agent) => agent.prover_options(opts) }) |
b05c0bb47f6d
support for File_Format.Session, e.g. server process accessible via prover options;
wenzelm
parents:
69277
diff
changeset
|
43 |
|
b05c0bb47f6d
support for File_Format.Session, e.g. server process accessible via prover options;
wenzelm
parents:
69277
diff
changeset
|
44 |
def stop_session { agents.foreach(_.stop) } |
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 |
b05c0bb47f6d
support for File_Format.Session, e.g. server process accessible via prover options;
wenzelm
parents:
69277
diff
changeset
|
50 |
def stop {} |
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 |
|
800b1ce96fce
more general support for Isabelle/PIDE file formats -- less hardwired Bibtex operations;
wenzelm
parents:
diff
changeset
|
56 |
trait File_Format |
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 |
71601 | 59 |
override def toString: String = 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 { |
|
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 |
} |
|
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 { |
|
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 |
} |
|
69255
800b1ce96fce
more general support for Isabelle/PIDE file formats -- less hardwired Bibtex operations;
wenzelm
parents:
diff
changeset
|
90 |
|
800b1ce96fce
more general support for Isabelle/PIDE file formats -- less hardwired Bibtex operations;
wenzelm
parents:
diff
changeset
|
91 |
def make_preview(snapshot: Document.Snapshot): Option[Present.Preview] = None |
69488
b05c0bb47f6d
support for File_Format.Session, e.g. server process accessible via prover options;
wenzelm
parents:
69277
diff
changeset
|
92 |
|
b05c0bb47f6d
support for File_Format.Session, e.g. server process accessible via prover options;
wenzelm
parents:
69277
diff
changeset
|
93 |
|
69489 | 94 |
/* PIDE session agent */ |
69488
b05c0bb47f6d
support for File_Format.Session, e.g. server process accessible via prover options;
wenzelm
parents:
69277
diff
changeset
|
95 |
|
69493 | 96 |
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
|
97 |
} |