support for static session imports, without affect build hierarchy;
authorwenzelm
Fri Apr 07 11:50:49 2017 +0200 (2017-04-07)
changeset 65420695d4e22345a
parent 65419 457e4fbed731
child 65421 6389e3ec32ec
support for static session imports, without affect build hierarchy;
src/Pure/Admin/build_doc.scala
src/Pure/Thy/sessions.scala
src/Pure/Tools/build.scala
src/Pure/Tools/ml_process.scala
src/Tools/jEdit/src/jedit_sessions.scala
     1.1 --- a/src/Pure/Admin/build_doc.scala	Fri Apr 07 10:47:25 2017 +0200
     1.2 +++ b/src/Pure/Admin/build_doc.scala	Fri Apr 07 11:50:49 2017 +0200
     1.3 @@ -24,7 +24,7 @@
     1.4    {
     1.5      val selection =
     1.6        for {
     1.7 -        (name, info) <- Sessions.load(options).topological_order
     1.8 +        (name, info) <- Sessions.load(options).build_topological_order
     1.9          if info.groups.contains("doc")
    1.10          doc = info.options.string("document_variants")
    1.11          if all_docs || docs.contains(doc)
     2.1 --- a/src/Pure/Thy/sessions.scala	Fri Apr 07 10:47:25 2017 +0200
     2.2 +++ b/src/Pure/Thy/sessions.scala	Fri Apr 07 11:50:49 2017 +0200
     2.3 @@ -57,7 +57,7 @@
     2.4        check_keywords: Set[String] = Set.empty,
     2.5        global_theories: Set[String] = Set.empty): Deps =
     2.6    {
     2.7 -    Deps((Map.empty[String, Base] /: sessions.topological_order)({
     2.8 +    Deps((Map.empty[String, Base] /: sessions.imports_topological_order)({
     2.9        case (sessions, (name, info)) =>
    2.10          if (progress.stopped) throw Exn.Interrupt()
    2.11  
    2.12 @@ -173,6 +173,7 @@
    2.13      parent: Option[String],
    2.14      description: String,
    2.15      options: Options,
    2.16 +    imports: List[String],
    2.17      theories: List[(Options, List[String])],
    2.18      global_theories: List[String],
    2.19      files: List[Path],
    2.20 @@ -235,7 +236,29 @@
    2.21  
    2.22    def make(infos: Traversable[(String, Info)]): T =
    2.23    {
    2.24 -    val graph1 =
    2.25 +    def add_edges(graph: Graph[String, Info], kind: String, edges: Info => Traversable[String])
    2.26 +      : Graph[String, Info] =
    2.27 +    {
    2.28 +      def add_edge(pos: Position.T, name: String, g: Graph[String, Info], parent: String) =
    2.29 +      {
    2.30 +        if (!g.defined(parent))
    2.31 +          error("Bad " + kind + " session " + quote(parent) + " for " +
    2.32 +            quote(name) + Position.here(pos))
    2.33 +
    2.34 +        try { g.add_edge_acyclic(parent, name) }
    2.35 +        catch {
    2.36 +          case exn: Graph.Cycles[_] =>
    2.37 +            error(cat_lines(exn.cycles.map(cycle =>
    2.38 +              "Cyclic session dependency of " +
    2.39 +                cycle.map(c => quote(c.toString)).mkString(" via "))) + Position.here(pos))
    2.40 +        }
    2.41 +      }
    2.42 +      (graph /: graph.iterator) {
    2.43 +        case (g, (name, (info, _))) => (g /: edges(info))(add_edge(info.pos, name, _, _))
    2.44 +      }
    2.45 +    }
    2.46 +
    2.47 +    val graph0 =
    2.48        (Graph.string[Info] /: infos) {
    2.49          case (graph, (name, info)) =>
    2.50            if (graph.defined(name))
    2.51 @@ -243,55 +266,47 @@
    2.52                Position.here(graph.get_node(name).pos))
    2.53            else graph.new_node(name, info)
    2.54        }
    2.55 -    val graph2 =
    2.56 -      (graph1 /: graph1.iterator) {
    2.57 -        case (graph, (name, (info, _))) =>
    2.58 -          info.parent match {
    2.59 -            case None => graph
    2.60 -            case Some(parent) =>
    2.61 -              if (!graph.defined(parent))
    2.62 -                error("Bad parent session " + quote(parent) + " for " +
    2.63 -                  quote(name) + Position.here(info.pos))
    2.64 +    val graph1 = add_edges(graph0, "parent", _.parent)
    2.65 +    val graph2 = add_edges(graph1, "imports", _.imports)
    2.66  
    2.67 -              try { graph.add_edge_acyclic(parent, name) }
    2.68 -              catch {
    2.69 -                case exn: Graph.Cycles[_] =>
    2.70 -                  error(cat_lines(exn.cycles.map(cycle =>
    2.71 -                    "Cyclic session dependency of " +
    2.72 -                      cycle.map(c => quote(c.toString)).mkString(" via "))) +
    2.73 -                        Position.here(info.pos))
    2.74 -              }
    2.75 -          }
    2.76 -      }
    2.77 -
    2.78 -    new T(graph2)
    2.79 +    new T(graph1, graph2)
    2.80    }
    2.81  
    2.82 -  final class T private[Sessions](val graph: Graph[String, Info])
    2.83 -    extends PartialFunction[String, Info]
    2.84 +  final class T private[Sessions](
    2.85 +      val build_graph: Graph[String, Info],
    2.86 +      val imports_graph: Graph[String, Info])
    2.87    {
    2.88 -    def apply(name: String): Info = graph.get_node(name)
    2.89 -    def isDefinedAt(name: String): Boolean = graph.defined(name)
    2.90 +    def apply(name: String): Info = imports_graph.get_node(name)
    2.91 +    def get(name: String): Option[Info] =
    2.92 +      if (imports_graph.defined(name)) Some(imports_graph.get_node(name)) else None
    2.93  
    2.94      def global_theories: Set[String] =
    2.95        (for {
    2.96 -        (_, (info, _)) <- graph.iterator
    2.97 +        (_, (info, _)) <- imports_graph.iterator
    2.98          name <- info.global_theories.iterator }
    2.99         yield name).toSet
   2.100  
   2.101      def selection(select: Selection): (List[String], T) =
   2.102      {
   2.103 -      val (selected, graph1) = select(graph)
   2.104 -      (selected, new T(graph1))
   2.105 +      val (_, build_graph1) = select(build_graph)
   2.106 +      val (selected, imports_graph1) = select(imports_graph)
   2.107 +      (selected, new T(build_graph1, imports_graph1))
   2.108      }
   2.109  
   2.110 -    def ancestors(name: String): List[String] =
   2.111 -      graph.all_preds(List(name)).tail.reverse
   2.112 +    def build_ancestors(name: String): List[String] =
   2.113 +      build_graph.all_preds(List(name)).tail.reverse
   2.114 +
   2.115 +    def build_descendants(names: List[String]): List[String] =
   2.116 +      build_graph.all_succs(names)
   2.117  
   2.118 -    def topological_order: List[(String, Info)] =
   2.119 -      graph.topological_order.map(name => (name, apply(name)))
   2.120 +    def build_topological_order: List[(String, Info)] =
   2.121 +      build_graph.topological_order.map(name => (name, apply(name)))
   2.122  
   2.123 -    override def toString: String = graph.keys_iterator.mkString("Sessions.T(", ", ", ")")
   2.124 +    def imports_topological_order: List[(String, Info)] =
   2.125 +      imports_graph.topological_order.map(name => (name, apply(name)))
   2.126 +
   2.127 +    override def toString: String =
   2.128 +      imports_graph.keys_iterator.mkString("Sessions.T(", ", ", ")")
   2.129    }
   2.130  
   2.131  
   2.132 @@ -305,6 +320,7 @@
   2.133    private val IN = "in"
   2.134    private val DESCRIPTION = "description"
   2.135    private val OPTIONS = "options"
   2.136 +  private val SESSIONS = "sessions"
   2.137    private val THEORIES = "theories"
   2.138    private val GLOBAL = "global"
   2.139    private val FILES = "files"
   2.140 @@ -316,6 +332,7 @@
   2.141        (SESSION, Keyword.THY_DECL) +
   2.142        (DESCRIPTION, Keyword.QUASI_COMMAND) +
   2.143        (OPTIONS, Keyword.QUASI_COMMAND) +
   2.144 +      (SESSIONS, Keyword.QUASI_COMMAND) +
   2.145        (THEORIES, Keyword.QUASI_COMMAND) +
   2.146        (FILES, Keyword.QUASI_COMMAND) +
   2.147        (DOCUMENT_FILES, Keyword.QUASI_COMMAND)
   2.148 @@ -332,6 +349,7 @@
   2.149        parent: Option[String],
   2.150        description: String,
   2.151        options: List[Options.Spec],
   2.152 +      imports: List[String],
   2.153        theories: List[(List[Options.Spec], List[(String, Boolean)])],
   2.154        files: List[String],
   2.155        document_files: List[(String, String)]) extends Entry
   2.156 @@ -377,11 +395,12 @@
   2.157              (opt(session_name ~! $$$("+") ^^ { case x ~ _ => x }) ~
   2.158                (($$$(DESCRIPTION) ~! text ^^ { case _ ~ x => x }) | success("")) ~
   2.159                (($$$(OPTIONS) ~! options ^^ { case _ ~ x => x }) | success(Nil)) ~
   2.160 +              (($$$(SESSIONS) ~! rep(session_name)  ^^ { case _ ~ x => x }) | success(Nil)) ~
   2.161                rep1(theories) ~
   2.162                (($$$(FILES) ~! rep1(path) ^^ { case _ ~ x => x }) | success(Nil)) ~
   2.163                (rep(document_files) ^^ (x => x.flatten))))) ^^
   2.164 -        { case _ ~ ((a, pos) ~ b ~ c ~ (_ ~ (d ~ e ~ f ~ g ~ h ~ i))) =>
   2.165 -            Session_Entry(pos, a, b, c, d, e, f, g, h, i) }
   2.166 +        { case _ ~ ((a, pos) ~ b ~ c ~ (_ ~ (d ~ e ~ f ~ g ~ h ~ i ~ j))) =>
   2.167 +            Session_Entry(pos, a, b, c, d, e, f, g, h, i, j) }
   2.168      }
   2.169  
   2.170      def parse(options: Options, select: Boolean, dir: Path): List[(String, Info)] =
   2.171 @@ -415,12 +434,12 @@
   2.172  
   2.173            val meta_digest =
   2.174              SHA1.digest((entry_chapter, name, entry.parent, entry.options,
   2.175 -              entry.theories, entry.files, entry.document_files).toString)
   2.176 +              entry.imports, entry.theories, entry.files, entry.document_files).toString)
   2.177  
   2.178            val info =
   2.179              Info(entry_chapter, select, entry.pos, entry.groups, dir + Path.explode(entry.path),
   2.180 -              entry.parent, entry.description, session_options, theories, global_theories,
   2.181 -              files, document_files, meta_digest)
   2.182 +              entry.parent, entry.description, session_options, entry.imports, theories,
   2.183 +              global_theories, files, document_files, meta_digest)
   2.184  
   2.185            (name, info)
   2.186          }
     3.1 --- a/src/Pure/Tools/build.scala	Fri Apr 07 10:47:25 2017 +0200
     3.2 +++ b/src/Pure/Tools/build.scala	Fri Apr 07 11:50:49 2017 +0200
     3.3 @@ -65,7 +65,7 @@
     3.4  
     3.5      def apply(sessions: Sessions.T, store: Sessions.Store): Queue =
     3.6      {
     3.7 -      val graph = sessions.graph
     3.8 +      val graph = sessions.build_graph
     3.9        val names = graph.keys
    3.10  
    3.11        val timings = names.map(name => (name, load_timings(store, name)))
    3.12 @@ -413,7 +413,7 @@
    3.13  
    3.14      // optional cleanup
    3.15      if (clean_build) {
    3.16 -      for (name <- full_sessions.graph.all_succs(selected)) {
    3.17 +      for (name <- full_sessions.build_descendants(selected)) {
    3.18          val files =
    3.19            List(Path.basic(name), store.database(name), store.log(name), store.log_gz(name)).
    3.20              map(store.output_dir + _).filter(_.is_file)
    3.21 @@ -519,7 +519,7 @@
    3.22              //{{{ check/start next job
    3.23              pending.dequeue(running.isDefinedAt(_)) match {
    3.24                case Some((name, info)) =>
    3.25 -                val ancestor_results = selected_sessions.ancestors(name).map(results(_))
    3.26 +                val ancestor_results = selected_sessions.build_ancestors(name).map(results(_))
    3.27                  val ancestor_heaps = ancestor_results.flatMap(_.heap_stamp)
    3.28  
    3.29                  val do_output = build_heap || Sessions.is_pure(name) || queue.is_inner(name)
     4.1 --- a/src/Pure/Tools/ml_process.scala	Fri Apr 07 10:47:25 2017 +0200
     4.2 +++ b/src/Pure/Tools/ml_process.scala	Fri Apr 07 11:50:49 2017 +0200
     4.3 @@ -33,7 +33,7 @@
     4.4          val selection = Sessions.Selection(sessions = List(logic_name))
     4.5          val (_, selected_sessions) =
     4.6            sessions.getOrElse(Sessions.load(options, dirs)).selection(selection)
     4.7 -        (selected_sessions.ancestors(logic_name) ::: List(logic_name)).
     4.8 +        (selected_sessions.build_ancestors(logic_name) ::: List(logic_name)).
     4.9            map(a => File.platform_path(store.heap(a)))
    4.10        }
    4.11  
     5.1 --- a/src/Tools/jEdit/src/jedit_sessions.scala	Fri Apr 07 10:47:25 2017 +0200
     5.2 +++ b/src/Tools/jEdit/src/jedit_sessions.scala	Fri Apr 07 11:50:49 2017 +0200
     5.3 @@ -41,7 +41,7 @@
     5.4        tree <-
     5.5          try { Some(Sessions.load(session_options(options), dirs = session_dirs())) }
     5.6          catch { case ERROR(_) => None }
     5.7 -      info <- tree.lift(logic)
     5.8 +      info <- tree.get(logic)
     5.9        parent <- info.parent
    5.10        if Isabelle_System.getenv("JEDIT_LOGIC_ROOT") == "true"
    5.11      } yield Info(parent, info.pos)) getOrElse Info(logic, Position.none)
    5.12 @@ -77,7 +77,7 @@
    5.13    {
    5.14      val session_tree = Sessions.load(options, dirs = session_dirs())
    5.15      val (main_sessions, other_sessions) =
    5.16 -      session_tree.topological_order.partition(p => p._2.groups.contains("main"))
    5.17 +      session_tree.imports_topological_order.partition(p => p._2.groups.contains("main"))
    5.18      main_sessions.map(_._1).sorted ::: other_sessions.map(_._1).sorted
    5.19    }
    5.20