--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/PIDE/resources.scala Tue Mar 18 17:39:03 2014 +0100
@@ -0,0 +1,111 @@
+/* Title: Pure/PIDE/resources.scala
+ Author: Makarius
+
+Resources for theories and auxiliary files.
+*/
+
+package isabelle
+
+
+import scala.annotation.tailrec
+
+import java.io.{File => JFile}
+
+
+object Resources
+{
+ /* paths */
+
+ def thy_path(path: Path): Path = path.ext("thy")
+
+ def is_wellformed_thy_path(str: String): Boolean =
+ try { thy_path(Path.explode(str)); true }
+ catch { case ERROR(_) => false }
+}
+
+
+class Resources(val loaded_theories: Set[String] = Set.empty, val base_syntax: Outer_Syntax)
+{
+ /* document node names */
+
+ def node_name(raw_path: Path): Document.Node.Name =
+ {
+ val path = raw_path.expand
+ val node = path.implode
+ val theory = Thy_Header.thy_name(node).getOrElse("")
+ val master_dir = if (theory == "") "" else path.dir.implode
+ Document.Node.Name(node, master_dir, theory)
+ }
+
+
+ /* file-system operations */
+
+ def append(dir: String, source_path: Path): String =
+ (Path.explode(dir) + source_path).expand.implode
+
+ def with_thy_text[A](name: Document.Node.Name, f: CharSequence => A): A =
+ {
+ val path = Path.explode(name.node)
+ if (!path.is_file) error("No such file: " + path.toString)
+
+ val text = File.read(path)
+ Symbol.decode_strict(text)
+ f(text)
+ }
+
+
+ /* theory files */
+
+ def body_files_test(syntax: Outer_Syntax, text: String): Boolean =
+ syntax.thy_load_commands.exists({ case (cmd, _) => text.containsSlice(cmd) })
+
+ def body_files(syntax: Outer_Syntax, text: String): List[String] =
+ {
+ val spans = Thy_Syntax.parse_spans(syntax.scan(text))
+ spans.iterator.map(Thy_Syntax.span_files(syntax, _)).flatten.toList
+ }
+
+ def import_name(master: Document.Node.Name, s: String): Document.Node.Name =
+ {
+ val theory = Thy_Header.base_name(s)
+ if (loaded_theories(theory)) Document.Node.Name(theory + ".thy", "", theory)
+ else {
+ val path = Path.explode(s)
+ val node = append(master.master_dir, Resources.thy_path(path))
+ val master_dir = append(master.master_dir, path.dir)
+ Document.Node.Name(node, master_dir, theory)
+ }
+ }
+
+ def check_thy_text(name: Document.Node.Name, text: CharSequence): Document.Node.Header =
+ {
+ try {
+ val header = Thy_Header.read(text)
+
+ val name1 = header.name
+ if (name.theory != name1)
+ error("Bad file name " + Resources.thy_path(Path.basic(name.theory)) +
+ " for theory " + quote(name1))
+
+ val imports = header.imports.map(import_name(name, _))
+ Document.Node.Header(imports, header.keywords, Nil)
+ }
+ catch { case exn: Throwable => Document.Node.bad_header(Exn.message(exn)) }
+ }
+
+ def check_thy(name: Document.Node.Name): Document.Node.Header =
+ with_thy_text(name, check_thy_text(name, _))
+
+
+ /* theory text edits */
+
+ def text_edits(
+ reparse_limit: Int,
+ previous: Document.Version,
+ doc_blobs: Document.Blobs,
+ edits: List[Document.Edit_Text]): (Boolean, List[Document.Edit_Command], Document.Version) =
+ Thy_Syntax.text_edits(this, reparse_limit, previous, doc_blobs, edits)
+
+ def syntax_changed() { }
+}
+