author | wenzelm |
Thu, 12 Mar 2015 16:47:47 +0100 | |
changeset 59683 | d6824d8490be |
parent 57917 | 8ce97e5d545f |
child 59689 | 7968c57ea240 |
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 |
||
56208 | 16 |
object Resources |
48422
9613780a805b
determine source dependencies, relatively to preloaded theories;
wenzelm
parents:
48409
diff
changeset
|
17 |
{ |
9613780a805b
determine source dependencies, relatively to preloaded theories;
wenzelm
parents:
48409
diff
changeset
|
18 |
def thy_path(path: Path): Path = path.ext("thy") |
9613780a805b
determine source dependencies, relatively to preloaded theories;
wenzelm
parents:
48409
diff
changeset
|
19 |
} |
44953 | 20 |
|
48422
9613780a805b
determine source dependencies, relatively to preloaded theories;
wenzelm
parents:
48409
diff
changeset
|
21 |
|
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
|
22 |
class Resources( |
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
|
23 |
val loaded_theories: Set[String], |
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
|
24 |
val known_theories: Map[String, Document.Node.Name], |
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
|
25 |
val base_syntax: Prover.Syntax) |
43651
511df47bcadc
some support for theory files within Isabelle/Scala session;
wenzelm
parents:
diff
changeset
|
26 |
{ |
54514 | 27 |
/* document node names */ |
28 |
||
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
|
29 |
def node_name(qualifier: String, raw_path: Path): Document.Node.Name = |
54514 | 30 |
{ |
56913
df4cd6e1fdfa
no qualifier for now, to avoid confusion concerning loaded_theories in PIDE interaction;
wenzelm
parents:
56823
diff
changeset
|
31 |
val no_qualifier = "" // FIXME |
54514 | 32 |
val path = raw_path.expand |
33 |
val node = path.implode |
|
56913
df4cd6e1fdfa
no qualifier for now, to avoid confusion concerning loaded_theories in PIDE interaction;
wenzelm
parents:
56823
diff
changeset
|
34 |
val theory = Long_Name.qualify(no_qualifier, Thy_Header.thy_name(node).getOrElse("")) |
54515 | 35 |
val master_dir = if (theory == "") "" else path.dir.implode |
36 |
Document.Node.Name(node, master_dir, theory) |
|
54514 | 37 |
} |
38 |
||
39 |
||
44953 | 40 |
/* file-system operations */ |
41 |
||
42 |
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
|
43 |
(Path.explode(dir) + source_path).expand.implode |
44953 | 44 |
|
56823
37be55461dbe
more frugal access to theory text via Reader, reduced costs for I/O text decoding;
wenzelm
parents:
56801
diff
changeset
|
45 |
def with_thy_reader[A](name: Document.Node.Name, f: Reader[Char] => A): A = |
48885 | 46 |
{ |
47 |
val path = Path.explode(name.node) |
|
48 |
if (!path.is_file) error("No such file: " + path.toString) |
|
50291
674893679352
prefer Symbol.decode_strict in batch mode, to avoid files with spurious Unicode symbols that clash with Isabelle symbol interpretation;
wenzelm
parents:
50204
diff
changeset
|
49 |
|
56823
37be55461dbe
more frugal access to theory text via Reader, reduced costs for I/O text decoding;
wenzelm
parents:
56801
diff
changeset
|
50 |
val reader = Scan.byte_reader(path.file) |
37be55461dbe
more frugal access to theory text via Reader, reduced costs for I/O text decoding;
wenzelm
parents:
56801
diff
changeset
|
51 |
try { f(reader) } finally { reader.close } |
48885 | 52 |
} |
53 |
||
46737 | 54 |
|
55 |
/* theory files */ |
|
56 |
||
56393
22f533e6a049
more abstract Prover.Syntax, as proposed by Carst Tankink;
wenzelm
parents:
56392
diff
changeset
|
57 |
def loaded_files(syntax: Prover.Syntax, text: String): List[String] = |
22f533e6a049
more abstract Prover.Syntax, as proposed by Carst Tankink;
wenzelm
parents:
56392
diff
changeset
|
58 |
if (syntax.load_commands_in(text)) { |
57906 | 59 |
val spans = syntax.parse_spans(text) |
59683 | 60 |
spans.iterator.map(Command_Span.span_files(syntax, _)._1).flatten.toList |
56392 | 61 |
} |
62 |
else Nil |
|
48885 | 63 |
|
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
|
64 |
private def dummy_name(theory: String): Document.Node.Name = |
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
|
65 |
Document.Node.Name(theory + ".thy", "", theory) |
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
|
66 |
|
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
|
67 |
def import_name(qualifier: String, 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
|
68 |
{ |
56913
df4cd6e1fdfa
no qualifier for now, to avoid confusion concerning loaded_theories in PIDE interaction;
wenzelm
parents:
56823
diff
changeset
|
69 |
val no_qualifier = "" // FIXME |
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
|
70 |
val thy1 = Thy_Header.base_name(s) |
56913
df4cd6e1fdfa
no qualifier for now, to avoid confusion concerning loaded_theories in PIDE interaction;
wenzelm
parents:
56823
diff
changeset
|
71 |
val thy2 = if (Long_Name.is_qualified(thy1)) thy1 else Long_Name.qualify(no_qualifier, thy1) |
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
|
72 |
(known_theories.get(thy1) orElse |
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
|
73 |
known_theories.get(thy2) orElse |
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
|
74 |
known_theories.get(Long_Name.base_name(thy1))) match { |
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
|
75 |
case Some(name) if loaded_theories(name.theory) => dummy_name(name.theory) |
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
|
76 |
case Some(name) => name |
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
|
77 |
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
|
78 |
val path = Path.explode(s) |
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
|
79 |
val theory = path.base.implode |
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
|
80 |
if (Long_Name.is_qualified(theory)) dummy_name(theory) |
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
|
81 |
else { |
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
|
82 |
val node = append(master.master_dir, Resources.thy_path(path)) |
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
|
83 |
val master_dir = append(master.master_dir, path.dir) |
56913
df4cd6e1fdfa
no qualifier for now, to avoid confusion concerning loaded_theories in PIDE interaction;
wenzelm
parents:
56823
diff
changeset
|
84 |
Document.Node.Name(node, master_dir, Long_Name.qualify(no_qualifier, 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
|
85 |
} |
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
|
86 |
} |
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
|
87 |
} |
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
|
88 |
|
56823
37be55461dbe
more frugal access to theory text via Reader, reduced costs for I/O text decoding;
wenzelm
parents:
56801
diff
changeset
|
89 |
def check_thy_reader(qualifier: String, name: Document.Node.Name, reader: Reader[Char]) |
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
|
90 |
: Document.Node.Header = |
46737 | 91 |
{ |
57615
df1b3452d71c
more explicit discrimination of empty nodes -- suppress from Theories panel;
wenzelm
parents:
56913
diff
changeset
|
92 |
if (reader.source.length > 0) { |
df1b3452d71c
more explicit discrimination of empty nodes -- suppress from Theories panel;
wenzelm
parents:
56913
diff
changeset
|
93 |
try { |
df1b3452d71c
more explicit discrimination of empty nodes -- suppress from Theories panel;
wenzelm
parents:
56913
diff
changeset
|
94 |
val header = Thy_Header.read(reader).decode_symbols |
48885 | 95 |
|
57615
df1b3452d71c
more explicit discrimination of empty nodes -- suppress from Theories panel;
wenzelm
parents:
56913
diff
changeset
|
96 |
val base_name = Long_Name.base_name(name.theory) |
df1b3452d71c
more explicit discrimination of empty nodes -- suppress from Theories panel;
wenzelm
parents:
56913
diff
changeset
|
97 |
val name1 = header.name |
df1b3452d71c
more explicit discrimination of empty nodes -- suppress from Theories panel;
wenzelm
parents:
56913
diff
changeset
|
98 |
if (base_name != name1) |
df1b3452d71c
more explicit discrimination of empty nodes -- suppress from Theories panel;
wenzelm
parents:
56913
diff
changeset
|
99 |
error("Bad file name " + Resources.thy_path(Path.basic(base_name)) + |
df1b3452d71c
more explicit discrimination of empty nodes -- suppress from Theories panel;
wenzelm
parents:
56913
diff
changeset
|
100 |
" for theory " + quote(name1)) |
48885 | 101 |
|
57615
df1b3452d71c
more explicit discrimination of empty nodes -- suppress from Theories panel;
wenzelm
parents:
56913
diff
changeset
|
102 |
val imports = header.imports.map(import_name(qualifier, name, _)) |
df1b3452d71c
more explicit discrimination of empty nodes -- suppress from Theories panel;
wenzelm
parents:
56913
diff
changeset
|
103 |
Document.Node.Header(imports, header.keywords, Nil) |
df1b3452d71c
more explicit discrimination of empty nodes -- suppress from Theories panel;
wenzelm
parents:
56913
diff
changeset
|
104 |
} |
df1b3452d71c
more explicit discrimination of empty nodes -- suppress from Theories panel;
wenzelm
parents:
56913
diff
changeset
|
105 |
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
|
106 |
} |
57615
df1b3452d71c
more explicit discrimination of empty nodes -- suppress from Theories panel;
wenzelm
parents:
56913
diff
changeset
|
107 |
else Document.Node.no_header |
46737 | 108 |
} |
46748
8f3ae4d04a2d
refined node_header -- more direct buffer access (again);
wenzelm
parents:
46737
diff
changeset
|
109 |
|
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
|
110 |
def check_thy(qualifier: String, name: Document.Node.Name): Document.Node.Header = |
56823
37be55461dbe
more frugal access to theory text via Reader, reduced costs for I/O text decoding;
wenzelm
parents:
56801
diff
changeset
|
111 |
with_thy_reader(name, check_thy_reader(qualifier, name, _)) |
50566
b43c4f660320
tuned signature: use thy_load to adapt to prover/editor specific view on sources;
wenzelm
parents:
50415
diff
changeset
|
112 |
|
b43c4f660320
tuned signature: use thy_load to adapt to prover/editor specific view on sources;
wenzelm
parents:
50415
diff
changeset
|
113 |
|
56316
b1cf8ddc2e04
propagate deps_changed, to resolve missing files without requiring jEdit events (e.g. buffer load/save);
wenzelm
parents:
56315
diff
changeset
|
114 |
/* document changes */ |
50566
b43c4f660320
tuned signature: use thy_load to adapt to prover/editor specific view on sources;
wenzelm
parents:
50415
diff
changeset
|
115 |
|
56316
b1cf8ddc2e04
propagate deps_changed, to resolve missing files without requiring jEdit events (e.g. buffer load/save);
wenzelm
parents:
56315
diff
changeset
|
116 |
def parse_change( |
56315 | 117 |
reparse_limit: Int, |
118 |
previous: Document.Version, |
|
119 |
doc_blobs: Document.Blobs, |
|
120 |
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
|
121 |
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
|
122 |
|
56316
b1cf8ddc2e04
propagate deps_changed, to resolve missing files without requiring jEdit events (e.g. buffer load/save);
wenzelm
parents:
56315
diff
changeset
|
123 |
def commit(change: Session.Change) { } |
56387 | 124 |
|
125 |
||
126 |
/* prover process */ |
|
127 |
||
128 |
def start_prover(receiver: Prover.Message => Unit, name: String, args: List[String]): Prover = |
|
57917 | 129 |
Isabelle_Process(receiver, args) |
43651
511df47bcadc
some support for theory files within Isabelle/Scala session;
wenzelm
parents:
diff
changeset
|
130 |
} |
511df47bcadc
some support for theory files within Isabelle/Scala session;
wenzelm
parents:
diff
changeset
|
131 |