author | wenzelm |
Tue, 04 Apr 2017 19:40:47 +0200 | |
changeset 65372 | b722ee40c26c |
parent 65368 | 7fb5aad28f38 |
child 65373 | 905ed0102c69 |
permissions | -rw-r--r-- |
56208 | 1 |
/* Title: Pure/PIDE/resources.scala |
43651
511df47bcadc
some support for theory files within Isabelle/Scala session;
wenzelm
parents:
diff
changeset
|
2 |
Author: Makarius |
511df47bcadc
some support for theory files within Isabelle/Scala session;
wenzelm
parents:
diff
changeset
|
3 |
|
56208 | 4 |
Resources for theories and auxiliary files. |
43651
511df47bcadc
some support for theory files within Isabelle/Scala session;
wenzelm
parents:
diff
changeset
|
5 |
*/ |
511df47bcadc
some support for theory files within Isabelle/Scala session;
wenzelm
parents:
diff
changeset
|
6 |
|
511df47bcadc
some support for theory files within Isabelle/Scala session;
wenzelm
parents:
diff
changeset
|
7 |
package isabelle |
511df47bcadc
some support for theory files within Isabelle/Scala session;
wenzelm
parents:
diff
changeset
|
8 |
|
44953 | 9 |
|
48885 | 10 |
import scala.annotation.tailrec |
56823
37be55461dbe
more frugal access to theory text via Reader, reduced costs for I/O text decoding;
wenzelm
parents:
56801
diff
changeset
|
11 |
import scala.util.parsing.input.Reader |
48885 | 12 |
|
48409 | 13 |
import java.io.{File => JFile} |
44953 | 14 |
|
15 |
||
65359 | 16 |
class Resources( |
17 |
val session_name: String, |
|
65361 | 18 |
val session_base: Sessions.Base, |
65359 | 19 |
val log: Logger = No_Logger) |
43651
511df47bcadc
some support for theory files within Isabelle/Scala session;
wenzelm
parents:
diff
changeset
|
20 |
{ |
64839 | 21 |
val thy_info = new Thy_Info(this) |
22 |
||
65250 | 23 |
def thy_path(path: Path): Path = path.ext("thy") |
24 |
||
64839 | 25 |
|
44953 | 26 |
/* file-system operations */ |
27 |
||
28 |
def append(dir: String, source_path: Path): String = |
|
48711
8d381fdef898
need to expand path in order to resolve imports like "~~/src/Tools/Code_Generator";
wenzelm
parents:
48710
diff
changeset
|
29 |
(Path.explode(dir) + source_path).expand.implode |
44953 | 30 |
|
64654 | 31 |
def append_file(dir: String, raw_name: String): String = |
32 |
if (Path.is_valid(raw_name)) append(dir, Path.explode(raw_name)) |
|
33 |
else raw_name |
|
34 |
||
35 |
||
46737 | 36 |
|
64657 | 37 |
/* source files of Isabelle/ML bootstrap */ |
38 |
||
39 |
def source_file(raw_name: String): Option[String] = |
|
40 |
{ |
|
41 |
if (Path.is_wellformed(raw_name)) { |
|
42 |
if (Path.is_valid(raw_name)) { |
|
43 |
def check(p: Path): Option[Path] = if (p.is_file) Some(p) else None |
|
44 |
||
45 |
val path = Path.explode(raw_name) |
|
46 |
val path1 = |
|
47 |
if (path.is_absolute || path.is_current) check(path) |
|
48 |
else { |
|
49 |
check(Path.explode("~~/src/Pure") + path) orElse |
|
50 |
(if (Isabelle_System.getenv("ML_SOURCES") == "") None |
|
51 |
else check(Path.explode("$ML_SOURCES") + path)) |
|
52 |
} |
|
53 |
Some(File.platform_path(path1 getOrElse path)) |
|
54 |
} |
|
55 |
else None |
|
56 |
} |
|
57 |
else Some(raw_name) |
|
58 |
} |
|
59 |
||
60 |
||
46737 | 61 |
/* theory files */ |
62 |
||
63584
68751fe1c036
tuned signature -- prover-independence is presently theoretical;
wenzelm
parents:
63579
diff
changeset
|
63 |
def loaded_files(syntax: Outer_Syntax, text: String): List[String] = |
56393
22f533e6a049
more abstract Prover.Syntax, as proposed by Carst Tankink;
wenzelm
parents:
56392
diff
changeset
|
64 |
if (syntax.load_commands_in(text)) { |
57906 | 65 |
val spans = syntax.parse_spans(text) |
59689
7968c57ea240
simplified Command.resolve_files in ML, using blobs_index from Scala;
wenzelm
parents:
59683
diff
changeset
|
66 |
spans.iterator.map(Command.span_files(syntax, _)._1).flatten.toList |
56392 | 67 |
} |
68 |
else Nil |
|
48885 | 69 |
|
65372
b722ee40c26c
refer to global_theories from all sessions, before selection;
wenzelm
parents:
65368
diff
changeset
|
70 |
def qualify(name: String): String = |
b722ee40c26c
refer to global_theories from all sessions, before selection;
wenzelm
parents:
65368
diff
changeset
|
71 |
if (Long_Name.is_qualified(name)) error("Bad qualified theory name " + quote(name)) |
b722ee40c26c
refer to global_theories from all sessions, before selection;
wenzelm
parents:
65368
diff
changeset
|
72 |
else if (session_base.global_theories.contains(name)) name |
b722ee40c26c
refer to global_theories from all sessions, before selection;
wenzelm
parents:
65368
diff
changeset
|
73 |
else Long_Name.qualify(session_name, name) |
b722ee40c26c
refer to global_theories from all sessions, before selection;
wenzelm
parents:
65368
diff
changeset
|
74 |
|
b722ee40c26c
refer to global_theories from all sessions, before selection;
wenzelm
parents:
65368
diff
changeset
|
75 |
def init_name(raw_path: Path): Document.Node.Name = |
65359 | 76 |
{ |
77 |
val path = raw_path.expand |
|
78 |
val node = path.implode |
|
65372
b722ee40c26c
refer to global_theories from all sessions, before selection;
wenzelm
parents:
65368
diff
changeset
|
79 |
val theory = qualify(Thy_Header.thy_name(node).getOrElse("")) |
65359 | 80 |
val master_dir = if (theory == "") "" else path.dir.implode |
81 |
Document.Node.Name(node, master_dir, theory) |
|
82 |
} |
|
83 |
||
84 |
def import_name(master: Document.Node.Name, s: String): Document.Node.Name = |
|
51634
553953ad8165
more general Thy_Load.import_name, e.g. relevant for Isabelle/eclipse -- NB: Thy_Load serves as main hub for funny overriding to adapt to provers and editors;
wenzelm
parents:
51293
diff
changeset
|
85 |
{ |
65362 | 86 |
val theory = Thy_Header.base_name(s) |
65368
7fb5aad28f38
back to more liberal imports (amending 908a27a4b9c9): tolerate mixed situations like "GCD" vs. "~~/src/HOL/GCD";
wenzelm
parents:
65362
diff
changeset
|
87 |
val is_qualified = Thy_Header.is_base_name(s) && Long_Name.is_qualified(s) |
65362 | 88 |
|
89 |
val known_theory = |
|
65368
7fb5aad28f38
back to more liberal imports (amending 908a27a4b9c9): tolerate mixed situations like "GCD" vs. "~~/src/HOL/GCD";
wenzelm
parents:
65362
diff
changeset
|
90 |
session_base.known_theories.get(theory) orElse |
7fb5aad28f38
back to more liberal imports (amending 908a27a4b9c9): tolerate mixed situations like "GCD" vs. "~~/src/HOL/GCD";
wenzelm
parents:
65362
diff
changeset
|
91 |
(if (is_qualified) session_base.known_theories.get(Long_Name.base_name(theory)) |
7fb5aad28f38
back to more liberal imports (amending 908a27a4b9c9): tolerate mixed situations like "GCD" vs. "~~/src/HOL/GCD";
wenzelm
parents:
65362
diff
changeset
|
92 |
else session_base.known_theories.get(Long_Name.qualify(session_name, theory))) |
65362 | 93 |
|
94 |
known_theory match { |
|
65361 | 95 |
case Some(name) if session_base.loaded_theory(name) => Document.Node.Name.theory(name.theory) |
56801
8dd9df88f647
some support for session-qualified theories: allow to refer to resources via qualified name instead of odd file-system path;
wenzelm
parents:
56393
diff
changeset
|
96 |
case Some(name) => name |
65362 | 97 |
case None if is_qualified => Document.Node.Name.theory(theory) |
56801
8dd9df88f647
some support for session-qualified theories: allow to refer to resources via qualified name instead of odd file-system path;
wenzelm
parents:
56393
diff
changeset
|
98 |
case None => |
8dd9df88f647
some support for session-qualified theories: allow to refer to resources via qualified name instead of odd file-system path;
wenzelm
parents:
56393
diff
changeset
|
99 |
val path = Path.explode(s) |
65362 | 100 |
val node = append(master.master_dir, thy_path(path)) |
101 |
val master_dir = append(master.master_dir, path.dir) |
|
102 |
Document.Node.Name(node, master_dir, Long_Name.qualify(session_name, theory)) |
|
51634
553953ad8165
more general Thy_Load.import_name, e.g. relevant for Isabelle/eclipse -- NB: Thy_Load serves as main hub for funny overriding to adapt to provers and editors;
wenzelm
parents:
51293
diff
changeset
|
103 |
} |
553953ad8165
more general Thy_Load.import_name, e.g. relevant for Isabelle/eclipse -- NB: Thy_Load serves as main hub for funny overriding to adapt to provers and editors;
wenzelm
parents:
51293
diff
changeset
|
104 |
} |
553953ad8165
more general Thy_Load.import_name, e.g. relevant for Isabelle/eclipse -- NB: Thy_Load serves as main hub for funny overriding to adapt to provers and editors;
wenzelm
parents:
51293
diff
changeset
|
105 |
|
64656 | 106 |
def with_thy_reader[A](name: Document.Node.Name, f: Reader[Char] => A): A = |
107 |
{ |
|
108 |
val path = Path.explode(name.node) |
|
109 |
if (!path.is_file) error("No such file: " + path.toString) |
|
110 |
||
111 |
val reader = Scan.byte_reader(path.file) |
|
112 |
try { f(reader) } finally { reader.close } |
|
113 |
} |
|
114 |
||
65359 | 115 |
def check_thy_reader(node_name: Document.Node.Name, reader: Reader[Char], |
116 |
start: Token.Pos = Token.Pos.command, strict: Boolean = true): Document.Node.Header = |
|
46737 | 117 |
{ |
64826
c97296294f6d
clarified check_thy_reader: check node_name here;
wenzelm
parents:
64825
diff
changeset
|
118 |
if (node_name.is_theory && reader.source.length > 0) { |
57615
df1b3452d71c
more explicit discrimination of empty nodes -- suppress from Theories panel;
wenzelm
parents:
56913
diff
changeset
|
119 |
try { |
64825 | 120 |
val header = Thy_Header.read(reader, start, strict).decode_symbols |
48885 | 121 |
|
59694 | 122 |
val base_name = Long_Name.base_name(node_name.theory) |
123 |
val (name, pos) = header.name |
|
124 |
if (base_name != name) |
|
59718 | 125 |
error("Bad theory name " + quote(name) + |
65250 | 126 |
" for file " + thy_path(Path.basic(base_name)) + Position.here(pos) + |
59718 | 127 |
Completion.report_names(pos, 1, List((base_name, ("theory", base_name))))) |
48885 | 128 |
|
59694 | 129 |
val imports = |
65359 | 130 |
header.imports.map({ case (s, pos) => (import_name(node_name, s), pos) }) |
63579 | 131 |
Document.Node.Header(imports, header.keywords, header.abbrevs) |
57615
df1b3452d71c
more explicit discrimination of empty nodes -- suppress from Theories panel;
wenzelm
parents:
56913
diff
changeset
|
132 |
} |
df1b3452d71c
more explicit discrimination of empty nodes -- suppress from Theories panel;
wenzelm
parents:
56913
diff
changeset
|
133 |
catch { case exn: Throwable => Document.Node.bad_header(Exn.message(exn)) } |
50414
e17a1f179bb0
explore theory_body_files via future, for improved performance;
wenzelm
parents:
50291
diff
changeset
|
134 |
} |
57615
df1b3452d71c
more explicit discrimination of empty nodes -- suppress from Theories panel;
wenzelm
parents:
56913
diff
changeset
|
135 |
else Document.Node.no_header |
46737 | 136 |
} |
46748
8f3ae4d04a2d
refined node_header -- more direct buffer access (again);
wenzelm
parents:
46737
diff
changeset
|
137 |
|
65359 | 138 |
def check_thy(name: Document.Node.Name, start: Token.Pos = Token.Pos.command, |
139 |
strict: Boolean = true): Document.Node.Header = |
|
140 |
with_thy_reader(name, check_thy_reader(name, _, start, strict)) |
|
50566
b43c4f660320
tuned signature: use thy_load to adapt to prover/editor specific view on sources;
wenzelm
parents:
50415
diff
changeset
|
141 |
|
b43c4f660320
tuned signature: use thy_load to adapt to prover/editor specific view on sources;
wenzelm
parents:
50415
diff
changeset
|
142 |
|
64673
b5965890e54d
more uniform treatment of file name vs. theory name and special header;
wenzelm
parents:
64657
diff
changeset
|
143 |
/* special header */ |
b5965890e54d
more uniform treatment of file name vs. theory name and special header;
wenzelm
parents:
64657
diff
changeset
|
144 |
|
b5965890e54d
more uniform treatment of file name vs. theory name and special header;
wenzelm
parents:
64657
diff
changeset
|
145 |
def special_header(name: Document.Node.Name): Option[Document.Node.Header] = |
b5965890e54d
more uniform treatment of file name vs. theory name and special header;
wenzelm
parents:
64657
diff
changeset
|
146 |
if (Thy_Header.is_ml_root(name.theory)) |
65359 | 147 |
Some(Document.Node.Header(List((import_name(name, Thy_Header.ML_BOOTSTRAP), Position.none)))) |
64673
b5965890e54d
more uniform treatment of file name vs. theory name and special header;
wenzelm
parents:
64657
diff
changeset
|
148 |
else if (Thy_Header.is_bootstrap(name.theory)) |
65359 | 149 |
Some(Document.Node.Header(List((import_name(name, Thy_Header.PURE), Position.none)))) |
64673
b5965890e54d
more uniform treatment of file name vs. theory name and special header;
wenzelm
parents:
64657
diff
changeset
|
150 |
else None |
b5965890e54d
more uniform treatment of file name vs. theory name and special header;
wenzelm
parents:
64657
diff
changeset
|
151 |
|
b5965890e54d
more uniform treatment of file name vs. theory name and special header;
wenzelm
parents:
64657
diff
changeset
|
152 |
|
64797 | 153 |
/* blobs */ |
154 |
||
155 |
def undefined_blobs(nodes: Document.Nodes): List[Document.Node.Name] = |
|
156 |
(for { |
|
157 |
(node_name, node) <- nodes.iterator |
|
65361 | 158 |
if !session_base.loaded_theory(node_name) |
64797 | 159 |
cmd <- node.load_commands.iterator |
160 |
name <- cmd.blobs_undefined.iterator |
|
161 |
} yield name).toList |
|
162 |
||
163 |
||
56316
b1cf8ddc2e04
propagate deps_changed, to resolve missing files without requiring jEdit events (e.g. buffer load/save);
wenzelm
parents:
56315
diff
changeset
|
164 |
/* document changes */ |
50566
b43c4f660320
tuned signature: use thy_load to adapt to prover/editor specific view on sources;
wenzelm
parents:
50415
diff
changeset
|
165 |
|
56316
b1cf8ddc2e04
propagate deps_changed, to resolve missing files without requiring jEdit events (e.g. buffer load/save);
wenzelm
parents:
56315
diff
changeset
|
166 |
def parse_change( |
56315 | 167 |
reparse_limit: Int, |
168 |
previous: Document.Version, |
|
169 |
doc_blobs: Document.Blobs, |
|
170 |
edits: List[Document.Edit_Text]): Session.Change = |
|
56316
b1cf8ddc2e04
propagate deps_changed, to resolve missing files without requiring jEdit events (e.g. buffer load/save);
wenzelm
parents:
56315
diff
changeset
|
171 |
Thy_Syntax.parse_change(this, reparse_limit, previous, doc_blobs, edits) |
55134
1b67b17cdad5
propagate update of outer syntax keywords: global propertiesChanged, buffer TokenMarker.markTokens, text area repainting;
wenzelm
parents:
54521
diff
changeset
|
172 |
|
56316
b1cf8ddc2e04
propagate deps_changed, to resolve missing files without requiring jEdit events (e.g. buffer load/save);
wenzelm
parents:
56315
diff
changeset
|
173 |
def commit(change: Session.Change) { } |
43651
511df47bcadc
some support for theory files within Isabelle/Scala session;
wenzelm
parents:
diff
changeset
|
174 |
} |