src/Pure/Thy/sessions.scala
changeset 70683 8c7706b053c7
parent 70681 a6c0f2d106c8
child 70684 60b1eda998f3
equal deleted inserted replaced
70682:4c53227f4b73 70683:8c7706b053c7
    39   object Known
    39   object Known
    40   {
    40   {
    41     val empty: Known = Known()
    41     val empty: Known = Known()
    42 
    42 
    43     def make(local_dir: Path, bases: List[Base],
    43     def make(local_dir: Path, bases: List[Base],
    44       sessions: List[(String, Position.T)] = Nil,
       
    45       theories: List[Document.Node.Entry] = Nil,
    44       theories: List[Document.Node.Entry] = Nil,
    46       loaded_files: List[(String, List[Path])] = Nil): Known =
    45       loaded_files: List[(String, List[Path])] = Nil): Known =
    47     {
    46     {
    48       def bases_iterator(local: Boolean) =
    47       def bases_iterator(local: Boolean) =
    49         for {
    48         for {
    55       {
    54       {
    56         val local_path = local_dir.canonical_file.toPath
    55         val local_path = local_dir.canonical_file.toPath
    57         theories.iterator.filter(entry =>
    56         theories.iterator.filter(entry =>
    58           entry.name.path.canonical_file.toPath.startsWith(local_path))
    57           entry.name.path.canonical_file.toPath.startsWith(local_path))
    59       }
    58       }
    60 
       
    61       val known_sessions =
       
    62         (sessions.toMap /: bases)({ case (known, base) => known ++ base.known.sessions })
       
    63 
    59 
    64       val known_theories =
    60       val known_theories =
    65         (Map.empty[String, Document.Node.Entry] /: (bases_iterator(false) ++ theories.iterator))({
    61         (Map.empty[String, Document.Node.Entry] /: (bases_iterator(false) ++ theories.iterator))({
    66           case (known, entry) =>
    62           case (known, entry) =>
    67             known.get(entry.name.theory) match {
    63             known.get(entry.name.theory) match {
    90 
    86 
    91       val known_loaded_files =
    87       val known_loaded_files =
    92         (loaded_files.toMap /: bases.map(base => base.known.loaded_files))(_ ++ _)
    88         (loaded_files.toMap /: bases.map(base => base.known.loaded_files))(_ ++ _)
    93 
    89 
    94       Known(
    90       Known(
    95         known_sessions,
       
    96         known_theories,
    91         known_theories,
    97         known_theories_local,
    92         known_theories_local,
    98         known_files.iterator.map(p => (p._1, p._2.reverse)).toMap,
    93         known_files.iterator.map(p => (p._1, p._2.reverse)).toMap,
    99         known_loaded_files)
    94         known_loaded_files)
   100     }
    95     }
   101   }
    96   }
   102 
    97 
   103   sealed case class Known(
    98   sealed case class Known(
   104     sessions: Map[String, Position.T] = Map.empty,
       
   105     theories: Map[String, Document.Node.Entry] = Map.empty,
    99     theories: Map[String, Document.Node.Entry] = Map.empty,
   106     theories_local: Map[String, Document.Node.Entry] = Map.empty,
   100     theories_local: Map[String, Document.Node.Entry] = Map.empty,
   107     files: Map[JFile, List[Document.Node.Name]] = Map.empty,
   101     files: Map[JFile, List[Document.Node.Name]] = Map.empty,
   108     loaded_files: Map[String, List[Path]] = Map.empty)
   102     loaded_files: Map[String, List[Path]] = Map.empty)
   109   {
   103   {
   178       loaded_theory_syntax(name.theory)
   172       loaded_theory_syntax(name.theory)
   179 
   173 
   180     def node_syntax(nodes: Document.Nodes, name: Document.Node.Name): Outer_Syntax =
   174     def node_syntax(nodes: Document.Nodes, name: Document.Node.Name): Outer_Syntax =
   181       nodes(name).syntax orElse loaded_theory_syntax(name) getOrElse overall_syntax
   175       nodes(name).syntax orElse loaded_theory_syntax(name) getOrElse overall_syntax
   182 
   176 
   183     def known_theory(name: String): Option[Document.Node.Name] =
       
   184       known.theories.get(name).map(_.name)
       
   185 
       
   186     def dest_known_theories: List[(String, String)] =
   177     def dest_known_theories: List[(String, String)] =
   187       for ((theory, entry) <- known.theories.toList)
   178       for ((theory, entry) <- known.theories.toList)
   188         yield (theory, entry.name.node)
   179         yield (theory, entry.name.node)
   189 
   180 
   190     def get_imports: Base =
   181     def get_imports: Base =
   302               }
   293               }
   303             val imports_base: Sessions.Base =
   294             val imports_base: Sessions.Base =
   304               parent_base.copy(known =
   295               parent_base.copy(known =
   305                 Known.make(info.dir, parent_base :: info.imports.map(session_bases(_))))
   296                 Known.make(info.dir, parent_base :: info.imports.map(session_bases(_))))
   306 
   297 
   307             val resources = new Resources(imports_base)
   298             val resources = new Resources(sessions_structure, imports_base)
   308 
   299 
   309             if (verbose || list_files) {
   300             if (verbose || list_files) {
   310               val groups =
   301               val groups =
   311                 if (info.groups.isEmpty) ""
   302                 if (info.groups.isEmpty) ""
   312                 else info.groups.mkString(" (", " ", ")")
   303                 else info.groups.mkString(" (", " ", ")")
   369                     ((g /: (a :: bs))(_.default_node(_, Nil)) /: bs)(_.add_edge(_, a)) })
   360                     ((g /: (a :: bs))(_.default_node(_, Nil)) /: bs)(_.add_edge(_, a)) })
   370             }
   361             }
   371 
   362 
   372             val known =
   363             val known =
   373               Known.make(info.dir, List(imports_base),
   364               Known.make(info.dir, List(imports_base),
   374                 sessions = List(info.name -> info.pos),
       
   375                 theories = dependencies.entries,
   365                 theories = dependencies.entries,
   376                 loaded_files = loaded_files)
   366                 loaded_files = loaded_files)
   377 
   367 
   378             val used_theories =
   368             val used_theories =
   379               for ((options, name) <- dependencies.adjunct_theories)
   369               for ((options, name) <- dependencies.adjunct_theories)
   464     session: String,
   454     session: String,
   465     progress: Progress = No_Progress,
   455     progress: Progress = No_Progress,
   466     dirs: List[Path] = Nil,
   456     dirs: List[Path] = Nil,
   467     include_sessions: List[String] = Nil,
   457     include_sessions: List[String] = Nil,
   468     session_ancestor: Option[String] = None,
   458     session_ancestor: Option[String] = None,
   469     session_requirements: Boolean = false,
   459     session_requirements: Boolean = false): Base_Info =
   470     session_focus: Boolean = false,
       
   471     all_known: Boolean = false): Base_Info =
       
   472   {
   460   {
   473     val full_sessions = load_structure(options, dirs = dirs)
   461     val full_sessions = load_structure(options, dirs = dirs)
   474 
   462 
   475     val selected_sessions =
   463     val selected_sessions =
   476       full_sessions.selection(Selection(sessions = session :: session_ancestor.toList))
   464       full_sessions.selection(Selection(sessions = session :: session_ancestor.toList))
   527     val full_sessions1 =
   515     val full_sessions1 =
   528       if (infos1.isEmpty) full_sessions
   516       if (infos1.isEmpty) full_sessions
   529       else load_structure(options, dirs = dirs, infos = infos1)
   517       else load_structure(options, dirs = dirs, infos = infos1)
   530 
   518 
   531     val selected_sessions1 =
   519     val selected_sessions1 =
   532     {
   520       full_sessions1.selection(Selection(sessions = session1 :: session :: include_sessions))
   533       val sel_sessions1 = session1 :: session :: include_sessions
   521 
   534       val select_sessions1 =
   522     val deps1 = Sessions.deps(selected_sessions1, progress = progress)
   535         if (session_focus) {
   523 
   536           full_sessions1.check_sessions(sel_sessions1)
   524     Base_Info(options, dirs, session1, full_sessions1, deps1.errors, deps1(session1), infos1)
   537           full_sessions1.imports_descendants(sel_sessions1)
       
   538         }
       
   539         else sel_sessions1
       
   540       full_sessions1.selection(Selection(sessions = select_sessions1))
       
   541     }
       
   542 
       
   543     val sessions1 = if (all_known) full_sessions1 else selected_sessions1
       
   544     val deps1 = Sessions.deps(sessions1, progress = progress)
       
   545     val base1 = deps1(session1).copy(known = deps1.all_known)
       
   546 
       
   547     Base_Info(options, dirs, session1, deps1.sessions_structure, deps1.errors, base1, infos1)
       
   548   }
   525   }
   549 
   526 
   550 
   527 
   551   /* cumulative session info */
   528   /* cumulative session info */
   552 
   529 
   698               Position.here(graph.get_node(info.name).pos))
   675               Position.here(graph.get_node(info.name).pos))
   699           else graph.new_node(info.name, info)
   676           else graph.new_node(info.name, info)
   700       }
   677       }
   701     val build_graph = add_edges(info_graph, "parent", _.parent)
   678     val build_graph = add_edges(info_graph, "parent", _.parent)
   702     val imports_graph = add_edges(build_graph, "imports", _.imports)
   679     val imports_graph = add_edges(build_graph, "imports", _.imports)
       
   680 
       
   681     val session_positions: List[(String, Position.T)] =
       
   682       (for ((name, (info, _)) <- info_graph.iterator) yield (name, info.pos)).toList
   703 
   683 
   704     val session_directories: Map[JFile, String] =
   684     val session_directories: Map[JFile, String] =
   705       (Map.empty[JFile, String] /:
   685       (Map.empty[JFile, String] /:
   706         (for {
   686         (for {
   707           session <- imports_graph.topological_order.iterator
   687           session <- imports_graph.topological_order.iterator
   733                 error("Duplicate global theory " + quote(thy) + Position.here(info.pos))
   713                 error("Duplicate global theory " + quote(thy) + Position.here(info.pos))
   734               case _ => global + (thy -> qualifier)
   714               case _ => global + (thy -> qualifier)
   735             }
   715             }
   736           })
   716           })
   737 
   717 
   738     new Structure(session_directories, global_theories, build_graph, imports_graph)
   718     new Structure(
       
   719       session_positions, session_directories, global_theories, build_graph, imports_graph)
   739   }
   720   }
   740 
   721 
   741   final class Structure private[Sessions](
   722   final class Structure private[Sessions](
       
   723       val session_positions: List[(String, Position.T)],
   742       val session_directories: Map[JFile, String],
   724       val session_directories: Map[JFile, String],
   743       val global_theories: Map[String, String],
   725       val global_theories: Map[String, String],
   744       val build_graph: Graph[String, Info],
   726       val build_graph: Graph[String, Info],
   745       val imports_graph: Graph[String, Info])
   727       val imports_graph: Graph[String, Info])
   746   {
   728   {
   747     sessions_structure =>
   729     sessions_structure =>
       
   730 
       
   731     def dest_session_directories: List[(String, String)] =
       
   732       for ((file, session) <- session_directories.toList)
       
   733         yield (File.standard_path(file), session)
   748 
   734 
   749     lazy val chapters: SortedMap[String, List[Info]] =
   735     lazy val chapters: SortedMap[String, List[Info]] =
   750       (SortedMap.empty[String, List[Info]] /: build_graph.iterator)(
   736       (SortedMap.empty[String, List[Info]] /: build_graph.iterator)(
   751         { case (chs, (_, (info, _))) =>
   737         { case (chs, (_, (info, _))) =>
   752             chs + (info.chapter -> (info :: chs.getOrElse(info.chapter, Nil))) })
   738             chs + (info.chapter -> (info :: chs.getOrElse(info.chapter, Nil))) })
   809         val sessions = graph.all_preds(selected(graph, sel)).filterNot(excluded)
   795         val sessions = graph.all_preds(selected(graph, sel)).filterNot(excluded)
   810         graph.restrict(graph.all_preds(sessions).toSet)
   796         graph.restrict(graph.all_preds(sessions).toSet)
   811       }
   797       }
   812 
   798 
   813       new Structure(
   799       new Structure(
   814         session_directories, global_theories, restrict(build_graph), restrict(imports_graph))
   800         session_positions, session_directories, global_theories,
       
   801         restrict(build_graph), restrict(imports_graph))
   815     }
   802     }
   816 
   803 
   817     def selection_deps(
   804     def selection_deps(
   818       options: Options,
   805       options: Options,
   819       selection: Selection,
   806       selection: Selection,