author | wenzelm |
Sat, 10 Nov 2018 14:08:02 +0100 | |
changeset 69277 | 258bef08b31e |
parent 69259 | 438e1a11445f |
child 69488 | b05c0bb47f6d |
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 |
{ |
800b1ce96fce
more general support for Isabelle/PIDE file formats -- less hardwired Bibtex operations;
wenzelm
parents:
diff
changeset
|
12 |
def environment(): Environment = |
69277
258bef08b31e
support for user-defined Isabelle/Scala command-line tools;
wenzelm
parents:
69259
diff
changeset
|
13 |
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
|
14 |
|
800b1ce96fce
more general support for Isabelle/PIDE file formats -- less hardwired Bibtex operations;
wenzelm
parents:
diff
changeset
|
15 |
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
|
16 |
{ |
800b1ce96fce
more general support for Isabelle/PIDE file formats -- less hardwired Bibtex operations;
wenzelm
parents:
diff
changeset
|
17 |
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
|
18 |
|
800b1ce96fce
more general support for Isabelle/PIDE file formats -- less hardwired Bibtex operations;
wenzelm
parents:
diff
changeset
|
19 |
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
|
20 |
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
|
21 |
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
|
22 |
def is_theory(name: Document.Node.Name): Boolean = get_theory(name).isDefined |
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 |
|
800b1ce96fce
more general support for Isabelle/PIDE file formats -- less hardwired Bibtex operations;
wenzelm
parents:
diff
changeset
|
25 |
sealed case class Theory_Context(name: Document.Node.Name, content: String) |
800b1ce96fce
more general support for Isabelle/PIDE file formats -- less hardwired Bibtex operations;
wenzelm
parents:
diff
changeset
|
26 |
} |
800b1ce96fce
more general support for Isabelle/PIDE file formats -- less hardwired Bibtex operations;
wenzelm
parents:
diff
changeset
|
27 |
|
800b1ce96fce
more general support for Isabelle/PIDE file formats -- less hardwired Bibtex operations;
wenzelm
parents:
diff
changeset
|
28 |
trait File_Format |
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 |
def format_name: String |
800b1ce96fce
more general support for Isabelle/PIDE file formats -- less hardwired Bibtex operations;
wenzelm
parents:
diff
changeset
|
31 |
override def toString = format_name |
800b1ce96fce
more general support for Isabelle/PIDE file formats -- less hardwired Bibtex operations;
wenzelm
parents:
diff
changeset
|
32 |
|
69257 | 33 |
def file_ext: String |
34 |
def detect(name: String): Boolean = name.endsWith("." + file_ext) |
|
35 |
||
36 |
||
37 |
/* implicit theory context: name and content */ |
|
38 |
||
39 |
def theory_suffix: String = "" |
|
69259 | 40 |
def theory_content(name: String): String = "" |
69255
800b1ce96fce
more general support for Isabelle/PIDE file formats -- less hardwired Bibtex operations;
wenzelm
parents:
diff
changeset
|
41 |
|
69257 | 42 |
def make_theory_name(resources: Resources, name: Document.Node.Name): Option[Document.Node.Name] = |
43 |
{ |
|
44 |
for { |
|
45 |
(_, ext_name) <- Thy_Header.split_file_name(name.node) |
|
46 |
if detect(ext_name) && theory_suffix.nonEmpty |
|
47 |
} |
|
48 |
yield { |
|
49 |
val thy_node = resources.append(name.node, Path.explode(theory_suffix)) |
|
50 |
Document.Node.Name(thy_node, name.master_dir, ext_name) |
|
51 |
} |
|
52 |
} |
|
69255
800b1ce96fce
more general support for Isabelle/PIDE file formats -- less hardwired Bibtex operations;
wenzelm
parents:
diff
changeset
|
53 |
|
69257 | 54 |
def make_theory_content(resources: Resources, thy_name: Document.Node.Name): Option[String] = |
55 |
{ |
|
56 |
for { |
|
57 |
(prefix, suffix) <- Thy_Header.split_file_name(thy_name.node) if suffix == theory_suffix |
|
58 |
(_, ext_name) <- Thy_Header.split_file_name(prefix) if detect(ext_name) |
|
59 |
s <- proper_string(theory_content(ext_name)) |
|
60 |
} yield s |
|
61 |
} |
|
69255
800b1ce96fce
more general support for Isabelle/PIDE file formats -- less hardwired Bibtex operations;
wenzelm
parents:
diff
changeset
|
62 |
|
800b1ce96fce
more general support for Isabelle/PIDE file formats -- less hardwired Bibtex operations;
wenzelm
parents:
diff
changeset
|
63 |
def make_preview(snapshot: Document.Snapshot): Option[Present.Preview] = None |
800b1ce96fce
more general support for Isabelle/PIDE file formats -- less hardwired Bibtex operations;
wenzelm
parents:
diff
changeset
|
64 |
} |