src/Pure/Thy/sessions.scala
changeset 65519 d244d8f8e13f
parent 65517 1544e61e5314
child 65520 f47bc12b6e8a
     1.1 --- a/src/Pure/Thy/sessions.scala	Wed Apr 19 21:32:46 2017 +0200
     1.2 +++ b/src/Pure/Thy/sessions.scala	Thu Apr 20 10:30:30 2017 +0200
     1.3 @@ -137,7 +137,7 @@
     1.4    {
     1.5      val session_bases =
     1.6        (Map.empty[String, Base] /: sessions.imports_topological_order)({
     1.7 -        case (session_bases, (session_name, info)) =>
     1.8 +        case (session_bases, info) =>
     1.9            if (progress.stopped) throw Exn.Interrupt()
    1.10  
    1.11            try {
    1.12 @@ -151,13 +151,13 @@
    1.13                  Known.make(info.dir, parent_base :: info.imports.map(session_bases(_)), Nil))
    1.14  
    1.15              val resources = new Resources(imports_base,
    1.16 -              default_qualifier = info.theory_qualifier(session_name))
    1.17 +              default_qualifier = info.theory_qualifier(info.name))
    1.18  
    1.19              if (verbose || list_files) {
    1.20                val groups =
    1.21                  if (info.groups.isEmpty) ""
    1.22                  else info.groups.mkString(" (", " ", ")")
    1.23 -              progress.echo("Session " + info.chapter + "/" + session_name + groups)
    1.24 +              progress.echo("Session " + info.chapter + "/" + info.name + groups)
    1.25              }
    1.26  
    1.27              val thy_deps =
    1.28 @@ -165,7 +165,7 @@
    1.29                val root_theories =
    1.30                  info.theories.flatMap({ case (_, thys) =>
    1.31                    thys.map({ case (thy, pos) =>
    1.32 -                    (resources.import_name(session_name, info.dir.implode, thy), pos) })
    1.33 +                    (resources.import_name(info.name, info.dir.implode, thy), pos) })
    1.34                  })
    1.35                val thy_deps = resources.thy_info.dependencies(root_theories)
    1.36  
    1.37 @@ -181,7 +181,7 @@
    1.38              val loaded_files =
    1.39                if (inlined_files) {
    1.40                  val pure_files =
    1.41 -                  if (is_pure(session_name)) {
    1.42 +                  if (is_pure(info.name)) {
    1.43                      val roots = Thy_Header.ml_roots.map(p => info.dir + Path.explode(p._1))
    1.44                      val files =
    1.45                        roots.flatMap(root => resources.loaded_files(syntax, File.read(root))).
    1.46 @@ -212,7 +212,7 @@
    1.47                def node(name: Document.Node.Name): Graph_Display.Node =
    1.48                {
    1.49                  val session = resources.theory_qualifier(name)
    1.50 -                if (session == session_name)
    1.51 +                if (session == info.name)
    1.52                    Graph_Display.Node(name.theory_base_name, "theory." + name.theory)
    1.53                  else session_node(session)
    1.54                }
    1.55 @@ -246,12 +246,12 @@
    1.56                  sources = all_files.map(p => (p, SHA1.digest(p.file))),
    1.57                  session_graph = session_graph)
    1.58  
    1.59 -            session_bases + (session_name -> base)
    1.60 +            session_bases + (info.name -> base)
    1.61            }
    1.62            catch {
    1.63              case ERROR(msg) =>
    1.64                cat_error(msg, "The error(s) above occurred in session " +
    1.65 -                quote(session_name) + Position.here(info.pos))
    1.66 +                quote(info.name) + Position.here(info.pos))
    1.67            }
    1.68        })
    1.69  
    1.70 @@ -283,6 +283,7 @@
    1.71    /* cumulative session info */
    1.72  
    1.73    sealed case class Info(
    1.74 +    name: String,
    1.75      chapter: String,
    1.76      select: Boolean,
    1.77      pos: Position.T,
    1.78 @@ -416,10 +417,11 @@
    1.79      def global_theories: Map[String, String] =
    1.80        (Thy_Header.bootstrap_global_theories.toMap /:
    1.81          (for {
    1.82 -          (session_name, (info, _)) <- imports_graph.iterator
    1.83 -          thy <- info.global_theories.iterator } yield (thy, session_name, info)))({
    1.84 -            case (global, (thy, session_name, info)) =>
    1.85 -              val qualifier = info.theory_qualifier(session_name)
    1.86 +          (_, (info, _)) <- imports_graph.iterator
    1.87 +          thy <- info.global_theories.iterator }
    1.88 +         yield (thy, info)))({
    1.89 +            case (global, (thy, info)) =>
    1.90 +              val qualifier = info.theory_qualifier(info.name)
    1.91                global.get(thy) match {
    1.92                  case Some(qualifier1) if qualifier != qualifier1 =>
    1.93                    error("Duplicate global theory " + quote(thy) + Position.here(info.pos))
    1.94 @@ -440,11 +442,11 @@
    1.95      def build_descendants(names: List[String]): List[String] =
    1.96        build_graph.all_succs(names)
    1.97  
    1.98 -    def build_topological_order: List[(String, Info)] =
    1.99 -      build_graph.topological_order.map(name => (name, apply(name)))
   1.100 +    def build_topological_order: List[Info] =
   1.101 +      build_graph.topological_order.map(apply(_))
   1.102  
   1.103 -    def imports_topological_order: List[(String, Info)] =
   1.104 -      imports_graph.topological_order.map(name => (name, apply(name)))
   1.105 +    def imports_topological_order: List[Info] =
   1.106 +      imports_graph.topological_order.map(apply(_))
   1.107  
   1.108      override def toString: String =
   1.109        imports_graph.keys_iterator.mkString("Sessions.T(", ", ", ")")
   1.110 @@ -579,9 +581,9 @@
   1.111                entry.imports, entry.theories, entry.files, entry.document_files).toString)
   1.112  
   1.113            val info =
   1.114 -            Info(entry_chapter, select, entry.pos, entry.groups, dir + Path.explode(entry.path),
   1.115 -              entry.parent, entry.description, session_options, entry.imports, theories,
   1.116 -              global_theories, files, document_files, meta_digest)
   1.117 +            Info(name, entry_chapter, select, entry.pos, entry.groups,
   1.118 +              dir + Path.explode(entry.path), entry.parent, entry.description, session_options,
   1.119 +              entry.imports, theories, global_theories, files, document_files, meta_digest)
   1.120  
   1.121            (name, info)
   1.122          }