src/Pure/Thy/sessions.scala
changeset 66720 b07192253605
parent 66719 d37efafd55b5
child 66721 ae38b8c0fdd9
     1.1 --- a/src/Pure/Thy/sessions.scala	Fri Sep 29 21:30:31 2017 +0200
     1.2 +++ b/src/Pure/Thy/sessions.scala	Fri Sep 29 22:12:32 2017 +0200
     1.3 @@ -107,7 +107,7 @@
     1.4      def bootstrap(global_theories: Map[String, String]): Base =
     1.5        Base(
     1.6          global_theories = global_theories,
     1.7 -        syntax = Thy_Header.bootstrap_syntax)
     1.8 +        overall_syntax = Thy_Header.bootstrap_syntax)
     1.9    }
    1.10  
    1.11    sealed case class Base(
    1.12 @@ -115,7 +115,7 @@
    1.13      global_theories: Map[String, String] = Map.empty,
    1.14      loaded_theories: Graph[String, Outer_Syntax] = Graph.string,
    1.15      known: Known = Known.empty,
    1.16 -    syntax: Outer_Syntax = Outer_Syntax.empty,
    1.17 +    overall_syntax: Outer_Syntax = Outer_Syntax.empty,
    1.18      sources: List[(Path, SHA1.Digest)] = Nil,
    1.19      session_graph: Graph_Display.Graph = Graph_Display.empty_graph,
    1.20      errors: List[String] = Nil,
    1.21 @@ -205,13 +205,13 @@
    1.22                resources.thy_info.dependencies(root_theories)
    1.23              }
    1.24  
    1.25 -            val session_syntax = thy_deps.overall_syntax
    1.26 +            val overall_syntax = thy_deps.overall_syntax
    1.27  
    1.28              val theory_files = thy_deps.names.map(_.path)
    1.29              val loaded_files =
    1.30                if (inlined_files) {
    1.31                  if (Sessions.is_pure(info.name)) {
    1.32 -                  (Thy_Header.PURE -> resources.pure_files(session_syntax, info.dir)) ::
    1.33 +                  (Thy_Header.PURE -> resources.pure_files(overall_syntax, info.dir)) ::
    1.34                      thy_deps.loaded_files.filterNot(p => p._1 == Thy_Header.PURE)
    1.35                  }
    1.36                  else thy_deps.loaded_files
    1.37 @@ -228,7 +228,7 @@
    1.38  
    1.39              if (check_keywords.nonEmpty) {
    1.40                Check_Keywords.check_keywords(
    1.41 -                progress, session_syntax.keywords, check_keywords, theory_files)
    1.42 +                progress, overall_syntax.keywords, check_keywords, theory_files)
    1.43              }
    1.44  
    1.45              val session_graph: Graph_Display.Graph =
    1.46 @@ -280,7 +280,7 @@
    1.47                  global_theories = global_theories,
    1.48                  loaded_theories = thy_deps.loaded_theories,
    1.49                  known = known,
    1.50 -                syntax = session_syntax,
    1.51 +                overall_syntax = overall_syntax,
    1.52                  sources = sources,
    1.53                  session_graph = session_graph,
    1.54                  errors = thy_deps.errors ::: sources_errors,