clarified signature;
authorwenzelm
Sun Mar 03 19:12:28 2019 +0100 (7 weeks ago ago)
changeset 70038a4b430ad848a
parent 70037 bb41977edb7e
child 70039 3d0f27273aa1
clarified signature;
suppress already loaded theories;
src/Pure/PIDE/headless.scala
src/Pure/Thy/sessions.scala
src/Pure/Tools/dump.scala
     1.1 --- a/src/Pure/PIDE/headless.scala	Sun Mar 03 18:45:08 2019 +0100
     1.2 +++ b/src/Pure/PIDE/headless.scala	Sun Mar 03 19:12:28 2019 +0100
     1.3 @@ -483,6 +483,18 @@
     1.4      def options: Options = session_base_info.options
     1.5  
     1.6  
     1.7 +    /* dependencies */
     1.8 +
     1.9 +    def used_theories(
    1.10 +      deps: Sessions.Deps, progress: Progress = No_Progress): List[Document.Node.Name] =
    1.11 +    {
    1.12 +      for {
    1.13 +        (_, name) <- deps.used_theories_condition(options, progress = progress)
    1.14 +        if !session_base.loaded_theory(name)
    1.15 +      } yield name
    1.16 +    }
    1.17 +
    1.18 +
    1.19      /* session */
    1.20  
    1.21      def start_session(print_mode: List[String] = Nil, progress: Progress = No_Progress): Session =
     2.1 --- a/src/Pure/Thy/sessions.scala	Sun Mar 03 18:45:08 2019 +0100
     2.2 +++ b/src/Pure/Thy/sessions.scala	Sun Mar 03 19:12:28 2019 +0100
     2.3 @@ -200,7 +200,7 @@
     2.4      def imported_sources(name: String): List[SHA1.Digest] =
     2.5        session_bases(name).imported_sources.map(_._2)
     2.6  
     2.7 -    def used_theories_condition(default_options: Options, warning: String => Unit = _ => ())
     2.8 +    def used_theories_condition(default_options: Options, progress: Progress = No_Progress)
     2.9        : List[(Options, Document.Node.Name)] =
    2.10      {
    2.11        val default_skip_proofs = default_options.bool("skip_proofs")
    2.12 @@ -208,7 +208,8 @@
    2.13          session_name <- sessions_structure.build_topological_order
    2.14          (options, name) <- session_bases(session_name).used_theories
    2.15          if {
    2.16 -          def warn(msg: String): Unit = warning("Skipping theory " + name + "  (" + msg + ")")
    2.17 +          def warn(msg: String): Unit =
    2.18 +            progress.echo_warning("Skipping theory " + name + "  (" + msg + ")")
    2.19  
    2.20            val conditions =
    2.21              space_explode(',', options.string("condition")).
     3.1 --- a/src/Pure/Tools/dump.scala	Sun Mar 03 18:45:08 2019 +0100
     3.2 +++ b/src/Pure/Tools/dump.scala	Sun Mar 03 19:12:28 2019 +0100
     3.3 @@ -87,12 +87,6 @@
     3.4          uniform_session = true, loading_sessions = true)
     3.5    }
     3.6  
     3.7 -  def used_theories(options: Options, deps: Sessions.Deps, progress: Progress = No_Progress)
     3.8 -    : List[Document.Node.Name] =
     3.9 -  {
    3.10 -    deps.used_theories_condition(options, progress.echo_warning).map(_._2)
    3.11 -  }
    3.12 -
    3.13  
    3.14    /* session */
    3.15  
    3.16 @@ -158,7 +152,7 @@
    3.17  
    3.18      val session = resources.start_session(progress = progress)
    3.19      try {
    3.20 -      val use_theories = used_theories(resources.options, deps).map(_.theory)
    3.21 +      val use_theories = resources.used_theories(deps).map(_.theory)
    3.22        val use_theories_result =
    3.23          session.use_theories(use_theories, progress = progress, commit = Some(Consumer.apply _))
    3.24