tuned signature;

--- a/src/Pure/PIDE/session.scala	Fri Sep 29 21:30:31 2017 +0200
+++ b/src/Pure/PIDE/session.scala	Fri Sep 29 22:12:32 2017 +0200
@@ -220,7 +220,7 @@
 
   def recent_syntax(name: Document.Node.Name): Outer_Syntax =
     global_state.value.recent_finished.version.get_finished.nodes(name).syntax getOrElse
-    resources.session_base.syntax
+    resources.session_base.overall_syntax
 
 
   /* pipelined change parsing */

--- 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,

--- a/src/Pure/Thy/thy_syntax.scala	Fri Sep 29 21:30:31 2017 +0200
+++ b/src/Pure/Thy/thy_syntax.scala	Fri Sep 29 22:12:32 2017 +0200
@@ -101,7 +101,7 @@
         else {
           val header = node.header
           val imports_syntax = header.imports.flatMap(a => nodes(a._1).syntax)
-          Some((resources.session_base.syntax /: imports_syntax)(_ ++ _) + header)
+          Some((resources.session_base.overall_syntax /: imports_syntax)(_ ++ _) + header)
         }
       nodes += (name -> node.update_syntax(syntax))
     }
@@ -323,7 +323,7 @@
         node_edits foreach {
           case (name, edits) =>
             val node = nodes(name)
-            val syntax = node.syntax getOrElse resources.session_base.syntax
+            val syntax = node.syntax getOrElse resources.session_base.overall_syntax
             val commands = node.commands
 
             val node1 =

--- a/src/Pure/Tools/imports.scala	Fri Sep 29 21:30:31 2017 +0200
+++ b/src/Pure/Tools/imports.scala	Fri Sep 29 22:12:32 2017 +0200
@@ -170,7 +170,7 @@
               (_, name) <- session_base.known.theories_local.toList
               if session_resources.theory_qualifier(name) == info.theory_qualifier
               (_, pos) <- session_resources.check_thy(name, Token.Pos.file(name.node)).imports
-              upd <- update_name(session_base.syntax.keywords, pos,
+              upd <- update_name(session_base.overall_syntax.keywords, pos,
                 standard_import(session_resources.theory_qualifier(name), name.master_dir, _))
             } yield upd
 

--- a/src/Tools/VSCode/src/build_vscode.scala	Fri Sep 29 21:30:31 2017 +0200
+++ b/src/Tools/VSCode/src/build_vscode.scala	Fri Sep 29 22:12:32 2017 +0200
@@ -20,7 +20,7 @@
   def build_grammar(options: Options, progress: Progress = No_Progress)
   {
     val logic = Grammar.default_logic
-    val keywords = Sessions.session_base(options, logic).syntax.keywords
+    val keywords = Sessions.session_base(options, logic).overall_syntax.keywords
 
     val output_path = extension_dir + Path.explode(Grammar.default_output(logic))
     progress.echo(output_path.implode)

--- a/src/Tools/VSCode/src/grammar.scala	Fri Sep 29 21:30:31 2017 +0200
+++ b/src/Tools/VSCode/src/grammar.scala	Fri Sep 29 22:12:32 2017 +0200
@@ -157,7 +157,7 @@
     val more_args = getopts(args)
     if (more_args.nonEmpty) getopts.usage()
 
-    val keywords = Sessions.session_base(Options.init(), logic, dirs).syntax.keywords
+    val keywords = Sessions.session_base(Options.init(), logic, dirs).overall_syntax.keywords
     val output_path = output getOrElse Path.explode(default_output(logic))
 
     Output.writeln(output_path.implode)

--- a/src/Tools/jEdit/src/isabelle.scala	Fri Sep 29 21:30:31 2017 +0200
+++ b/src/Tools/jEdit/src/isabelle.scala	Fri Sep 29 22:12:32 2017 +0200
@@ -50,7 +50,7 @@
 
   def mode_syntax(mode: String): Option[Outer_Syntax] =
     mode match {
-      case "isabelle" => Some(PIDE.resources.session_base.syntax)
+      case "isabelle" => Some(PIDE.resources.session_base.overall_syntax)
       case "isabelle-options" => Some(Options.options_syntax)
       case "isabelle-root" => Some(Sessions.root_syntax)
       case "isabelle-ml" => Some(ml_syntax)