# HG changeset patch
# User wenzelm
# Date 1344352102 -7200
# Node ID 5b51ccdc8623b1a0d70a5de40057c41a475277f7
# Parent  719f458cd89ea582a34b1ac12c6125228fb4f227
prefer static Build.session_content for loaded theories -- discontinued incremental protocol;

diff -r 719f458cd89e -r 5b51ccdc8623 src/Pure/PIDE/isabelle_markup.ML
--- a/src/Pure/PIDE/isabelle_markup.ML	Tue Aug 07 16:34:15 2012 +0200
+++ b/src/Pure/PIDE/isabelle_markup.ML	Tue Aug 07 17:08:22 2012 +0200
@@ -103,7 +103,6 @@
   val badN: string val bad: Markup.T
   val functionN: string
   val ready: Properties.T
-  val loaded_theory: string -> Properties.T
   val assign_execs: Properties.T
   val removed_versions: Properties.T
   val invoke_scala: string -> string -> Properties.T
@@ -308,8 +307,6 @@
 
 val ready = [(functionN, "ready")];
 
-fun loaded_theory name = [(functionN, "loaded_theory"), (Markup.nameN, name)];
-
 val assign_execs = [(functionN, "assign_execs")];
 val removed_versions = [(functionN, "removed_versions")];
 
diff -r 719f458cd89e -r 5b51ccdc8623 src/Pure/PIDE/isabelle_markup.scala
--- a/src/Pure/PIDE/isabelle_markup.scala	Tue Aug 07 16:34:15 2012 +0200
+++ b/src/Pure/PIDE/isabelle_markup.scala	Tue Aug 07 17:08:22 2012 +0200
@@ -252,15 +252,6 @@
 
   val Ready: Properties.T = List((FUNCTION, "ready"))
 
-  object Loaded_Theory
-  {
-    def unapply(props: Properties.T): Option[String] =
-      props match {
-        case List((FUNCTION, "loaded_theory"), (Markup.NAME, name)) => Some(name)
-        case _ => None
-      }
-  }
-
   val Assign_Execs: Properties.T = List((FUNCTION, "assign_execs"))
   val Removed_Versions: Properties.T = List((FUNCTION, "removed_versions"))
 
diff -r 719f458cd89e -r 5b51ccdc8623 src/Pure/System/build.scala
--- a/src/Pure/System/build.scala	Tue Aug 07 16:34:15 2012 +0200
+++ b/src/Pure/System/build.scala	Tue Aug 07 17:08:22 2012 +0200
@@ -315,22 +315,22 @@
   }
 
 
-  /* source dependencies */
+  /* source dependencies and static content */
 
-  sealed case class Node(
+  sealed case class Session_Content(
     loaded_theories: Set[String],
     syntax: Outer_Syntax,
     sources: List[(Path, SHA1.Digest)])
 
-  sealed case class Deps(deps: Map[String, Node])
+  sealed case class Deps(deps: Map[String, Session_Content])
   {
     def is_empty: Boolean = deps.isEmpty
-    def apply(name: String): Node = deps(name)
+    def apply(name: String): Session_Content = deps(name)
     def sources(name: String): List[SHA1.Digest] = deps(name).sources.map(_._2)
   }
 
   def dependencies(verbose: Boolean, tree: Session_Tree): Deps =
-    Deps((Map.empty[String, Node] /: tree.topological_order)(
+    Deps((Map.empty[String, Session_Content] /: tree.topological_order)(
       { case (deps, (name, info)) =>
           val (preloaded, parent_syntax) =
             info.parent match {
@@ -374,9 +374,17 @@
                   quote(name) + Position.str_of(info.pos))
             }
 
-          deps + (name -> Node(loaded_theories, syntax, sources))
+          deps + (name -> Session_Content(loaded_theories, syntax, sources))
       }))
 
+  def session_content(session: String): Session_Content =
+  {
+    val (_, tree) = find_sessions(Options.init(), Nil).required(false, Nil, List(session))
+    dependencies(false, tree)(session)
+  }
+
+  def outer_syntax(session: String): Outer_Syntax = session_content(session).syntax
+
 
   /* jobs */
 
@@ -391,7 +399,7 @@
         browser_info + Path.explode("isabelle.gif"))
       File.write(browser_info + Path.explode("index.html"),
         File.read(Path.explode("~~/lib/html/library_index_header.template")) +
-        File.read(Path.explode("~~/lib/html/library_index_content.template")) +
+        File.read(Path.explode("~~/lib/html/library_index_Session_Content.template")) +
         File.read(Path.explode("~~/lib/html/library_index_footer.template")))
     }
 
@@ -695,14 +703,5 @@
       }
     }
   }
-
-
-  /* static outer syntax */
-
-  def outer_syntax(session: String): Outer_Syntax =
-  {
-    val (_, tree) = find_sessions(Options.init(), Nil).required(false, Nil, List(session))
-    dependencies(false, tree)(session).syntax
-  }
 }
 
diff -r 719f458cd89e -r 5b51ccdc8623 src/Pure/System/isabelle_process.ML
--- a/src/Pure/System/isabelle_process.ML	Tue Aug 07 16:34:15 2012 +0200
+++ b/src/Pure/System/isabelle_process.ML	Tue Aug 07 17:08:22 2012 +0200
@@ -183,7 +183,6 @@
     val channel = rendezvous ();
     val _ = setup_channels channel;
 
-    val _ = Thy_Info.status ();
     val _ = Output.protocol_message Isabelle_Markup.ready "";
   in loop channel end));
 
diff -r 719f458cd89e -r 5b51ccdc8623 src/Pure/System/session.scala
--- a/src/Pure/System/session.scala	Tue Aug 07 16:34:15 2012 +0200
+++ b/src/Pure/System/session.scala	Tue Aug 07 17:08:22 2012 +0200
@@ -37,7 +37,7 @@
 }
 
 
-class Session(thy_load: Thy_Load = new Thy_Load())
+class Session(val thy_load: Thy_Load = new Thy_Load())
 {
   /* global flags */
 
@@ -354,9 +354,6 @@
         case Isabelle_Markup.Ready if output.is_protocol =>
             phase = Session.Ready
 
-        case Isabelle_Markup.Loaded_Theory(name) if output.is_protocol =>
-          thy_load.register_thy(name)
-
         case Isabelle_Markup.Return_Code(rc) if output.is_exit =>
           if (rc == 0) phase = Session.Inactive
           else phase = Session.Failed
@@ -380,7 +377,12 @@
         case Start(name, args) if prover.isEmpty =>
           if (phase == Session.Inactive || phase == Session.Failed) {
             phase = Session.Startup
-            base_syntax = Build.outer_syntax(name)
+
+            // FIXME static init in main constructor
+            val content = Build.session_content(name)
+            thy_load.register_thys(content.loaded_theories)
+            base_syntax = content.syntax
+
             prover = Some(new Isabelle_Process(receiver.invoke _, args) with Protocol)
           }
 
diff -r 719f458cd89e -r 5b51ccdc8623 src/Pure/Thy/thy_info.ML
--- a/src/Pure/Thy/thy_info.ML	Tue Aug 07 16:34:15 2012 +0200
+++ b/src/Pure/Thy/thy_info.ML	Tue Aug 07 17:08:22 2012 +0200
@@ -10,7 +10,6 @@
   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,10 +87,6 @@
 
 fun get_names () = Graph.topological_order (get_thys ());
 
-fun status () =
-  List.app (fn name => Output.protocol_message (Isabelle_Markup.loaded_theory name) "")
-    (get_names ());
-
 
 (* access thy *)
 
diff -r 719f458cd89e -r 5b51ccdc8623 src/Pure/Thy/thy_load.scala
--- a/src/Pure/Thy/thy_load.scala	Tue Aug 07 16:34:15 2012 +0200
+++ b/src/Pure/Thy/thy_load.scala	Tue Aug 07 17:08:22 2012 +0200
@@ -26,8 +26,11 @@
 
   private var loaded_theories: Set[String] = preloaded
 
-  def register_thy(thy_name: String): Unit =
-    synchronized { loaded_theories += thy_name }
+  def register_thy(name: String): Unit =
+    synchronized { loaded_theories += name }
+
+  def register_thys(names: Set[String]): Unit =
+    synchronized { loaded_theories ++= names }
 
   def is_loaded(thy_name: String): Boolean =
     synchronized { loaded_theories.contains(thy_name) }