tuned signature;
authorwenzelm
Mon Mar 13 15:59:00 2017 +0100 (2017-03-13)
changeset 652108cfdf420b643
parent 65209 eb89ad5ae115
child 65211 73ba79126b55
tuned signature;
src/Pure/Tools/build.scala
src/Tools/VSCode/src/build_vscode.scala
src/Tools/VSCode/src/grammar.scala
src/Tools/VSCode/src/server.scala
src/Tools/jEdit/src/jedit_sessions.scala
src/Tools/jEdit/src/plugin.scala
     1.1 --- a/src/Pure/Tools/build.scala	Mon Mar 13 15:32:19 2017 +0100
     1.2 +++ b/src/Pure/Tools/build.scala	Mon Mar 13 15:59:00 2017 +0100
     1.3 @@ -211,16 +211,13 @@
     1.4  
     1.5    def session_base(
     1.6      options: Options,
     1.7 -    inlined_files: Boolean,
     1.8 -    dirs: List[Path],
     1.9 -    session: String): Sessions.Base =
    1.10 +    session_name: String,
    1.11 +    session_dirs: List[Path] = Nil,
    1.12 +    inlined_files: Boolean = false): Sessions.Base =
    1.13    {
    1.14 -    session_dependencies(options, inlined_files, dirs, List(session))(session)
    1.15 +    session_dependencies(options, inlined_files, session_dirs, List(session_name))(session_name)
    1.16    }
    1.17  
    1.18 -  def outer_syntax(options: Options, dirs: List[Path], session: String): Outer_Syntax =
    1.19 -    session_base(options, false, dirs, session).syntax
    1.20 -
    1.21  
    1.22    /* jobs */
    1.23  
     2.1 --- a/src/Tools/VSCode/src/build_vscode.scala	Mon Mar 13 15:32:19 2017 +0100
     2.2 +++ b/src/Tools/VSCode/src/build_vscode.scala	Mon Mar 13 15:59:00 2017 +0100
     2.3 @@ -49,7 +49,7 @@
     2.4    def build_grammar(options: Options, progress: Progress = No_Progress)
     2.5    {
     2.6      val logic = Grammar.default_logic
     2.7 -    val keywords = Build.outer_syntax(options, Nil, logic).keywords
     2.8 +    val keywords = Build.session_base(options, logic).syntax.keywords
     2.9  
    2.10      val output_path = extension_dir + Path.explode(Grammar.default_output(logic))
    2.11      progress.echo(output_path.implode)
     3.1 --- a/src/Tools/VSCode/src/grammar.scala	Mon Mar 13 15:32:19 2017 +0100
     3.2 +++ b/src/Tools/VSCode/src/grammar.scala	Mon Mar 13 15:59:00 2017 +0100
     3.3 @@ -159,7 +159,7 @@
     3.4      val more_args = getopts(args)
     3.5      if (more_args.nonEmpty) getopts.usage()
     3.6  
     3.7 -    val keywords = Build.outer_syntax(Options.init(), dirs, logic).keywords
     3.8 +    val keywords = Build.session_base(Options.init(), logic, dirs).syntax.keywords
     3.9      val output_path = output getOrElse Path.explode(default_output(logic))
    3.10  
    3.11      Output.writeln(output_path.implode)
     4.1 --- a/src/Tools/VSCode/src/server.scala	Mon Mar 13 15:32:19 2017 +0100
     4.2 +++ b/src/Tools/VSCode/src/server.scala	Mon Mar 13 15:59:00 2017 +0100
     4.3 @@ -212,7 +212,7 @@
     4.4            }
     4.5          }
     4.6  
     4.7 -        val base = Build.session_base(options, false, session_dirs, session_name)
     4.8 +        val base = Build.session_base(options, session_name, session_dirs)
     4.9          val resources = new VSCode_Resources(options, base, log)
    4.10            {
    4.11              override def commit(change: Session.Change): Unit =
     5.1 --- a/src/Tools/jEdit/src/jedit_sessions.scala	Mon Mar 13 15:32:19 2017 +0100
     5.2 +++ b/src/Tools/jEdit/src/jedit_sessions.scala	Mon Mar 13 15:59:00 2017 +0100
     5.3 @@ -79,10 +79,10 @@
     5.4      main_sessions.map(_._1).sorted ::: other_sessions.map(_._1).sorted
     5.5    }
     5.6  
     5.7 -  def session_base(inlined_files: Boolean): Sessions.Base =
     5.8 +  def session_base(): Sessions.Base =
     5.9    {
    5.10      val base =
    5.11 -      try { Build.session_base(PIDE.options.value, inlined_files, session_dirs(), session_name()) }
    5.12 +      try { Build.session_base(PIDE.options.value, session_name(), session_dirs()) }
    5.13        catch { case ERROR(_) => Sessions.Base.empty }
    5.14      base.copy(known_theories = base.known_theories.mapValues(a => a.map(File.platform_path(_))))
    5.15    }
     6.1 --- a/src/Tools/jEdit/src/plugin.scala	Mon Mar 13 15:32:19 2017 +0100
     6.2 +++ b/src/Tools/jEdit/src/plugin.scala	Mon Mar 13 15:59:00 2017 +0100
     6.3 @@ -389,7 +389,7 @@
     6.4  
     6.5        JEdit_Lib.jedit_text_areas.foreach(Completion_Popup.Text_Area.init _)
     6.6  
     6.7 -      val resources = new JEdit_Resources(JEdit_Sessions.session_base(false))
     6.8 +      val resources = new JEdit_Resources(JEdit_Sessions.session_base())
     6.9  
    6.10        PIDE.session.stop()
    6.11        PIDE.session = new Session(resources) {