--- a/src/Pure/System/session.scala Mon Jul 04 13:43:10 2011 +0200
+++ b/src/Pure/System/session.scala Mon Jul 04 16:27:11 2011 +0200
@@ -2,7 +2,7 @@
Author: Makarius
Options: :folding=explicit:collapseFolds=1:
-Isabelle session, potentially with running prover.
+Main Isabelle/Scala session, potentially with running prover process.
*/
package isabelle
@@ -124,7 +124,7 @@
/** main protocol actor **/
- val thy_header = new Thy_Header(system.symbols)
+ /* global state */
@volatile private var syntax = new Outer_Syntax(system.symbols)
def current_syntax(): Outer_Syntax = syntax
@@ -144,6 +144,28 @@
private val global_state = new Volatile(Document.State.init)
def current_state(): Document.State = global_state.peek()
+
+ /* theory files */
+
+ val thy_header = new Thy_Header(system.symbols)
+
+ val thy_load = new Thy_Load
+ {
+ override def check_thy(dir: Path, name: String): (String, Thy_Header.Header) =
+ {
+ val file = system.platform_file(dir + Thy_Header.thy_path(name))
+ if (!file.exists || !file.isFile) error("No such file: " + Library.quote(file.toString))
+ val text = Standard_System.read_file(file)
+ val header = thy_header.read(text)
+ (text, header)
+ }
+ }
+
+ val thy_info = new Thy_Info(thy_load)
+
+
+ /* actor messages */
+
private case object Interrupt_Prover
private case class Edit_Node(thy_name: String,
header: Exn.Result[Thy_Header.Header], edits: List[Text.Edit])
--- a/src/Pure/Thy/thy_info.ML Mon Jul 04 13:43:10 2011 +0200
+++ b/src/Pure/Thy/thy_info.ML Mon Jul 04 16:27:11 2011 +0200
@@ -279,13 +279,14 @@
let
val path = Path.expand (Path.explode str);
val name = Path.implode (Path.base path);
- val dir' = Path.append dir (Path.dir path);
- val _ = member (op =) initiators name andalso error (cycle_msg initiators);
in
(case try (Graph.get_node tasks) name of
SOME task => (task_finished task, tasks)
| NONE =>
let
+ val dir' = Path.append dir (Path.dir path);
+ val _ = member (op =) initiators name andalso error (cycle_msg initiators);
+
val (current, deps, imports) = check_deps dir' name
handle ERROR msg => cat_error msg
(loader_msg "the error(s) above occurred while examining theory" [name] ^
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/Thy/thy_info.scala Mon Jul 04 16:27:11 2011 +0200
@@ -0,0 +1,59 @@
+/* Title: Pure/Thy/thy_info.scala
+ Author: Makarius
+
+Theory and file dependencies.
+*/
+
+package isabelle
+
+
+class Thy_Info(thy_load: Thy_Load)
+{
+ /* messages */
+
+ private def show_path(names: List[String]): String =
+ names.map(Library.quote).mkString(" via ")
+
+ private def cycle_msg(names: List[String]): String =
+ "Cyclic dependency of " + show_path(names)
+
+ private def required_by(s: String, initiators: List[String]): String =
+ if (initiators.isEmpty) ""
+ else s + "(required by " + show_path(initiators.reverse) + ")"
+
+
+ /* dependencies */
+
+ type Deps = Map[String, Exn.Result[(String, Thy_Header.Header)]] // name -> (text, header)
+
+ private def require_thys(
+ initiators: List[String], dir: Path, deps: Deps, strs: List[String]): Deps =
+ (deps /: strs)(require_thy(initiators, dir, _, _))
+
+ private def require_thy(initiators: List[String], dir: Path, deps: Deps, str: String): Deps =
+ {
+ val path = Path.explode(str)
+ val name = path.base.implode
+
+ if (deps.isDefinedAt(name)) deps
+ else {
+ val dir1 = dir + path.dir
+ try {
+ if (initiators.contains(name)) error(cycle_msg(initiators))
+ val (text, header) =
+ try { thy_load.check_thy(dir1, name) }
+ catch {
+ case ERROR(msg) =>
+ cat_error(msg, "The error(s) above occurred while examining theory " +
+ Library.quote(name) + required_by("\n", initiators))
+ }
+ require_thys(name :: initiators, dir1,
+ deps + (name -> Exn.Res(text, header)), header.imports)
+ }
+ catch { case e: Throwable => deps + (name -> Exn.Exn(e)) }
+ }
+ }
+
+ def dependencies(dir: Path, str: String): Deps =
+ require_thy(Nil, dir, Map.empty, str) // FIXME capture errors in str (!??)
+}
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/Thy/thy_load.scala Mon Jul 04 16:27:11 2011 +0200
@@ -0,0 +1,13 @@
+/* Title: Pure/Thy/thy_load.scala
+ Author: Makarius
+
+Loading files that contribute to a theory.
+*/
+
+package isabelle
+
+abstract class Thy_Load
+{
+ def check_thy(dir: Path, name: String): (String, Thy_Header.Header)
+}
+
--- a/src/Pure/build-jars Mon Jul 04 13:43:10 2011 +0200
+++ b/src/Pure/build-jars Mon Jul 04 16:27:11 2011 +0200
@@ -50,6 +50,8 @@
Thy/completion.scala
Thy/html.scala
Thy/thy_header.scala
+ Thy/thy_info.scala
+ Thy/thy_load.scala
Thy/thy_syntax.scala
library.scala
package.scala
--- a/src/Pure/package.scala Mon Jul 04 13:43:10 2011 +0200
+++ b/src/Pure/package.scala Mon Jul 04 16:27:11 2011 +0200
@@ -6,6 +6,8 @@
package object isabelle
{
+ /* errors */
+
object ERROR
{
def apply(message: String): Throwable = new RuntimeException(message)
@@ -17,6 +19,11 @@
case _ => None
}
}
+
def error(message: String): Nothing = throw ERROR(message)
+
+ def cat_error(msg1: String, msg2: String): Nothing =
+ if (msg1 == "") error(msg1)
+ else error(msg1 + "\n" + msg2)
}