# HG changeset patch
# User wenzelm
# Date 1309789631 -7200
# Node ID 511df47bcadc0ff0668fdc1775b353131b10c43b
# Parent  f00da558b78e645286455c7932d1445caf07e6ac
some support for theory files within Isabelle/Scala session;

diff -r f00da558b78e -r 511df47bcadc src/Pure/System/session.scala
--- 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])
diff -r f00da558b78e -r 511df47bcadc src/Pure/Thy/thy_info.ML
--- 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] ^
diff -r f00da558b78e -r 511df47bcadc src/Pure/Thy/thy_info.scala
--- /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 (!??)
+}
diff -r f00da558b78e -r 511df47bcadc src/Pure/Thy/thy_load.scala
--- /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)
+}
+
diff -r f00da558b78e -r 511df47bcadc src/Pure/build-jars
--- 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
diff -r f00da558b78e -r 511df47bcadc src/Pure/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)
 }