# HG changeset patch # User wenzelm # Date 1506715952 -7200 # Node ID b071922536050340f4a3cf7fc568579f8e96dd2d # Parent d37efafd55b5c30860c4a4fa8228a5060a35b835 tuned signature; diff -r d37efafd55b5 -r b07192253605 src/Pure/PIDE/session.scala --- 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 */ diff -r d37efafd55b5 -r b07192253605 src/Pure/Thy/sessions.scala --- 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, diff -r d37efafd55b5 -r b07192253605 src/Pure/Thy/thy_syntax.scala --- 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 = diff -r d37efafd55b5 -r b07192253605 src/Pure/Tools/imports.scala --- 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 diff -r d37efafd55b5 -r b07192253605 src/Tools/VSCode/src/build_vscode.scala --- 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) diff -r d37efafd55b5 -r b07192253605 src/Tools/VSCode/src/grammar.scala --- 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) diff -r d37efafd55b5 -r b07192253605 src/Tools/jEdit/src/isabelle.scala --- 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)