src/Pure/System/session.scala

     }
   }
 }
 
 
-class Session(val thy_load: Thy_Load)
+class Session(val resources: Resources)
 {
   /* global flags */
 
   @volatile var timing: Boolean = false
   @volatile var verbose: Boolean = false

         case Stop => finished = true; reply(())
 
         case Text_Edits(previous, doc_blobs, text_edits, version_result) =>
           val prev = previous.get_finished
           val (syntax_changed, doc_edits, version) =
-            Timing.timeit("Thy_Load.text_edits", timing) {
-              thy_load.text_edits(reparse_limit, prev, doc_blobs, text_edits)
+            Timing.timeit("text_edits", timing) {
+              resources.text_edits(reparse_limit, prev, doc_blobs, text_edits)
             }
           version_result.fulfill(version)
           sender ! Change(doc_blobs, syntax_changed, doc_edits, prev, version)
 
         case bad => System.err.println("change_parser: ignoring bad message " + bad)

   def current_state(): Document.State = global_state()
 
   def recent_syntax(): Outer_Syntax =
   {
     val version = current_state().recent_finished.version.get_finished
-    if (version.is_init) thy_load.base_syntax
+    if (version.is_init) resources.base_syntax
     else version.syntax
   }
 
   def snapshot(name: Document.Node.Name = Document.Node.Name.empty,
       pending_edits: List[Text.Edit] = Nil): Document.Snapshot =

   /* theory files */
 
   def header_edit(name: Document.Node.Name, header: Document.Node.Header): Document.Edit_Text =
   {
     val header1 =
-      if (thy_load.loaded_theories(name.theory))
+      if (resources.loaded_theories(name.theory))
         header.error("Cannot update finished theory " + quote(name.theory))
       else header
     (name, Document.Node.Deps(header1))
   }
 

 
       val assignment = global_state().the_assignment(previous).check_finished
       global_state >> (_.define_version(version, assignment))
       prover.get.update(previous.id, version.id, doc_edits)
 
-      if (syntax_changed) thy_load.syntax_changed()
+      if (syntax_changed) resources.syntax_changed()
     }
     //}}}
 
 
     /* prover output */