# HG changeset patch # User wenzelm # Date 1510066236 -3600 # Node ID 72d37a2e9ccad9c5559361b8e1e9e2b69dfe0000 # Parent e27e05d6f2a78e0c320d57aa46d4a37394bd84aa tuned; diff -r e27e05d6f2a7 -r 72d37a2e9cca src/Pure/Thy/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]) diff -r e27e05d6f2a7 -r 72d37a2e9cca src/Tools/jEdit/src/jedit_sessions.scala --- 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 =