src/Pure/Thy/sessions.scala
changeset 66720 b07192253605
parent 66719 d37efafd55b5
child 66721 ae38b8c0fdd9
--- a/src/Pure/Thy/sessions.scala	Fri Sep 29 21:30:31 2017 +0200
+++ b/src/Pure/Thy/sessions.scala	Fri Sep 29 22:12:32 2017 +0200
@@ -107,7 +107,7 @@
     def bootstrap(global_theories: Map[String, String]): Base =
       Base(
         global_theories = global_theories,
-        syntax = Thy_Header.bootstrap_syntax)
+        overall_syntax = Thy_Header.bootstrap_syntax)
   }
 
   sealed case class Base(
@@ -115,7 +115,7 @@
     global_theories: Map[String, String] = Map.empty,
     loaded_theories: Graph[String, Outer_Syntax] = Graph.string,
     known: Known = Known.empty,
-    syntax: Outer_Syntax = Outer_Syntax.empty,
+    overall_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,
@@ -205,13 +205,13 @@
               resources.thy_info.dependencies(root_theories)
             }
 
-            val session_syntax = thy_deps.overall_syntax
+            val overall_syntax = thy_deps.overall_syntax
 
             val theory_files = thy_deps.names.map(_.path)
             val loaded_files =
               if (inlined_files) {
                 if (Sessions.is_pure(info.name)) {
-                  (Thy_Header.PURE -> resources.pure_files(session_syntax, info.dir)) ::
+                  (Thy_Header.PURE -> resources.pure_files(overall_syntax, info.dir)) ::
                     thy_deps.loaded_files.filterNot(p => p._1 == Thy_Header.PURE)
                 }
                 else thy_deps.loaded_files
@@ -228,7 +228,7 @@
 
             if (check_keywords.nonEmpty) {
               Check_Keywords.check_keywords(
-                progress, session_syntax.keywords, check_keywords, theory_files)
+                progress, overall_syntax.keywords, check_keywords, theory_files)
             }
 
             val session_graph: Graph_Display.Graph =
@@ -280,7 +280,7 @@
                 global_theories = global_theories,
                 loaded_theories = thy_deps.loaded_theories,
                 known = known,
-                syntax = session_syntax,
+                overall_syntax = overall_syntax,
                 sources = sources,
                 session_graph = session_graph,
                 errors = thy_deps.errors ::: sources_errors,