clarified modules;
authorwenzelm
Wed Mar 15 10:31:42 2017 +0100 (2017-03-15)
changeset 652514b0a43afc3fb
parent 65250 13a6c81534a8
child 65252 8b776d12f6c0
clarified modules;
src/Pure/PIDE/batch_session.scala
src/Pure/Thy/sessions.scala
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
     1.1 --- a/src/Pure/PIDE/batch_session.scala	Wed Mar 15 10:08:27 2017 +0100
     1.2 +++ b/src/Pure/PIDE/batch_session.scala	Wed Mar 15 10:31:42 2017 +0100
     1.3 @@ -28,7 +28,7 @@
     1.4          dirs = dirs, sessions = List(parent_session)).ok)
     1.5        new RuntimeException
     1.6  
     1.7 -    val deps = Build.dependencies(verbose = verbose, tree = session_tree)
     1.8 +    val deps = Sessions.dependencies(verbose = verbose, tree = session_tree)
     1.9      val resources = new Resources(deps(parent_session))
    1.10  
    1.11      val progress = new Console_Progress(verbose = verbose)
     2.1 --- a/src/Pure/Thy/sessions.scala	Wed Mar 15 10:08:27 2017 +0100
     2.2 +++ b/src/Pure/Thy/sessions.scala	Wed Mar 15 10:31:42 2017 +0100
     2.3 @@ -29,7 +29,7 @@
     2.4    }
     2.5  
     2.6  
     2.7 -  /* base info */
     2.8 +  /* base info and source dependencies */
     2.9  
    2.10    object Base
    2.11    {
    2.12 @@ -47,8 +47,117 @@
    2.13      sources: List[(Path, SHA1.Digest)] = Nil,
    2.14      session_graph: Graph_Display.Graph = Graph_Display.empty_graph)
    2.15  
    2.16 +  sealed case class Deps(deps: Map[String, Base])
    2.17 +  {
    2.18 +    def is_empty: Boolean = deps.isEmpty
    2.19 +    def apply(name: String): Base = deps(name)
    2.20 +    def sources(name: String): List[SHA1.Digest] = deps(name).sources.map(_._2)
    2.21 +  }
    2.22  
    2.23 -  /* info */
    2.24 +  def dependencies(
    2.25 +      progress: Progress = No_Progress,
    2.26 +      inlined_files: Boolean = false,
    2.27 +      verbose: Boolean = false,
    2.28 +      list_files: Boolean = false,
    2.29 +      check_keywords: Set[String] = Set.empty,
    2.30 +      tree: Tree): Deps =
    2.31 +    Deps((Map.empty[String, Base] /: tree.topological_order)(
    2.32 +      { case (deps, (name, info)) =>
    2.33 +          if (progress.stopped) throw Exn.Interrupt()
    2.34 +
    2.35 +          try {
    2.36 +            val resources =
    2.37 +              new Resources(
    2.38 +                info.parent match {
    2.39 +                  case None => Base.bootstrap
    2.40 +                  case Some(parent) => deps(parent)
    2.41 +                })
    2.42 +
    2.43 +            if (verbose || list_files) {
    2.44 +              val groups =
    2.45 +                if (info.groups.isEmpty) ""
    2.46 +                else info.groups.mkString(" (", " ", ")")
    2.47 +              progress.echo("Session " + info.chapter + "/" + name + groups)
    2.48 +            }
    2.49 +
    2.50 +            val thy_deps =
    2.51 +            {
    2.52 +              val root_theories =
    2.53 +                info.theories.flatMap({
    2.54 +                  case (global, _, thys) =>
    2.55 +                    thys.map(thy =>
    2.56 +                      (resources.node_name(
    2.57 +                        if (global) "" else name, info.dir + resources.thy_path(thy)), info.pos))
    2.58 +                })
    2.59 +              val thy_deps = resources.thy_info.dependencies(name, root_theories)
    2.60 +
    2.61 +              thy_deps.errors match {
    2.62 +                case Nil => thy_deps
    2.63 +                case errs => error(cat_lines(errs))
    2.64 +              }
    2.65 +            }
    2.66 +
    2.67 +            val known_theories =
    2.68 +              (resources.base.known_theories /: thy_deps.deps)({ case (known, dep) =>
    2.69 +                val name = dep.name
    2.70 +                known.get(name.theory) match {
    2.71 +                  case Some(name1) if name != name1 =>
    2.72 +                    error("Duplicate theory " + quote(name.node) + " vs. " + quote(name1.node))
    2.73 +                  case _ =>
    2.74 +                    known + (name.theory -> name) + (Long_Name.base_name(name.theory) -> name)
    2.75 +                }
    2.76 +              })
    2.77 +
    2.78 +            val loaded_theories = thy_deps.loaded_theories
    2.79 +            val keywords = thy_deps.keywords
    2.80 +            val syntax = thy_deps.syntax
    2.81 +
    2.82 +            val theory_files = thy_deps.deps.map(dep => Path.explode(dep.name.node))
    2.83 +            val loaded_files =
    2.84 +              if (inlined_files) {
    2.85 +                val pure_files =
    2.86 +                  if (pure_name(name)) Sessions.pure_files(resources, syntax, info.dir)
    2.87 +                  else Nil
    2.88 +                pure_files ::: thy_deps.loaded_files
    2.89 +              }
    2.90 +              else Nil
    2.91 +
    2.92 +            val all_files =
    2.93 +              (theory_files ::: loaded_files :::
    2.94 +                info.files.map(file => info.dir + file) :::
    2.95 +                info.document_files.map(file => info.dir + file._1 + file._2)).map(_.expand)
    2.96 +
    2.97 +            if (list_files)
    2.98 +              progress.echo(cat_lines(all_files.map(_.implode).sorted.map("  " + _)))
    2.99 +
   2.100 +            if (check_keywords.nonEmpty)
   2.101 +              Check_Keywords.check_keywords(progress, syntax.keywords, check_keywords, theory_files)
   2.102 +
   2.103 +            val sources = all_files.map(p => (p, SHA1.digest(p.file)))
   2.104 +
   2.105 +            val session_graph =
   2.106 +              Present.session_graph(info.parent getOrElse "",
   2.107 +                resources.base.loaded_theories, thy_deps.deps)
   2.108 +
   2.109 +            val base =
   2.110 +              Base(loaded_theories, known_theories, keywords, syntax, sources, session_graph)
   2.111 +            deps + (name -> base)
   2.112 +          }
   2.113 +          catch {
   2.114 +            case ERROR(msg) =>
   2.115 +              cat_error(msg, "The error(s) above occurred in session " +
   2.116 +                quote(name) + Position.here(info.pos))
   2.117 +          }
   2.118 +      }))
   2.119 +
   2.120 +  def session_base(options: Options, session: String, dirs: List[Path] = Nil): Base =
   2.121 +  {
   2.122 +    val (_, tree) = load(options, dirs = dirs).selection(sessions = List(session))
   2.123 +    dependencies(tree = tree)(session)
   2.124 +  }
   2.125 +
   2.126 +
   2.127 +  /* session tree */
   2.128  
   2.129    sealed case class Info(
   2.130      chapter: String,
   2.131 @@ -67,9 +176,6 @@
   2.132      def timeout: Time = Time.seconds(options.real("timeout") * options.real("timeout_scale"))
   2.133    }
   2.134  
   2.135 -
   2.136 -  /* session tree */
   2.137 -
   2.138    object Tree
   2.139    {
   2.140      def apply(infos: Seq[(String, Info)]): Tree =
     3.1 --- a/src/Pure/Tools/build.scala	Wed Mar 15 10:08:27 2017 +0100
     3.2 +++ b/src/Pure/Tools/build.scala	Wed Mar 15 10:31:42 2017 +0100
     3.3 @@ -93,119 +93,6 @@
     3.4    }
     3.5  
     3.6  
     3.7 -  /* source dependencies and static content */
     3.8 -
     3.9 -  sealed case class Deps(deps: Map[String, Sessions.Base])
    3.10 -  {
    3.11 -    def is_empty: Boolean = deps.isEmpty
    3.12 -    def apply(name: String): Sessions.Base = deps(name)
    3.13 -    def sources(name: String): List[SHA1.Digest] = deps(name).sources.map(_._2)
    3.14 -  }
    3.15 -
    3.16 -  def dependencies(
    3.17 -      progress: Progress = No_Progress,
    3.18 -      inlined_files: Boolean = false,
    3.19 -      verbose: Boolean = false,
    3.20 -      list_files: Boolean = false,
    3.21 -      check_keywords: Set[String] = Set.empty,
    3.22 -      tree: Sessions.Tree): Deps =
    3.23 -    Deps((Map.empty[String, Sessions.Base] /: tree.topological_order)(
    3.24 -      { case (deps, (name, info)) =>
    3.25 -          if (progress.stopped) throw Exn.Interrupt()
    3.26 -
    3.27 -          try {
    3.28 -            val resources =
    3.29 -              new Resources(
    3.30 -                info.parent match {
    3.31 -                  case None => Sessions.Base.bootstrap
    3.32 -                  case Some(parent) => deps(parent)
    3.33 -                })
    3.34 -
    3.35 -            if (verbose || list_files) {
    3.36 -              val groups =
    3.37 -                if (info.groups.isEmpty) ""
    3.38 -                else info.groups.mkString(" (", " ", ")")
    3.39 -              progress.echo("Session " + info.chapter + "/" + name + groups)
    3.40 -            }
    3.41 -
    3.42 -            val thy_deps =
    3.43 -            {
    3.44 -              val root_theories =
    3.45 -                info.theories.flatMap({
    3.46 -                  case (global, _, thys) =>
    3.47 -                    thys.map(thy =>
    3.48 -                      (resources.node_name(
    3.49 -                        if (global) "" else name, info.dir + resources.thy_path(thy)), info.pos))
    3.50 -                })
    3.51 -              val thy_deps = resources.thy_info.dependencies(name, root_theories)
    3.52 -
    3.53 -              thy_deps.errors match {
    3.54 -                case Nil => thy_deps
    3.55 -                case errs => error(cat_lines(errs))
    3.56 -              }
    3.57 -            }
    3.58 -
    3.59 -            val known_theories =
    3.60 -              (resources.base.known_theories /: thy_deps.deps)({ case (known, dep) =>
    3.61 -                val name = dep.name
    3.62 -                known.get(name.theory) match {
    3.63 -                  case Some(name1) if name != name1 =>
    3.64 -                    error("Duplicate theory " + quote(name.node) + " vs. " + quote(name1.node))
    3.65 -                  case _ =>
    3.66 -                    known + (name.theory -> name) + (Long_Name.base_name(name.theory) -> name)
    3.67 -                }
    3.68 -              })
    3.69 -
    3.70 -            val loaded_theories = thy_deps.loaded_theories
    3.71 -            val keywords = thy_deps.keywords
    3.72 -            val syntax = thy_deps.syntax
    3.73 -
    3.74 -            val theory_files = thy_deps.deps.map(dep => Path.explode(dep.name.node))
    3.75 -            val loaded_files =
    3.76 -              if (inlined_files) {
    3.77 -                val pure_files =
    3.78 -                  if (Sessions.pure_name(name)) Sessions.pure_files(resources, syntax, info.dir)
    3.79 -                  else Nil
    3.80 -                pure_files ::: thy_deps.loaded_files
    3.81 -              }
    3.82 -              else Nil
    3.83 -
    3.84 -            val all_files =
    3.85 -              (theory_files ::: loaded_files :::
    3.86 -                info.files.map(file => info.dir + file) :::
    3.87 -                info.document_files.map(file => info.dir + file._1 + file._2)).map(_.expand)
    3.88 -
    3.89 -            if (list_files)
    3.90 -              progress.echo(cat_lines(all_files.map(_.implode).sorted.map("  " + _)))
    3.91 -
    3.92 -            if (check_keywords.nonEmpty)
    3.93 -              Check_Keywords.check_keywords(progress, syntax.keywords, check_keywords, theory_files)
    3.94 -
    3.95 -            val sources = all_files.map(p => (p, SHA1.digest(p.file)))
    3.96 -
    3.97 -            val session_graph =
    3.98 -              Present.session_graph(info.parent getOrElse "",
    3.99 -                resources.base.loaded_theories, thy_deps.deps)
   3.100 -
   3.101 -            val base =
   3.102 -              Sessions.Base(
   3.103 -                loaded_theories, known_theories, keywords, syntax, sources, session_graph)
   3.104 -            deps + (name -> base)
   3.105 -          }
   3.106 -          catch {
   3.107 -            case ERROR(msg) =>
   3.108 -              cat_error(msg, "The error(s) above occurred in session " +
   3.109 -                quote(name) + Position.here(info.pos))
   3.110 -          }
   3.111 -      }))
   3.112 -
   3.113 -  def session_base(options: Options, session: String, dirs: List[Path] = Nil): Sessions.Base =
   3.114 -  {
   3.115 -    val (_, tree) = Sessions.load(options, dirs = dirs).selection(sessions = List(session))
   3.116 -    dependencies(tree = tree)(session)
   3.117 -  }
   3.118 -
   3.119 -
   3.120    /* jobs */
   3.121  
   3.122    private class Job(progress: Progress, name: String, val info: Sessions.Info, tree: Sessions.Tree,
   3.123 @@ -431,7 +318,8 @@
   3.124      val build_options = options.int.update("completion_limit", 0).bool.update("ML_statistics", true)
   3.125      val full_tree = Sessions.load(build_options, dirs, select_dirs)
   3.126      val (selected, selected_tree) = selection(full_tree)
   3.127 -    val deps = dependencies(progress, true, verbose, list_files, check_keywords, selected_tree)
   3.128 +    val deps =
   3.129 +      Sessions.dependencies(progress, true, verbose, list_files, check_keywords, selected_tree)
   3.130  
   3.131      def session_sources_stamp(name: String): String =
   3.132        sources_stamp(selected_tree(name).meta_digest :: deps.sources(name))
     4.1 --- a/src/Tools/VSCode/src/build_vscode.scala	Wed Mar 15 10:08:27 2017 +0100
     4.2 +++ b/src/Tools/VSCode/src/build_vscode.scala	Wed Mar 15 10:31:42 2017 +0100
     4.3 @@ -49,7 +49,7 @@
     4.4    def build_grammar(options: Options, progress: Progress = No_Progress)
     4.5    {
     4.6      val logic = Grammar.default_logic
     4.7 -    val keywords = Build.session_base(options, logic).syntax.keywords
     4.8 +    val keywords = Sessions.session_base(options, logic).syntax.keywords
     4.9  
    4.10      val output_path = extension_dir + Path.explode(Grammar.default_output(logic))
    4.11      progress.echo(output_path.implode)
     5.1 --- a/src/Tools/VSCode/src/grammar.scala	Wed Mar 15 10:08:27 2017 +0100
     5.2 +++ b/src/Tools/VSCode/src/grammar.scala	Wed Mar 15 10:31:42 2017 +0100
     5.3 @@ -159,7 +159,7 @@
     5.4      val more_args = getopts(args)
     5.5      if (more_args.nonEmpty) getopts.usage()
     5.6  
     5.7 -    val keywords = Build.session_base(Options.init(), logic, dirs).syntax.keywords
     5.8 +    val keywords = Sessions.session_base(Options.init(), logic, dirs).syntax.keywords
     5.9      val output_path = output getOrElse Path.explode(default_output(logic))
    5.10  
    5.11      Output.writeln(output_path.implode)
     6.1 --- a/src/Tools/VSCode/src/server.scala	Wed Mar 15 10:08:27 2017 +0100
     6.2 +++ b/src/Tools/VSCode/src/server.scala	Wed Mar 15 10:31:42 2017 +0100
     6.3 @@ -225,7 +225,7 @@
     6.4            }
     6.5          }
     6.6  
     6.7 -        val base = Build.session_base(options, session_name, session_dirs)
     6.8 +        val base = Sessions.session_base(options, session_name, session_dirs)
     6.9          val resources = new VSCode_Resources(options, base, log)
    6.10            {
    6.11              override def commit(change: Session.Change): Unit =
     7.1 --- a/src/Tools/jEdit/src/jedit_sessions.scala	Wed Mar 15 10:08:27 2017 +0100
     7.2 +++ b/src/Tools/jEdit/src/jedit_sessions.scala	Wed Mar 15 10:31:42 2017 +0100
     7.3 @@ -82,7 +82,7 @@
     7.4    def session_base(): Sessions.Base =
     7.5    {
     7.6      val base =
     7.7 -      try { Build.session_base(PIDE.options.value, session_name(), session_dirs()) }
     7.8 +      try { Sessions.session_base(PIDE.options.value, session_name(), session_dirs()) }
     7.9        catch { case ERROR(_) => Sessions.Base.empty }
    7.10      base.copy(known_theories = base.known_theories.mapValues(a => a.map(File.platform_path(_))))
    7.11    }