# HG changeset patch # User wenzelm # Date 1506439936 -7200 # Node ID 41177b1240674769055704890584b8f705ed4658 # Parent 02588021b5811e1c5e2c918a933cf44bb24c92ca tuned signature -- more readable output as Scala value; diff -r 02588021b581 -r 41177b124067 src/Pure/Thy/sessions.scala --- a/src/Pure/Thy/sessions.scala Tue Sep 26 16:12:21 2017 +0200 +++ b/src/Pure/Thy/sessions.scala Tue Sep 26 17:32:16 2017 +0200 @@ -106,7 +106,6 @@ sealed case class Base( pos: Position.T = Position.none, - imports: Option[Base] = None, global_theories: Map[String, String] = Map.empty, loaded_theories: Map[String, String] = Map.empty, known: Known = Known.empty, @@ -114,10 +113,9 @@ syntax: Outer_Syntax = Outer_Syntax.empty, sources: List[(Path, SHA1.Digest)] = Nil, session_graph: Graph_Display.Graph = Graph_Display.empty_graph, - errors: List[String] = Nil) + errors: List[String] = Nil, + imports: Option[Base] = None) { - def get_imports: Base = imports getOrElse Base.bootstrap(global_theories) - def platform_path: Base = copy(known = known.platform_path) def standard_path: Base = copy(known = known.standard_path) @@ -130,6 +128,8 @@ def dest_known_theories: List[(String, String)] = for ((theory, node_name) <- known.theories.toList) yield (theory, node_name.node) + + def get_imports: Base = imports getOrElse Base.bootstrap(global_theories) } sealed case class Deps(session_bases: Map[String, Base], all_known: Known) @@ -265,7 +265,6 @@ val base = Base( pos = info.pos, - imports = Some(imports_base), global_theories = global_theories, loaded_theories = thy_deps.loaded_theories, known = Known.make(info.dir, List(imports_base), thy_deps.deps.map(_.name)), @@ -273,7 +272,8 @@ syntax = syntax, sources = sources, session_graph = session_graph, - errors = thy_deps.errors ::: sources_errors) + errors = thy_deps.errors ::: sources_errors, + imports = Some(imports_base)) session_bases + (info.name -> base) }