src/Pure/Thy/sessions.scala
changeset 65499 fc7f03cbccbc
parent 65498 2af863e28204
child 65500 a6644e0e8728
equal deleted inserted replaced
65498:2af863e28204 65499:fc7f03cbccbc
    31     def make(local_dir: Path, bases: List[Base], theories: List[Document.Node.Name]): Known =
    31     def make(local_dir: Path, bases: List[Base], theories: List[Document.Node.Name]): Known =
    32     {
    32     {
    33       def bases_iterator(local: Boolean) =
    33       def bases_iterator(local: Boolean) =
    34         for {
    34         for {
    35           base <- bases.iterator
    35           base <- bases.iterator
    36           known = base.known
    36           (_, name) <- (if (local) base.known.theories_local else base.known.theories).iterator
    37           (_, name) <- (if (local) known.known_theories_local else known.known_theories).iterator
       
    38         } yield name
    37         } yield name
    39 
    38 
    40       def local_theories_iterator =
    39       def local_theories_iterator =
    41       {
    40       {
    42         val local_path = local_dir.file.getCanonicalFile.toPath
    41         val local_path = local_dir.file.getCanonicalFile.toPath
    72         known_files.iterator.map(p => (p._1, p._2.reverse)).toMap)
    71         known_files.iterator.map(p => (p._1, p._2.reverse)).toMap)
    73     }
    72     }
    74   }
    73   }
    75 
    74 
    76   sealed case class Known(
    75   sealed case class Known(
    77     known_theories: Map[String, Document.Node.Name] = Map.empty,
    76     theories: Map[String, Document.Node.Name] = Map.empty,
    78     known_theories_local: Map[String, Document.Node.Name] = Map.empty,
    77     theories_local: Map[String, Document.Node.Name] = Map.empty,
    79     known_files: Map[JFile, List[Document.Node.Name]] = Map.empty)
    78     files: Map[JFile, List[Document.Node.Name]] = Map.empty)
    80   {
    79   {
    81     def platform_path: Known =
    80     def platform_path: Known =
    82       copy(
    81       copy(theories = for ((a, b) <- theories) yield (a, b.map(File.platform_path(_))),
    83         known_theories =
    82         theories_local = for ((a, b) <- theories_local) yield (a, b.map(File.platform_path(_))),
    84           for ((a, b) <- known_theories) yield (a, b.map(File.platform_path(_))),
    83         files = for ((a, b) <- files) yield (a, b.map(c => c.map(File.platform_path(_)))))
    85         known_theories_local =
       
    86           for ((a, b) <- known_theories_local) yield (a, b.map(File.platform_path(_))),
       
    87         known_files =
       
    88           for ((a, b) <- known_files) yield (a, b.map(c => c.map(File.platform_path(_)))))
       
    89   }
    84   }
    90 
    85 
    91   object Base
    86   object Base
    92   {
    87   {
    93     def pure(options: Options): Base = session_base(options, Thy_Header.PURE)
    88     def pure(options: Options): Base = session_base(options, Thy_Header.PURE)
   112 
   107 
   113     def loaded_theory(name: Document.Node.Name): Boolean =
   108     def loaded_theory(name: Document.Node.Name): Boolean =
   114       loaded_theories.isDefinedAt(name.theory)
   109       loaded_theories.isDefinedAt(name.theory)
   115 
   110 
   116     def known_theory(name: String): Option[Document.Node.Name] =
   111     def known_theory(name: String): Option[Document.Node.Name] =
   117       known.known_theories.get(name)
   112       known.theories.get(name)
   118 
   113 
   119     def known_file(file: JFile): Option[Document.Node.Name] =
   114     def known_file(file: JFile): Option[Document.Node.Name] =
   120       known.known_files.getOrElse(file, Nil).headOption
   115       known.files.getOrElse(file, Nil).headOption
   121 
   116 
   122     def dest_known_theories: List[(String, String)] =
   117     def dest_known_theories: List[(String, String)] =
   123       for ((theory, node_name) <- known.known_theories.toList)
   118       for ((theory, node_name) <- known.theories.toList)
   124         yield (theory, node_name.node)
   119         yield (theory, node_name.node)
   125   }
   120   }
   126 
   121 
   127   sealed case class Deps(session_bases: Map[String, Base], all_known: Known)
   122   sealed case class Deps(session_bases: Map[String, Base], all_known: Known)
   128   {
   123   {