tuned signature;
authorwenzelm
Wed Nov 01 16:43:51 2017 +0100 (18 months ago)
changeset 66976806bc39550a5
parent 66975 ca73d44d51aa
child 66977 fa79f18eadc7
tuned signature;
src/Pure/ML/ml_console.scala
src/Pure/Thy/sessions.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
     1.1 --- a/src/Pure/ML/ml_console.scala	Wed Nov 01 16:38:15 2017 +0100
     1.2 +++ b/src/Pure/ML/ml_console.scala	Wed Nov 01 16:43:51 2017 +0100
     1.3 @@ -75,7 +75,7 @@
     1.4            raw_ml_system = raw_ml_system, store = Sessions.store(system_mode),
     1.5            session_base =
     1.6              if (raw_ml_system) None
     1.7 -            else Some(Sessions.session_base_info(options, logic, dirs).check_base))
     1.8 +            else Some(Sessions.base_info(options, logic, dirs).check_base))
     1.9        val process_output = Future.thread[Unit]("process_output") {
    1.10          try {
    1.11            var result = new StringBuilder(100)
     2.1 --- a/src/Pure/Thy/sessions.scala	Wed Nov 01 16:38:15 2017 +0100
     2.2 +++ b/src/Pure/Thy/sessions.scala	Wed Nov 01 16:43:51 2017 +0100
     2.3 @@ -335,9 +335,7 @@
     2.4      def check_base: Base = if (errors.isEmpty) base else error(cat_lines(errors))
     2.5    }
     2.6  
     2.7 -  def session_base_info(
     2.8 -    options: Options,
     2.9 -    session: String,
    2.10 +  def base_info(options: Options, session: String,
    2.11      dirs: List[Path] = Nil,
    2.12      all_known: Boolean = false,
    2.13      required_session: Boolean = false): Base_Info =
     3.1 --- a/src/Tools/VSCode/src/build_vscode.scala	Wed Nov 01 16:38:15 2017 +0100
     3.2 +++ b/src/Tools/VSCode/src/build_vscode.scala	Wed Nov 01 16:43:51 2017 +0100
     3.3 @@ -20,7 +20,7 @@
     3.4    def build_grammar(options: Options, progress: Progress = No_Progress)
     3.5    {
     3.6      val logic = Grammar.default_logic
     3.7 -    val keywords = Sessions.session_base_info(options, logic).check_base.overall_syntax.keywords
     3.8 +    val keywords = Sessions.base_info(options, logic).check_base.overall_syntax.keywords
     3.9  
    3.10      val output_path = extension_dir + Path.explode(Grammar.default_output(logic))
    3.11      progress.echo(output_path.implode)
     4.1 --- a/src/Tools/VSCode/src/grammar.scala	Wed Nov 01 16:38:15 2017 +0100
     4.2 +++ b/src/Tools/VSCode/src/grammar.scala	Wed Nov 01 16:43:51 2017 +0100
     4.3 @@ -158,7 +158,7 @@
     4.4      if (more_args.nonEmpty) getopts.usage()
     4.5  
     4.6      val keywords =
     4.7 -      Sessions.session_base_info(Options.init(), logic, dirs).check_base.overall_syntax.keywords
     4.8 +      Sessions.base_info(Options.init(), logic, dirs).check_base.overall_syntax.keywords
     4.9      val output_path = output getOrElse Path.explode(default_output(logic))
    4.10  
    4.11      Output.writeln(output_path.implode)
     5.1 --- a/src/Tools/VSCode/src/server.scala	Wed Nov 01 16:38:15 2017 +0100
     5.2 +++ b/src/Tools/VSCode/src/server.scala	Wed Nov 01 16:43:51 2017 +0100
     5.3 @@ -269,7 +269,7 @@
     5.4          }
     5.5  
     5.6          val session_base =
     5.7 -          Sessions.session_base_info(
     5.8 +          Sessions.base_info(
     5.9              options, session_name, dirs = session_dirs, all_known = all_known).check_base
    5.10          val resources = new VSCode_Resources(options, session_base, log)
    5.11            {
     6.1 --- a/src/Tools/jEdit/src/jedit_sessions.scala	Wed Nov 01 16:38:15 2017 +0100
     6.2 +++ b/src/Tools/jEdit/src/jedit_sessions.scala	Wed Nov 01 16:43:51 2017 +0100
     6.3 @@ -59,7 +59,7 @@
     6.4    {
     6.5      val logic = logic_name(options)
     6.6  
     6.7 -    Sessions.session_base_info(options,
     6.8 +    Sessions.base_info(options,
     6.9        if (logic_parent) logic_info(options).flatMap(_.parent) getOrElse logic else logic,
    6.10        dirs = JEdit_Sessions.session_dirs(),
    6.11        all_known = true,