src/Pure/Thy/sessions.scala
changeset 66719 d37efafd55b5
parent 66718 514c4907ff0b
child 66720 b07192253605
     1.1 --- a/src/Pure/Thy/sessions.scala	Fri Sep 29 21:03:04 2017 +0200
     1.2 +++ b/src/Pure/Thy/sessions.scala	Fri Sep 29 21:30:31 2017 +0200
     1.3 @@ -205,13 +205,13 @@
     1.4                resources.thy_info.dependencies(root_theories)
     1.5              }
     1.6  
     1.7 -            val syntax = thy_deps.syntax
     1.8 +            val session_syntax = thy_deps.overall_syntax
     1.9  
    1.10              val theory_files = thy_deps.names.map(_.path)
    1.11              val loaded_files =
    1.12                if (inlined_files) {
    1.13                  if (Sessions.is_pure(info.name)) {
    1.14 -                  (Thy_Header.PURE -> resources.pure_files(syntax, info.dir)) ::
    1.15 +                  (Thy_Header.PURE -> resources.pure_files(session_syntax, info.dir)) ::
    1.16                      thy_deps.loaded_files.filterNot(p => p._1 == Thy_Header.PURE)
    1.17                  }
    1.18                  else thy_deps.loaded_files
    1.19 @@ -226,8 +226,10 @@
    1.20              if (list_files)
    1.21                progress.echo(cat_lines(all_files.map(_.implode).sorted.map("  " + _)))
    1.22  
    1.23 -            if (check_keywords.nonEmpty)
    1.24 -              Check_Keywords.check_keywords(progress, syntax.keywords, check_keywords, theory_files)
    1.25 +            if (check_keywords.nonEmpty) {
    1.26 +              Check_Keywords.check_keywords(
    1.27 +                progress, session_syntax.keywords, check_keywords, theory_files)
    1.28 +            }
    1.29  
    1.30              val session_graph: Graph_Display.Graph =
    1.31              {
    1.32 @@ -278,7 +280,7 @@
    1.33                  global_theories = global_theories,
    1.34                  loaded_theories = thy_deps.loaded_theories,
    1.35                  known = known,
    1.36 -                syntax = syntax,
    1.37 +                syntax = session_syntax,
    1.38                  sources = sources,
    1.39                  session_graph = session_graph,
    1.40                  errors = thy_deps.errors ::: sources_errors,