Thy_Info.dependencies: ignore already loaded theories, according to initial prover session status;

--- a/src/Pure/General/markup.ML	Tue Jul 05 22:38:44 2011 +0200
+++ b/src/Pure/General/markup.ML	Tue Jul 05 22:39:15 2011 +0200
@@ -92,6 +92,7 @@
   val command_spanN: string val command_span: string -> T
   val ignored_spanN: string val ignored_span: T
   val malformed_spanN: string val malformed_span: T
+  val loaded_theoryN: string val loaded_theory: string -> T
   val elapsedN: string
   val cpuN: string
   val gcN: string
@@ -305,6 +306,11 @@
 val (malformed_spanN, malformed_span) = markup_elem "malformed_span";
 
 
+(* theory loader *)
+
+val (loaded_theoryN, loaded_theory) = markup_string "loaded_theory" nameN;
+
+
 (* timing *)
 
 val timingN = "timing";

--- a/src/Pure/General/markup.scala	Tue Jul 05 22:38:44 2011 +0200
+++ b/src/Pure/General/markup.scala	Tue Jul 05 22:39:15 2011 +0200
@@ -246,6 +246,11 @@
   val MALFORMED_SPAN = "malformed_span"
 
 
+  /* theory loader */
+
+  val LOADED_THEORY = "loaded_theory"
+
+
   /* timing */
 
   val TIMING = "timing"

--- a/src/Pure/System/isabelle_process.ML	Tue Jul 05 22:38:44 2011 +0200
+++ b/src/Pure/System/isabelle_process.ML	Tue Jul 05 22:39:15 2011 +0200
@@ -180,6 +180,7 @@
 
     val in_stream = setup_channels in_fifo out_fifo;
     val _ = Keyword.status ();
+    val _ = Thy_Info.status ();
     val _ = Output.status (Markup.markup Markup.ready "process ready");
   in loop in_stream end));
 

--- a/src/Pure/System/session.scala	Tue Jul 05 22:38:44 2011 +0200
+++ b/src/Pure/System/session.scala	Tue Jul 05 22:39:15 2011 +0200
@@ -115,6 +115,8 @@
 
   /* global state */
 
+  @volatile var loaded_theories: Set[String] = Set()
+
   @volatile private var syntax = new Outer_Syntax(Isabelle_System.symbols)
   def current_syntax(): Outer_Syntax = syntax
 
@@ -138,6 +140,9 @@
 
   val thy_load = new Thy_Load
   {
+    override def is_loaded(name: String): Boolean =
+      loaded_theories.contains(name)
+
     override def check_thy(dir: Path, name: String): (String, Thy_Header.Header) =
     {
       val file = Isabelle_System.platform_file(dir + Thy_Header.thy_path(name))
@@ -255,6 +260,7 @@
                 catch { case _: Document.State.Fail => bad_result(result) }
               case List(Keyword.Command_Decl(name, kind)) => syntax += (name, kind)
               case List(Keyword.Keyword_Decl(name)) => syntax += name
+              case List(Thy_Info.Loaded_Theory(name)) => loaded_theories += name
               case _ => bad_result(result)
             }
           }

--- a/src/Pure/Thy/thy_info.ML	Tue Jul 05 22:38:44 2011 +0200
+++ b/src/Pure/Thy/thy_info.ML	Tue Jul 05 22:39:15 2011 +0200
@@ -10,6 +10,7 @@
   datatype action = Update | Remove
   val add_hook: (action -> string -> unit) -> unit
   val get_names: unit -> string list
+  val status: unit -> unit
   val lookup_theory: string -> theory option
   val get_theory: string -> theory
   val is_finished: string -> bool
@@ -88,6 +89,9 @@
 
 fun get_names () = Graph.topological_order (get_thys ());
 
+fun status () =
+  List.app (Output.status o Markup.markup_only o Markup.loaded_theory) (get_names ());
+
 
 (* access thy *)
 

--- a/src/Pure/Thy/thy_info.scala	Tue Jul 05 22:38:44 2011 +0200
+++ b/src/Pure/Thy/thy_info.scala	Tue Jul 05 22:39:15 2011 +0200
@@ -7,6 +7,20 @@
 package isabelle
 
 
+object Thy_Info
+{
+  /* protocol messages */
+
+  object Loaded_Theory {
+    def unapply(msg: XML.Tree): Option[String] =
+      msg match {
+        case XML.Elem(Markup(Markup.LOADED_THEORY, List((Markup.NAME, name))), _) => Some(name)
+        case _ => None
+      }
+  }
+}
+
+
 class Thy_Info(thy_load: Thy_Load)
 {
   /* messages */
@@ -26,16 +40,17 @@
 
   type Deps = Map[String, Exn.Result[(String, Thy_Header.Header)]]  // name -> (text, header)
 
-  private def require_thys(
+  private def require_thys(ignored: String => Boolean,
       initiators: List[String], dir: Path, deps: Deps, strs: List[String]): Deps =
-    (deps /: strs)(require_thy(initiators, dir, _, _))
+    (deps /: strs)(require_thy(ignored, initiators, dir, _, _))
 
-  private def require_thy(initiators: List[String], dir: Path, deps: Deps, str: String): Deps =
+  private def require_thy(ignored: String => Boolean,
+      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
+    if (deps.isDefinedAt(name) || ignored(name)) deps
     else {
       val dir1 = dir + path.dir
       try {
@@ -47,7 +62,7 @@
               cat_error(msg, "The error(s) above occurred while examining theory " +
                 quote(name) + required_by("\n", initiators))
           }
-        require_thys(name :: initiators, dir1,
+        require_thys(ignored, name :: initiators, dir1,
           deps + (name -> Exn.Res(text, header)), header.imports)
       }
       catch { case e: Throwable => deps + (name -> Exn.Exn(e)) }
@@ -55,5 +70,5 @@
   }
 
   def dependencies(dir: Path, str: String): Deps =
-    require_thy(Nil, dir, Map.empty, str)  // FIXME capture errors in str (!??)
+    require_thy(thy_load.is_loaded, Nil, dir, Map.empty, str)  // FIXME capture errors in str (!??)
 }

--- a/src/Pure/Thy/thy_load.scala	Tue Jul 05 22:38:44 2011 +0200
+++ b/src/Pure/Thy/thy_load.scala	Tue Jul 05 22:39:15 2011 +0200
@@ -8,6 +8,8 @@
 
 abstract class Thy_Load
 {
+  def is_loaded(name: String): Boolean
+
   def check_thy(dir: Path, name: String): (String, Thy_Header.Header)
 }