tuned signature;
authorwenzelm
Fri Sep 29 22:12:32 2017 +0200 (20 months ago)
changeset 66720b07192253605
parent 66719 d37efafd55b5
child 66721 ae38b8c0fdd9
tuned signature;
src/Pure/PIDE/session.scala
src/Pure/Thy/sessions.scala
src/Pure/Thy/thy_syntax.scala
src/Pure/Tools/imports.scala
src/Tools/VSCode/src/build_vscode.scala
src/Tools/VSCode/src/grammar.scala
src/Tools/jEdit/src/isabelle.scala
     1.1 --- a/src/Pure/PIDE/session.scala	Fri Sep 29 21:30:31 2017 +0200
     1.2 +++ b/src/Pure/PIDE/session.scala	Fri Sep 29 22:12:32 2017 +0200
     1.3 @@ -220,7 +220,7 @@
     1.4  
     1.5    def recent_syntax(name: Document.Node.Name): Outer_Syntax =
     1.6      global_state.value.recent_finished.version.get_finished.nodes(name).syntax getOrElse
     1.7 -    resources.session_base.syntax
     1.8 +    resources.session_base.overall_syntax
     1.9  
    1.10  
    1.11    /* pipelined change parsing */
     2.1 --- a/src/Pure/Thy/sessions.scala	Fri Sep 29 21:30:31 2017 +0200
     2.2 +++ b/src/Pure/Thy/sessions.scala	Fri Sep 29 22:12:32 2017 +0200
     2.3 @@ -107,7 +107,7 @@
     2.4      def bootstrap(global_theories: Map[String, String]): Base =
     2.5        Base(
     2.6          global_theories = global_theories,
     2.7 -        syntax = Thy_Header.bootstrap_syntax)
     2.8 +        overall_syntax = Thy_Header.bootstrap_syntax)
     2.9    }
    2.10  
    2.11    sealed case class Base(
    2.12 @@ -115,7 +115,7 @@
    2.13      global_theories: Map[String, String] = Map.empty,
    2.14      loaded_theories: Graph[String, Outer_Syntax] = Graph.string,
    2.15      known: Known = Known.empty,
    2.16 -    syntax: Outer_Syntax = Outer_Syntax.empty,
    2.17 +    overall_syntax: Outer_Syntax = Outer_Syntax.empty,
    2.18      sources: List[(Path, SHA1.Digest)] = Nil,
    2.19      session_graph: Graph_Display.Graph = Graph_Display.empty_graph,
    2.20      errors: List[String] = Nil,
    2.21 @@ -205,13 +205,13 @@
    2.22                resources.thy_info.dependencies(root_theories)
    2.23              }
    2.24  
    2.25 -            val session_syntax = thy_deps.overall_syntax
    2.26 +            val overall_syntax = thy_deps.overall_syntax
    2.27  
    2.28              val theory_files = thy_deps.names.map(_.path)
    2.29              val loaded_files =
    2.30                if (inlined_files) {
    2.31                  if (Sessions.is_pure(info.name)) {
    2.32 -                  (Thy_Header.PURE -> resources.pure_files(session_syntax, info.dir)) ::
    2.33 +                  (Thy_Header.PURE -> resources.pure_files(overall_syntax, info.dir)) ::
    2.34                      thy_deps.loaded_files.filterNot(p => p._1 == Thy_Header.PURE)
    2.35                  }
    2.36                  else thy_deps.loaded_files
    2.37 @@ -228,7 +228,7 @@
    2.38  
    2.39              if (check_keywords.nonEmpty) {
    2.40                Check_Keywords.check_keywords(
    2.41 -                progress, session_syntax.keywords, check_keywords, theory_files)
    2.42 +                progress, overall_syntax.keywords, check_keywords, theory_files)
    2.43              }
    2.44  
    2.45              val session_graph: Graph_Display.Graph =
    2.46 @@ -280,7 +280,7 @@
    2.47                  global_theories = global_theories,
    2.48                  loaded_theories = thy_deps.loaded_theories,
    2.49                  known = known,
    2.50 -                syntax = session_syntax,
    2.51 +                overall_syntax = overall_syntax,
    2.52                  sources = sources,
    2.53                  session_graph = session_graph,
    2.54                  errors = thy_deps.errors ::: sources_errors,
     3.1 --- a/src/Pure/Thy/thy_syntax.scala	Fri Sep 29 21:30:31 2017 +0200
     3.2 +++ b/src/Pure/Thy/thy_syntax.scala	Fri Sep 29 22:12:32 2017 +0200
     3.3 @@ -101,7 +101,7 @@
     3.4          else {
     3.5            val header = node.header
     3.6            val imports_syntax = header.imports.flatMap(a => nodes(a._1).syntax)
     3.7 -          Some((resources.session_base.syntax /: imports_syntax)(_ ++ _) + header)
     3.8 +          Some((resources.session_base.overall_syntax /: imports_syntax)(_ ++ _) + header)
     3.9          }
    3.10        nodes += (name -> node.update_syntax(syntax))
    3.11      }
    3.12 @@ -323,7 +323,7 @@
    3.13          node_edits foreach {
    3.14            case (name, edits) =>
    3.15              val node = nodes(name)
    3.16 -            val syntax = node.syntax getOrElse resources.session_base.syntax
    3.17 +            val syntax = node.syntax getOrElse resources.session_base.overall_syntax
    3.18              val commands = node.commands
    3.19  
    3.20              val node1 =
     4.1 --- a/src/Pure/Tools/imports.scala	Fri Sep 29 21:30:31 2017 +0200
     4.2 +++ b/src/Pure/Tools/imports.scala	Fri Sep 29 22:12:32 2017 +0200
     4.3 @@ -170,7 +170,7 @@
     4.4                (_, name) <- session_base.known.theories_local.toList
     4.5                if session_resources.theory_qualifier(name) == info.theory_qualifier
     4.6                (_, pos) <- session_resources.check_thy(name, Token.Pos.file(name.node)).imports
     4.7 -              upd <- update_name(session_base.syntax.keywords, pos,
     4.8 +              upd <- update_name(session_base.overall_syntax.keywords, pos,
     4.9                  standard_import(session_resources.theory_qualifier(name), name.master_dir, _))
    4.10              } yield upd
    4.11  
     5.1 --- a/src/Tools/VSCode/src/build_vscode.scala	Fri Sep 29 21:30:31 2017 +0200
     5.2 +++ b/src/Tools/VSCode/src/build_vscode.scala	Fri Sep 29 22:12:32 2017 +0200
     5.3 @@ -20,7 +20,7 @@
     5.4    def build_grammar(options: Options, progress: Progress = No_Progress)
     5.5    {
     5.6      val logic = Grammar.default_logic
     5.7 -    val keywords = Sessions.session_base(options, logic).syntax.keywords
     5.8 +    val keywords = Sessions.session_base(options, logic).overall_syntax.keywords
     5.9  
    5.10      val output_path = extension_dir + Path.explode(Grammar.default_output(logic))
    5.11      progress.echo(output_path.implode)
     6.1 --- a/src/Tools/VSCode/src/grammar.scala	Fri Sep 29 21:30:31 2017 +0200
     6.2 +++ b/src/Tools/VSCode/src/grammar.scala	Fri Sep 29 22:12:32 2017 +0200
     6.3 @@ -157,7 +157,7 @@
     6.4      val more_args = getopts(args)
     6.5      if (more_args.nonEmpty) getopts.usage()
     6.6  
     6.7 -    val keywords = Sessions.session_base(Options.init(), logic, dirs).syntax.keywords
     6.8 +    val keywords = Sessions.session_base(Options.init(), logic, dirs).overall_syntax.keywords
     6.9      val output_path = output getOrElse Path.explode(default_output(logic))
    6.10  
    6.11      Output.writeln(output_path.implode)
     7.1 --- a/src/Tools/jEdit/src/isabelle.scala	Fri Sep 29 21:30:31 2017 +0200
     7.2 +++ b/src/Tools/jEdit/src/isabelle.scala	Fri Sep 29 22:12:32 2017 +0200
     7.3 @@ -50,7 +50,7 @@
     7.4  
     7.5    def mode_syntax(mode: String): Option[Outer_Syntax] =
     7.6      mode match {
     7.7 -      case "isabelle" => Some(PIDE.resources.session_base.syntax)
     7.8 +      case "isabelle" => Some(PIDE.resources.session_base.overall_syntax)
     7.9        case "isabelle-options" => Some(Options.options_syntax)
    7.10        case "isabelle-root" => Some(Sessions.root_syntax)
    7.11        case "isabelle-ml" => Some(ml_syntax)