clarified signature, notably cascade of dump_options, deps, resources, session;
authorwenzelm
Sat Dec 29 17:37:02 2018 +0100 (7 months ago ago)
changeset 69550faf547d2834c
parent 69549 b8e8a724182b
child 69551 da2726f78610
clarified signature, notably cascade of dump_options, deps, resources, session;
src/Pure/PIDE/headless.scala
src/Pure/Tools/dump.scala
     1.1 --- a/src/Pure/PIDE/headless.scala	Sat Dec 29 16:13:05 2018 +0100
     1.2 +++ b/src/Pure/PIDE/headless.scala	Sat Dec 29 17:37:02 2018 +0100
     1.3 @@ -433,12 +433,13 @@
     1.4    {
     1.5      resources =>
     1.6  
     1.7 +    def options: Options = session_base_info.options
     1.8 +
     1.9  
    1.10      /* session */
    1.11  
    1.12      def start_session(print_mode: List[String] = Nil, progress: Progress = No_Progress): Session =
    1.13      {
    1.14 -      val options = session_base_info.options
    1.15        val session = new Session(session_base_info.session, options, resources)
    1.16  
    1.17        val session_error = Future.promise[String]
     2.1 --- a/src/Pure/Tools/dump.scala	Sat Dec 29 16:13:05 2018 +0100
     2.2 +++ b/src/Pure/Tools/dump.scala	Sat Dec 29 17:37:02 2018 +0100
     2.3 @@ -73,28 +73,41 @@
     2.4        error("Unknown aspect " + quote(name))
     2.5  
     2.6  
     2.7 -  /* session */
     2.8 +  /* dependencies */
     2.9  
    2.10 -  def session(dump_options: Options, logic: String,
    2.11 -    process_theory: (Sessions.Deps, Document.Snapshot, Document_Status.Node_Status) => Unit,
    2.12 +  def used_theories(options: Options, deps: Sessions.Deps, progress: Progress = No_Progress)
    2.13 +    : List[Document.Node.Name] =
    2.14 +  {
    2.15 +    deps.used_theories_condition(options, progress.echo_warning).map(_._2)
    2.16 +  }
    2.17 +
    2.18 +  def dependencies(
    2.19 +    options: Options,
    2.20      progress: Progress = No_Progress,
    2.21 -    log: Logger = No_Logger,
    2.22      dirs: List[Path] = Nil,
    2.23      select_dirs: List[Path] = Nil,
    2.24      selection: Sessions.Selection = Sessions.Selection.empty)
    2.25 +      : (Sessions.Deps, List[Document.Node.Name]) =
    2.26    {
    2.27 -    /* dependencies */
    2.28 -
    2.29      val deps =
    2.30 -      Sessions.load_structure(dump_options, dirs = dirs, select_dirs = select_dirs).
    2.31 -        selection_deps(dump_options, selection, progress = progress,
    2.32 +      Sessions.load_structure(options, dirs = dirs, select_dirs = select_dirs).
    2.33 +        selection_deps(options, selection, progress = progress,
    2.34            uniform_session = true, loading_sessions = true)
    2.35  
    2.36 -    val use_theories =
    2.37 -      for { (_, name) <- deps.used_theories_condition(dump_options, progress.echo_warning) }
    2.38 -      yield name.theory
    2.39 +    val theories = used_theories(options, deps, progress = progress)
    2.40 +
    2.41 +    (deps, theories)
    2.42 +  }
    2.43  
    2.44  
    2.45 +  /* session */
    2.46 +
    2.47 +  def session(
    2.48 +    deps: Sessions.Deps,
    2.49 +    resources: Headless.Resources,
    2.50 +    process_theory: (Sessions.Deps, Document.Snapshot, Document_Status.Node_Status) => Unit,
    2.51 +    progress: Progress = No_Progress)
    2.52 +  {
    2.53      /* asynchronous consumer */
    2.54  
    2.55      object Consumer
    2.56 @@ -149,14 +162,9 @@
    2.57  
    2.58      /* run session */
    2.59  
    2.60 -    val resources =
    2.61 -      Headless.Resources.make(dump_options, logic, progress = progress, log = log,
    2.62 -        session_dirs = dirs ::: select_dirs,
    2.63 -        include_sessions = deps.sessions_structure.imports_topological_order)
    2.64 -
    2.65      val session = resources.start_session(progress = progress)
    2.66 -
    2.67      try {
    2.68 +      val use_theories = used_theories(resources.options, deps).map(_.theory)
    2.69        val use_theories_result =
    2.70          session.use_theories(use_theories, progress = progress, commit = Some(Consumer.apply _))
    2.71  
    2.72 @@ -209,17 +217,22 @@
    2.73  
    2.74      val dump_options = make_options(options, aspects)
    2.75  
    2.76 -    def process_theory(
    2.77 -      deps: Sessions.Deps,
    2.78 -      snapshot: Document.Snapshot,
    2.79 -      status: Document_Status.Node_Status)
    2.80 -    {
    2.81 -      val aspect_args = Aspect_Args(dump_options, progress, deps, output_dir, snapshot, status)
    2.82 -      aspects.foreach(_.operation(aspect_args))
    2.83 -    }
    2.84 +    val deps =
    2.85 +      dependencies(dump_options, progress = progress,
    2.86 +        dirs = dirs, select_dirs = select_dirs, selection = selection)._1
    2.87  
    2.88 -    session(dump_options, logic, process_theory _,
    2.89 -      progress = progress, log = log, dirs = dirs, select_dirs = select_dirs, selection = selection)
    2.90 +    val resources =
    2.91 +      Headless.Resources.make(dump_options, logic, progress = progress, log = log,
    2.92 +        session_dirs = dirs ::: select_dirs,
    2.93 +        include_sessions = deps.sessions_structure.imports_topological_order)
    2.94 +
    2.95 +    session(deps, resources, progress = progress,
    2.96 +      process_theory =
    2.97 +        (deps: Sessions.Deps, snapshot: Document.Snapshot, status: Document_Status.Node_Status) =>
    2.98 +        {
    2.99 +          val aspect_args = Aspect_Args(dump_options, progress, deps, output_dir, snapshot, status)
   2.100 +          aspects.foreach(_.operation(aspect_args))
   2.101 +        })
   2.102    }
   2.103  
   2.104