src/Pure/PIDE/document_info.scala

clarified modules;

/*  Title:      Pure/PIDE/document_info.scala
    Author:     Makarius

Persistent document information --- for presentation purposes.
*/

package isabelle


object Document_Info {
  sealed case class Session(
    name: String,
    used_theories: List[String],
    loaded_theories: Map[String, Theory])

  object Theory {
    def apply(
      name: String,
      files: List[String],
      static_session: String,
      dynamic_session: String,
      entities: List[Export_Theory.Entity0],
      others: List[String]
    ): Theory = {
      val entities1 =
        entities.filter(e => e.file.nonEmpty && Position.Range.unapply(e.pos).isDefined)
      new Theory(name, files, static_session, dynamic_session, entities1, others)
    }
  }

  class Theory private(
    val name: String,
    val files: List[String],
    val static_session: String,
    val dynamic_session: String,
    entities: List[Export_Theory.Entity0],
    others: List[String]
  ) {
    override def toString: String = name

    val (thy_file, blobs_files) =
      files match {
        case Nil => error("Unknown theory file for " + quote(name))
        case a :: bs =>
          def for_theory: String = " for theory " + quote(name)
          if (!File.is_thy(a)) error("Bad .thy file " + quote(a) + for_theory)
          for (b <- bs if File.is_thy(b)) error("Bad auxiliary file " + quote(b) + for_theory)
          (a, bs)
      }

    def home_session: Boolean = static_session == dynamic_session

    def print_short: String =
      if (home_session) Long_Name.base_name(name) else name

    def print_long: String =
      "theory " + quote(name) +
      (if (home_session) "" else " (session " + quote(dynamic_session) + ")")

    private lazy val by_file_range: Map[(String, Symbol.Range), List[Export_Theory.Entity0]] =
      entities.groupBy(entity => (entity.file, entity.range))

    private lazy val by_file_kname: Map[(String, String), Export_Theory.Entity0] =
      (for {
        entity <- entities
        file <- Position.File.unapply(entity.pos)
      } yield (file, entity.kname) -> entity).toMap

    def get_defs(file: String, range: Symbol.Range): List[Export_Theory.Entity0] =
      by_file_range.getOrElse((file, range), Nil)

    def get_def(file: String, kind: String, name: String): Option[Export_Theory.Entity0] =
      by_file_kname.get((file, Export_Theory.export_kind_name(kind, name)))

    def elements(elements: Presentation.Elements): Presentation.Elements =
      elements.copy(entity = others.foldLeft(elements.entity)(_ + _))
  }

  val empty: Document_Info = new Document_Info(Map.empty)

  def read(
    database_context: Export.Database_Context,
    deps: Sessions.Deps,
    sessions: List[String]
  ): Document_Info = {
    val sessions_domain = sessions.toSet
    val sessions_structure = deps.sessions_structure
    val sessions_requirements = sessions_structure.build_requirements(sessions)

    def read_theory(theory_context: Export.Theory_Context): Document_Info.Theory =
    {
      val session_name = theory_context.session_context.session_name
      val theory_name = theory_context.theory

      val files = theory_context.files0(permissive = true)

      val (entities, others) =
        if (sessions_domain(session_name)) {
          val theory = Export_Theory.read_theory(theory_context, permissive = true)
          (theory.entity_iterator.toList,
           theory.others.keySet.toList)
        }
        else (Nil, Nil)

      Theory(theory_name,
        static_session = sessions_structure.theory_qualifier(theory_name),
        dynamic_session = session_name,
        files = files,
        entities = entities,
        others = others)
    }

    def read_session(session_name: String): Document_Info.Session = {
      val used_theories = deps(session_name).used_theories.map(_._1.theory)
      val loaded_theories0 =
        using(database_context.open_session(deps.base_info(session_name))) { session_context =>
          for (theory_name <- used_theories)
            yield theory_name -> read_theory(session_context.theory(theory_name))
        }
      Session(session_name, used_theories, loaded_theories0.toMap)
    }

    val result0 =
      (for (session <- Par_List.map(read_session, sessions_requirements).iterator)
        yield session.name -> session).toMap

    val result1 =
      sessions_requirements.foldLeft(Map.empty[String, Session]) {
        case (seen, session_name) =>
          val session0 = result0(session_name)
          val loaded_theories1 =
            sessions_structure(session_name).parent.map(seen) match {
              case None => session0.loaded_theories
              case Some(parent_session) =>
                parent_session.loaded_theories ++ session0.loaded_theories
            }
          val session1 = session0.copy(loaded_theories = loaded_theories1)
          seen + (session_name -> session1)
      }

    new Document_Info(result1)
  }
}

class Document_Info private(sessions: Map[String, Document_Info.Session]) {
  override def toString: String =
    sessions.keysIterator.toList.sorted.mkString("Document_Info(", ", ", ")")

  def the_session(session: String): Document_Info.Session =
    sessions.getOrElse(session,
      error("Unknown document information for session: " + quote(session)))

  def theory_by_name(session: String, theory: String): Option[Document_Info.Theory] =
    by_session_and_theory_name.get((session, theory))

  def theory_by_file(session: String, file: String): Option[Document_Info.Theory] =
    by_session_and_theory_file.get((session, file))

  private lazy val by_session_and_theory_name: Map[(String, String), Document_Info.Theory] =
    (for {
      session <- sessions.valuesIterator
      theory <- session.loaded_theories.valuesIterator
    } yield (session.name, theory.name) -> theory).toMap

  private lazy val by_session_and_theory_file: Map[(String, String), Document_Info.Theory] = {
    (for {
      session <- sessions.valuesIterator
      theory <- session.loaded_theories.valuesIterator
      file <- theory.files.iterator
    } yield (session.name, file) -> theory).toMap
  }
}