# HG changeset patch
# User wenzelm
# Date 1521235209 -3600
# Node ID 43af581d7d8ec5a3e8602b2c691106a5b3f7e755
# Parent  171e7735ce2581639944ab47c1c693f766051373
unload_theories after consolidation -- reset node_required;
proper node_perspective (amending 0d8e4e777973);

diff -r 171e7735ce25 -r 43af581d7d8e src/Pure/Thy/thy_resources.scala
--- a/src/Pure/Thy/thy_resources.scala	Fri Mar 16 18:42:35 2018 +0100
+++ b/src/Pure/Thy/thy_resources.scala	Fri Mar 16 22:20:09 2018 +0100
@@ -68,10 +68,11 @@
       theories: List[(String, Position.T)],
       qualifier: String = Sessions.DRAFT,
       master_dir: String = "",
+      id: String = Library.UUID(),
       progress: Progress = No_Progress): Theories_Result =
     {
       val requirements =
-        resources.load_theories(session, theories, qualifier = qualifier,
+        resources.load_theories(session, id, theories, qualifier = qualifier,
           master_dir = master_dir, progress = progress)
 
       val result = Future.promise[Theories_Result]
@@ -99,6 +100,9 @@
       check_state
       result.join
       session.commands_changed -= consumer
+
+      resources.unload_theories(session, id, requirements)
+
       result.join
     }
   }
@@ -106,30 +110,45 @@
 
   /* internal state */
 
-  sealed case class State(theories: Map[Document.Node.Name, Theory] = Map.empty)
+  sealed case class State(
+    theories: Map[Document.Node.Name, Theory] = Map.empty,
+    required: Multi_Map[Document.Node.Name, String] = Multi_Map.empty)
+  {
+    def update(theory_edits: List[((Document.Node.Name, Theory), List[Document.Edit_Text])],
+        new_required: Multi_Map[Document.Node.Name, String]): (List[Document.Edit_Text], State) =
+    {
+      val edits = theory_edits.flatMap(_._2)
+      val st = State(theories ++ theory_edits.map(_._1), new_required)
+      (edits, st)
+    }
+  }
 
   final class Theory private[Thy_Resources](
     val node_name: Document.Node.Name,
     val node_header: Document.Node.Header,
-    val text: String)
+    val text: String,
+    val node_required: Boolean)
   {
     override def toString: String = node_name.toString
 
     def node_perspective: Document.Node.Perspective_Text =
-      Document.Node.Perspective(true, Text.Perspective.full, Document.Node.Overlays.empty)
+      Document.Node.Perspective(node_required, Text.Perspective.empty, Document.Node.Overlays.empty)
 
     def node_edits(old: Option[Theory]): List[Document.Edit_Text] =
     {
-      val text_edits =
-        if (old.isEmpty) Text.Edit.inserts(0, text)
-        else Text.Edit.replace(0, old.get.text, text)
+      val (text_edits, old_required) =
+        if (old.isEmpty) (Text.Edit.inserts(0, text), false)
+        else (Text.Edit.replace(0, old.get.text, text), old.get.node_required)
 
-      if (text_edits.isEmpty) Nil
+      if (text_edits.isEmpty && node_required == old_required) Nil
       else
         List(node_name -> Document.Node.Deps(node_header),
           node_name -> Document.Node.Edits(text_edits),
           node_name -> node_perspective)
     }
+
+    def unload: Theory =
+      if (node_required) new Theory(node_name, node_header, text, false) else this
   }
 }
 
@@ -140,18 +159,19 @@
 
   private val state = Synchronized(Thy_Resources.State())
 
-  def read_thy(node_name: Document.Node.Name): Thy_Resources.Theory =
+  def load_thy(node_name: Document.Node.Name): Thy_Resources.Theory =
   {
     val path = node_name.path
     if (!node_name.is_theory) error("Not a theory file: " + path)
 
     val text = File.read(path)
     val node_header = resources.check_thy_reader(node_name, Scan.char_reader(text))
-    new Thy_Resources.Theory(node_name, node_header, text)
+    new Thy_Resources.Theory(node_name, node_header, text, true)
   }
 
   def load_theories(
     session: Session,
+    id: String,
     theories: List[(String, Position.T)],
     qualifier: String = Sessions.DRAFT,
     master_dir: String = "",
@@ -162,24 +182,44 @@
       yield (import_name(qualifier, master_dir, thy), pos)
 
     val dependencies = resources.dependencies(import_names, progress = progress).check_errors
-    val loaded_theories = dependencies.theories.map(read_thy(_))
+    val loaded_theories = dependencies.theories.map(load_thy(_))
 
     val edits =
       state.change_result(st =>
       {
         val theory_edits =
-          for {
-            theory <- loaded_theories
+          (for {
+            theory <- loaded_theories.iterator
             node_name = theory.node_name
             edits = theory.node_edits(st.theories.get(node_name))
             if edits.nonEmpty
-          } yield ((node_name, theory), edits)
-
-        val st1 = st.copy(theories = st.theories ++ theory_edits.map(_._1))
-        (theory_edits.flatMap(_._2), st1)
+          } yield ((node_name, theory), edits)).toList
+        val required =
+          (st.required /: loaded_theories)({ case (req, thy) => req.insert(thy.node_name, id) })
+        st.update(theory_edits, required)
       })
     session.update(Document.Blobs.empty, edits)
 
     dependencies.theories
   }
+
+  def unload_theories(session: Session, id: String, theories: List[Document.Node.Name])
+  {
+    val edits =
+      state.change_result(st =>
+      {
+        val theory_edits =
+          (for {
+            node_name <- theories.iterator
+            theory <- st.theories.get(node_name)
+            theory1 = theory.unload
+            edits = theory1.node_edits(Some(theory))
+            if edits.nonEmpty
+          } yield ((node_name, theory1), edits)).toList
+        val required =
+          (st.required /: theories)({ case (req, node_name) => req.remove(node_name, id) })
+        st.update(theory_edits, required)
+      })
+    session.update(Document.Blobs.empty, edits)
+  }
 }
diff -r 171e7735ce25 -r 43af581d7d8e src/Pure/Tools/server.scala
--- a/src/Pure/Tools/server.scala	Fri Mar 16 18:42:35 2018 +0100
+++ b/src/Pure/Tools/server.scala	Fri Mar 16 22:20:09 2018 +0100
@@ -97,7 +97,8 @@
               context.make_task(task =>
                 {
                   val session = context.server.the_session(args.session_id)
-                  Server_Commands.Use_Theories.command(args, session, progress = task.progress)._1
+                  Server_Commands.Use_Theories.command(
+                    args, session, id = task.id, progress = task.progress)._1
                 })
           })
 
diff -r 171e7735ce25 -r 43af581d7d8e src/Pure/Tools/server_commands.scala
--- a/src/Pure/Tools/server_commands.scala	Fri Mar 16 18:42:35 2018 +0100
+++ b/src/Pure/Tools/server_commands.scala	Fri Mar 16 22:20:09 2018 +0100
@@ -170,12 +170,14 @@
       }
       yield Args(session_id, theories, qualifier = qualifier, master_dir = master_dir)
 
-    def command(args: Args, session: Thy_Resources.Session, progress: Progress = No_Progress)
-      : (JSON.Object.T, Thy_Resources.Theories_Result) =
+    def command(args: Args,
+      session: Thy_Resources.Session,
+      id: String = Library.UUID(),
+      progress: Progress = No_Progress): (JSON.Object.T, Thy_Resources.Theories_Result) =
     {
       val result =
         session.use_theories(args.theories, qualifier = args.qualifier,
-          master_dir = args.master_dir, progress = progress)
+          master_dir = args.master_dir, id = id, progress = progress)
 
       val result_json =
         JSON.Object(