src/Pure/Thy/sessions.scala
changeset 67053 57c37ee49c39
parent 67052 caf87d4b9b61
child 67059 df7d728103f1
     1.1 --- a/src/Pure/Thy/sessions.scala	Sun Nov 12 12:41:05 2017 +0100
     1.2 +++ b/src/Pure/Thy/sessions.scala	Sun Nov 12 12:55:10 2017 +0100
     1.3 @@ -227,21 +227,21 @@
     1.4                progress.echo("Session " + info.chapter + "/" + info.name + groups)
     1.5              }
     1.6  
     1.7 -            val thy_deps =
     1.8 +            val dependencies =
     1.9                resources.dependencies(
    1.10                  for { (_, thys) <- info.theories; (thy, pos) <- thys }
    1.11                  yield (resources.import_name(info.name, info.dir.implode, thy), pos))
    1.12  
    1.13 -            val overall_syntax = thy_deps.overall_syntax
    1.14 +            val overall_syntax = dependencies.overall_syntax
    1.15  
    1.16 -            val theory_files = thy_deps.names.map(_.path)
    1.17 +            val theory_files = dependencies.names.map(_.path)
    1.18              val loaded_files =
    1.19                if (inlined_files) {
    1.20                  if (Sessions.is_pure(info.name)) {
    1.21                    (Thy_Header.PURE -> resources.pure_files(overall_syntax, info.dir)) ::
    1.22 -                    thy_deps.loaded_files.filterNot(p => p._1 == Thy_Header.PURE)
    1.23 +                    dependencies.loaded_files.filterNot(p => p._1 == Thy_Header.PURE)
    1.24                  }
    1.25 -                else thy_deps.loaded_files
    1.26 +                else dependencies.loaded_files
    1.27                }
    1.28                else Nil
    1.29  
    1.30 @@ -249,7 +249,7 @@
    1.31                (theory_files ::: loaded_files.flatMap(_._2) :::
    1.32                  info.document_files.map(file => info.dir + file._1 + file._2)).map(_.expand)
    1.33  
    1.34 -            val imported_files = if (inlined_files) thy_deps.imported_files else Nil
    1.35 +            val imported_files = if (inlined_files) dependencies.imported_files else Nil
    1.36  
    1.37              if (list_files)
    1.38                progress.echo(cat_lines(session_files.map(_.implode).sorted.map("  " + _)))
    1.39 @@ -283,7 +283,7 @@
    1.40                        val bs = imports_subgraph.imm_preds(session).toList.map(session_node(_))
    1.41                        ((g /: (a :: bs))(_.default_node(_, Nil)) /: bs)(_.add_edge(_, a)) })
    1.42  
    1.43 -              (graph0 /: thy_deps.entries)(
    1.44 +              (graph0 /: dependencies.entries)(
    1.45                  { case (g, entry) =>
    1.46                      val a = node(entry.name)
    1.47                      val bs =
    1.48 @@ -294,7 +294,7 @@
    1.49  
    1.50              val known =
    1.51                Known.make(info.dir, List(imports_base),
    1.52 -                theories = thy_deps.names,
    1.53 +                theories = dependencies.names,
    1.54                  loaded_files = loaded_files)
    1.55  
    1.56              val sources_errors =
    1.57 @@ -304,13 +304,13 @@
    1.58                Base(
    1.59                  pos = info.pos,
    1.60                  global_theories = global_theories,
    1.61 -                loaded_theories = thy_deps.loaded_theories,
    1.62 +                loaded_theories = dependencies.loaded_theories,
    1.63                  known = known,
    1.64                  overall_syntax = overall_syntax,
    1.65                  imported_sources = check_sources(imported_files),
    1.66                  sources = check_sources(session_files),
    1.67                  session_graph_display = session_graph_display,
    1.68 -                errors = thy_deps.errors ::: sources_errors,
    1.69 +                errors = dependencies.errors ::: sources_errors,
    1.70                  imports = Some(imports_base))
    1.71  
    1.72              session_bases + (info.name -> base)