tuned;
authorwenzelm
Tue, 07 Nov 2017 15:50:36 +0100
changeset 67024 72d37a2e9cca
parent 67023 e27e05d6f2a7
child 67025 961285f581e6
tuned;
src/Pure/Thy/sessions.scala
src/Tools/jEdit/src/jedit_sessions.scala
--- a/src/Pure/Thy/sessions.scala	Tue Nov 07 15:45:33 2017 +0100
+++ b/src/Pure/Thy/sessions.scala	Tue Nov 07 15:50:36 2017 +0100
@@ -175,7 +175,7 @@
       }
   }
 
-  def deps(sessions: T,
+  def deps(sessions_structure: T,
       global_theories: Map[String, String],
       progress: Progress = No_Progress,
       inlined_files: Boolean = false,
@@ -203,11 +203,11 @@
     }
 
     val session_bases =
-      (Map.empty[String, Base] /: sessions.imports_topological_order)({
+      (Map.empty[String, Base] /: sessions_structure.imports_topological_order)({
         case (session_bases, session_name) =>
           if (progress.stopped) throw Exn.Interrupt()
 
-          val info = sessions(session_name)
+          val info = sessions_structure(session_name)
           try {
             val parent_base: Sessions.Base =
               info.parent match {
@@ -273,7 +273,8 @@
               }
 
               val imports_subgraph =
-                sessions.imports_graph.restrict(sessions.imports_graph.all_preds(info.deps).toSet)
+                sessions_structure.imports_graph.
+                  restrict(sessions_structure.imports_graph.all_preds(info.deps).toSet)
 
               val graph0 =
                 (Graph_Display.empty_graph /: imports_subgraph.topological_order)(
@@ -329,7 +330,7 @@
 
   sealed case class Base_Info(
     session: String,
-    sessions: T,
+    sessions_structure: T,
     errors: List[String],
     base: Base,
     infos: List[Info])
--- a/src/Tools/jEdit/src/jedit_sessions.scala	Tue Nov 07 15:45:33 2017 +0100
+++ b/src/Tools/jEdit/src/jedit_sessions.scala	Tue Nov 07 15:50:36 2017 +0100
@@ -130,7 +130,7 @@
   def session_start(options: Options)
   {
     Isabelle_Process.start(PIDE.session, session_options(options),
-      sessions = Some(PIDE.resources.session_base_info.sessions),
+      sessions = Some(PIDE.resources.session_base_info.sessions_structure),
       logic = PIDE.resources.session_name,
       store = Sessions.store(session_build_mode() == "system"),
       modes =