refer to global_theories from all sessions, before selection;
authorwenzelm
Tue Apr 04 19:40:47 2017 +0200 (2017-04-04)
changeset 65372b722ee40c26c
parent 65371 ce09e947c1d5
child 65373 905ed0102c69
refer to global_theories from all sessions, before selection;
src/Pure/PIDE/resources.scala
src/Pure/Thy/sessions.scala
src/Pure/Tools/build.scala
     1.1 --- a/src/Pure/PIDE/resources.scala	Tue Apr 04 18:43:58 2017 +0200
     1.2 +++ b/src/Pure/PIDE/resources.scala	Tue Apr 04 19:40:47 2017 +0200
     1.3 @@ -67,12 +67,16 @@
     1.4      }
     1.5      else Nil
     1.6  
     1.7 -  def init_name(global: Boolean, raw_path: Path): Document.Node.Name =
     1.8 +  def qualify(name: String): String =
     1.9 +    if (Long_Name.is_qualified(name)) error("Bad qualified theory name " + quote(name))
    1.10 +    else if (session_base.global_theories.contains(name)) name
    1.11 +    else Long_Name.qualify(session_name, name)
    1.12 +
    1.13 +  def init_name(raw_path: Path): Document.Node.Name =
    1.14    {
    1.15      val path = raw_path.expand
    1.16      val node = path.implode
    1.17 -    val qualifier = if (global) "" else session_name
    1.18 -    val theory = Long_Name.qualify(qualifier, Thy_Header.thy_name(node).getOrElse(""))
    1.19 +    val theory = qualify(Thy_Header.thy_name(node).getOrElse(""))
    1.20      val master_dir = if (theory == "") "" else path.dir.implode
    1.21      Document.Node.Name(node, master_dir, theory)
    1.22    }
     2.1 --- a/src/Pure/Thy/sessions.scala	Tue Apr 04 18:43:58 2017 +0200
     2.2 +++ b/src/Pure/Thy/sessions.scala	Tue Apr 04 19:40:47 2017 +0200
     2.3 @@ -30,6 +30,7 @@
     2.4    }
     2.5  
     2.6    sealed case class Base(
     2.7 +    global_theories: Set[String] = Set.empty,
     2.8      loaded_theories: Set[String] = Set.empty,
     2.9      known_theories: Map[String, Document.Node.Name] = Map.empty,
    2.10      keywords: Thy_Header.Keywords = Nil,
    2.11 @@ -54,7 +55,9 @@
    2.12        verbose: Boolean = false,
    2.13        list_files: Boolean = false,
    2.14        check_keywords: Set[String] = Set.empty,
    2.15 +      global_theories: Set[String] = Set.empty,
    2.16        tree: Tree): Deps =
    2.17 +  {
    2.18      Deps((Map.empty[String, Base] /: tree.topological_order)(
    2.19        { case (deps, (name, info)) =>
    2.20            if (progress.stopped) throw Exn.Interrupt()
    2.21 @@ -78,9 +81,9 @@
    2.22              {
    2.23                val root_theories =
    2.24                  info.theories.flatMap({
    2.25 -                  case (global, _, thys) =>
    2.26 +                  case (_, _, thys) =>
    2.27                      thys.map(thy =>
    2.28 -                      (resources.init_name(global, info.dir + resources.thy_path(thy)), info.pos))
    2.29 +                      (resources.init_name(info.dir + resources.thy_path(thy)), info.pos))
    2.30                  })
    2.31                val thy_deps = resources.thy_info.dependencies(root_theories)
    2.32  
    2.33 @@ -132,14 +135,17 @@
    2.34              if (check_keywords.nonEmpty)
    2.35                Check_Keywords.check_keywords(progress, syntax.keywords, check_keywords, theory_files)
    2.36  
    2.37 -            val sources = all_files.map(p => (p, SHA1.digest(p.file)))
    2.38 +            val base =
    2.39 +              Base(global_theories = global_theories,
    2.40 +                loaded_theories = loaded_theories,
    2.41 +                known_theories = known_theories,
    2.42 +                keywords = keywords,
    2.43 +                syntax = syntax,
    2.44 +                sources = all_files.map(p => (p, SHA1.digest(p.file))),
    2.45 +                session_graph =
    2.46 +                  Present.session_graph(info.parent getOrElse "",
    2.47 +                    parent_base.loaded_theories, thy_deps.deps))
    2.48  
    2.49 -            val session_graph =
    2.50 -              Present.session_graph(info.parent getOrElse "",
    2.51 -                parent_base.loaded_theories, thy_deps.deps)
    2.52 -
    2.53 -            val base =
    2.54 -              Base(loaded_theories, known_theories, keywords, syntax, sources, session_graph)
    2.55              deps + (name -> base)
    2.56            }
    2.57            catch {
    2.58 @@ -148,11 +154,14 @@
    2.59                  quote(name) + Position.here(info.pos))
    2.60            }
    2.61        }))
    2.62 +  }
    2.63  
    2.64    def session_base(options: Options, session: String, dirs: List[Path] = Nil): Base =
    2.65    {
    2.66 -    val (_, tree) = load(options, dirs = dirs).selection(sessions = List(session))
    2.67 -    dependencies(tree = tree)(session)
    2.68 +    val full_tree = load(options, dirs = dirs)
    2.69 +    val (_, tree) = full_tree.selection(sessions = List(session))
    2.70 +
    2.71 +    dependencies(global_theories = full_tree.global_theories, tree = tree)(session)
    2.72    }
    2.73  
    2.74  
    2.75 @@ -173,6 +182,10 @@
    2.76      meta_digest: SHA1.Digest)
    2.77    {
    2.78      def timeout: Time = Time.seconds(options.real("timeout") * options.real("timeout_scale"))
    2.79 +
    2.80 +    def global_theories: List[String] =
    2.81 +      for { (global, _, paths) <- theories if global; path <- paths }
    2.82 +      yield path.base.implode
    2.83    }
    2.84  
    2.85    object Tree
    2.86 @@ -207,6 +220,7 @@
    2.87                  }
    2.88              }
    2.89          }
    2.90 +
    2.91        new Tree(graph2)
    2.92      }
    2.93    }
    2.94 @@ -217,6 +231,12 @@
    2.95      def apply(name: String): Info = graph.get_node(name)
    2.96      def isDefinedAt(name: String): Boolean = graph.defined(name)
    2.97  
    2.98 +    def global_theories: Set[String] =
    2.99 +      (for {
   2.100 +        (_, (info, _)) <- graph.iterator
   2.101 +        name <- info.global_theories.iterator }
   2.102 +       yield name).toSet
   2.103 +
   2.104      def selection(
   2.105        requirements: Boolean = false,
   2.106        all_sessions: Boolean = false,
     3.1 --- a/src/Pure/Tools/build.scala	Tue Apr 04 18:43:58 2017 +0200
     3.2 +++ b/src/Pure/Tools/build.scala	Tue Apr 04 19:40:47 2017 +0200
     3.3 @@ -396,7 +396,9 @@
     3.4      val full_tree = Sessions.load(build_options, dirs, select_dirs)
     3.5      val (selected, selected_tree) = selection(full_tree)
     3.6      val deps =
     3.7 -      Sessions.dependencies(progress, true, verbose, list_files, check_keywords, selected_tree)
     3.8 +      Sessions.dependencies(
     3.9 +        progress, true, verbose, list_files, check_keywords,
    3.10 +          full_tree.global_theories, selected_tree)
    3.11  
    3.12      def sources_stamp(name: String): List[String] =
    3.13        (selected_tree(name).meta_digest :: deps.sources(name)).map(_.toString).sorted