author | wenzelm |
Sun, 25 Nov 2012 20:31:49 +0100 | |
changeset 50204 | daeb1674fb91 |
parent 48889 | 04deeb14327c |
child 50291 | 674893679352 |
permissions | -rw-r--r-- |
43651
511df47bcadc
some support for theory files within Isabelle/Scala session;
wenzelm
parents:
diff
changeset
|
1 |
/* Title: Pure/Thy/thy_load.scala |
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 |
|
44577
96b6388d06c4
separate module for jEdit primitives for loading theory files;
wenzelm
parents:
44574
diff
changeset
|
4 |
Primitives for loading theory 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 |
11 |
||
48409 | 12 |
import java.io.{File => JFile} |
44953 | 13 |
|
14 |
||
48422
9613780a805b
determine source dependencies, relatively to preloaded theories;
wenzelm
parents:
48409
diff
changeset
|
15 |
object Thy_Load |
9613780a805b
determine source dependencies, relatively to preloaded theories;
wenzelm
parents:
48409
diff
changeset
|
16 |
{ |
50204
daeb1674fb91
tuned signature -- avoid intrusion of module Path in generic PIDE concepts;
wenzelm
parents:
48889
diff
changeset
|
17 |
/* paths */ |
daeb1674fb91
tuned signature -- avoid intrusion of module Path in generic PIDE concepts;
wenzelm
parents:
48889
diff
changeset
|
18 |
|
48422
9613780a805b
determine source dependencies, relatively to preloaded theories;
wenzelm
parents:
48409
diff
changeset
|
19 |
def thy_path(path: Path): Path = path.ext("thy") |
48484 | 20 |
|
21 |
def is_ok(str: String): Boolean = |
|
22 |
try { thy_path(Path.explode(str)); true } |
|
23 |
catch { case ERROR(_) => false } |
|
50204
daeb1674fb91
tuned signature -- avoid intrusion of module Path in generic PIDE concepts;
wenzelm
parents:
48889
diff
changeset
|
24 |
|
daeb1674fb91
tuned signature -- avoid intrusion of module Path in generic PIDE concepts;
wenzelm
parents:
48889
diff
changeset
|
25 |
|
daeb1674fb91
tuned signature -- avoid intrusion of module Path in generic PIDE concepts;
wenzelm
parents:
48889
diff
changeset
|
26 |
/* node names */ |
daeb1674fb91
tuned signature -- avoid intrusion of module Path in generic PIDE concepts;
wenzelm
parents:
48889
diff
changeset
|
27 |
|
daeb1674fb91
tuned signature -- avoid intrusion of module Path in generic PIDE concepts;
wenzelm
parents:
48889
diff
changeset
|
28 |
def external_node(raw_path: Path): Document.Node.Name = |
daeb1674fb91
tuned signature -- avoid intrusion of module Path in generic PIDE concepts;
wenzelm
parents:
48889
diff
changeset
|
29 |
{ |
daeb1674fb91
tuned signature -- avoid intrusion of module Path in generic PIDE concepts;
wenzelm
parents:
48889
diff
changeset
|
30 |
val path = raw_path.expand |
daeb1674fb91
tuned signature -- avoid intrusion of module Path in generic PIDE concepts;
wenzelm
parents:
48889
diff
changeset
|
31 |
val node = path.implode |
daeb1674fb91
tuned signature -- avoid intrusion of module Path in generic PIDE concepts;
wenzelm
parents:
48889
diff
changeset
|
32 |
val dir = path.dir.implode |
daeb1674fb91
tuned signature -- avoid intrusion of module Path in generic PIDE concepts;
wenzelm
parents:
48889
diff
changeset
|
33 |
val theory = Thy_Header.thy_name(node) getOrElse error("Bad theory file name: " + path) |
daeb1674fb91
tuned signature -- avoid intrusion of module Path in generic PIDE concepts;
wenzelm
parents:
48889
diff
changeset
|
34 |
Document.Node.Name(node, dir, theory) |
daeb1674fb91
tuned signature -- avoid intrusion of module Path in generic PIDE concepts;
wenzelm
parents:
48889
diff
changeset
|
35 |
} |
48422
9613780a805b
determine source dependencies, relatively to preloaded theories;
wenzelm
parents:
48409
diff
changeset
|
36 |
} |
44953 | 37 |
|
48422
9613780a805b
determine source dependencies, relatively to preloaded theories;
wenzelm
parents:
48409
diff
changeset
|
38 |
|
48870
4accee106f0f
clarified initialization of Thy_Load, Thy_Info, Session;
wenzelm
parents:
48827
diff
changeset
|
39 |
class Thy_Load(val loaded_theories: Set[String] = Set.empty, val base_syntax: Outer_Syntax) |
43651
511df47bcadc
some support for theory files within Isabelle/Scala session;
wenzelm
parents:
diff
changeset
|
40 |
{ |
44953 | 41 |
/* file-system operations */ |
42 |
||
43 |
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
|
44 |
(Path.explode(dir) + source_path).expand.implode |
44953 | 45 |
|
48885 | 46 |
def with_thy_text[A](name: Document.Node.Name, f: CharSequence => A): A = |
47 |
{ |
|
48 |
val path = Path.explode(name.node) |
|
49 |
if (!path.is_file) error("No such file: " + path.toString) |
|
50 |
f(File.read(path)) |
|
51 |
} |
|
52 |
||
46737 | 53 |
|
54 |
/* theory files */ |
|
55 |
||
56 |
private def import_name(dir: String, s: String): Document.Node.Name = |
|
57 |
{ |
|
58 |
val theory = Thy_Header.base_name(s) |
|
48870
4accee106f0f
clarified initialization of Thy_Load, Thy_Info, Session;
wenzelm
parents:
48827
diff
changeset
|
59 |
if (loaded_theories(theory)) Document.Node.Name(theory, "", theory) |
46737 | 60 |
else { |
61 |
val path = Path.explode(s) |
|
48422
9613780a805b
determine source dependencies, relatively to preloaded theories;
wenzelm
parents:
48409
diff
changeset
|
62 |
val node = append(dir, Thy_Load.thy_path(path)) |
46737 | 63 |
val dir1 = append(dir, path.dir) |
64 |
Document.Node.Name(node, dir1, theory) |
|
65 |
} |
|
66 |
} |
|
67 |
||
48885 | 68 |
private def find_file(tokens: List[Token]): Option[String] = |
69 |
{ |
|
70 |
def clean(toks: List[Token]): List[Token] = |
|
71 |
toks match { |
|
72 |
case t :: _ :: ts if t.is_keyword && (t.source == "%" || t.source == "--") => clean(ts) |
|
73 |
case t :: ts => t :: clean(ts) |
|
74 |
case Nil => Nil |
|
75 |
} |
|
76 |
val clean_tokens = clean(tokens.filter(_.is_proper)) |
|
77 |
clean_tokens.reverse.find(_.is_name).map(_.content) |
|
78 |
} |
|
79 |
||
80 |
def find_files(syntax: Outer_Syntax, text: String): List[String] = |
|
81 |
{ |
|
82 |
val thy_load_commands = syntax.thy_load_commands |
|
83 |
if (thy_load_commands.exists({ case (cmd, _) => text.containsSlice(cmd) })) { |
|
84 |
val spans = Thy_Syntax.parse_spans(syntax.scan(text)) |
|
85 |
spans.iterator.map({ |
|
86 |
case toks @ (tok :: _) if tok.is_command => |
|
87 |
thy_load_commands.find({ case (cmd, _) => cmd == tok.content }) match { |
|
88 |
case Some((_, exts)) => |
|
89 |
find_file(toks) match { |
|
90 |
case Some(file) => |
|
91 |
if (exts.isEmpty) List(file) |
|
92 |
else exts.map(ext => file + "." + ext) |
|
93 |
case None => Nil |
|
94 |
} |
|
95 |
case None => Nil |
|
96 |
} |
|
97 |
case _ => Nil |
|
98 |
}).flatten.toList |
|
99 |
} |
|
100 |
else Nil |
|
101 |
} |
|
102 |
||
103 |
def check_thy_text(name: Document.Node.Name, text: CharSequence): Document.Node.Header = |
|
46737 | 104 |
{ |
48882
61dc7d5d150a
use Thy_Header.read on explicit text only -- potentially via File.read, not Scan.byte_reader;
wenzelm
parents:
48870
diff
changeset
|
105 |
val header = Thy_Header.read(text) |
48885 | 106 |
|
46737 | 107 |
val name1 = header.name |
108 |
if (name.theory != name1) |
|
48422
9613780a805b
determine source dependencies, relatively to preloaded theories;
wenzelm
parents:
48409
diff
changeset
|
109 |
error("Bad file name " + Thy_Load.thy_path(Path.basic(name.theory)) + |
9613780a805b
determine source dependencies, relatively to preloaded theories;
wenzelm
parents:
48409
diff
changeset
|
110 |
" for theory " + quote(name1)) |
48885 | 111 |
|
112 |
val imports = header.imports.map(import_name(name.dir, _)) |
|
113 |
val uses = header.uses |
|
48707
ba531af91148
simplified Document.Node.Header -- internalized errors;
wenzelm
parents:
48484
diff
changeset
|
114 |
Document.Node.Header(imports, header.keywords, uses) |
46737 | 115 |
} |
46748
8f3ae4d04a2d
refined node_header -- more direct buffer access (again);
wenzelm
parents:
46737
diff
changeset
|
116 |
|
48885 | 117 |
def check_thy(name: Document.Node.Name): Document.Node.Header = |
118 |
with_thy_text(name, check_thy_text(name, _)) |
|
119 |
||
120 |
def check_thy_files(syntax: Outer_Syntax, name: Document.Node.Name): Document.Node.Header = |
|
121 |
with_thy_text(name, text => |
|
122 |
{ |
|
123 |
val string = text.toString |
|
124 |
val header = check_thy_text(name, string) |
|
48889
04deeb14327c
add keywords of this node as well (e.g. relevant for Pure.thy);
wenzelm
parents:
48885
diff
changeset
|
125 |
val more_uses = find_files(syntax.add_keywords(header.keywords), string) |
48885 | 126 |
header.copy(uses = header.uses ::: more_uses.map((_, false))) |
127 |
}) |
|
43651
511df47bcadc
some support for theory files within Isabelle/Scala session;
wenzelm
parents:
diff
changeset
|
128 |
} |
511df47bcadc
some support for theory files within Isabelle/Scala session;
wenzelm
parents:
diff
changeset
|
129 |