src/Pure/Thy/thy_info.scala
author wenzelm
Tue, 05 Jul 2011 22:39:15 +0200
changeset 43673 29eb1cd29961
parent 43652 dcd0b667f73d
child 43674 3ddaa75c669c
permissions -rw-r--r--
Thy_Info.dependencies: ignore already loaded theories, according to initial prover session status;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
43651
511df47bcadc some support for theory files within Isabelle/Scala session;
wenzelm
parents:
diff changeset
     1
/*  Title:      Pure/Thy/thy_info.scala
511df47bcadc some support for theory files within Isabelle/Scala session;
wenzelm
parents:
diff changeset
     2
    Author:     Makarius
511df47bcadc some support for theory files within Isabelle/Scala session;
wenzelm
parents:
diff changeset
     3
511df47bcadc some support for theory files within Isabelle/Scala session;
wenzelm
parents:
diff changeset
     4
Theory and file dependencies.
511df47bcadc some support for theory files within Isabelle/Scala session;
wenzelm
parents:
diff changeset
     5
*/
511df47bcadc some support for theory files within Isabelle/Scala session;
wenzelm
parents:
diff changeset
     6
511df47bcadc some support for theory files within Isabelle/Scala session;
wenzelm
parents:
diff changeset
     7
package isabelle
511df47bcadc some support for theory files within Isabelle/Scala session;
wenzelm
parents:
diff changeset
     8
511df47bcadc some support for theory files within Isabelle/Scala session;
wenzelm
parents:
diff changeset
     9
43673
29eb1cd29961 Thy_Info.dependencies: ignore already loaded theories, according to initial prover session status;
wenzelm
parents: 43652
diff changeset
    10
object Thy_Info
29eb1cd29961 Thy_Info.dependencies: ignore already loaded theories, according to initial prover session status;
wenzelm
parents: 43652
diff changeset
    11
{
29eb1cd29961 Thy_Info.dependencies: ignore already loaded theories, according to initial prover session status;
wenzelm
parents: 43652
diff changeset
    12
  /* protocol messages */
29eb1cd29961 Thy_Info.dependencies: ignore already loaded theories, according to initial prover session status;
wenzelm
parents: 43652
diff changeset
    13
29eb1cd29961 Thy_Info.dependencies: ignore already loaded theories, according to initial prover session status;
wenzelm
parents: 43652
diff changeset
    14
  object Loaded_Theory {
29eb1cd29961 Thy_Info.dependencies: ignore already loaded theories, according to initial prover session status;
wenzelm
parents: 43652
diff changeset
    15
    def unapply(msg: XML.Tree): Option[String] =
29eb1cd29961 Thy_Info.dependencies: ignore already loaded theories, according to initial prover session status;
wenzelm
parents: 43652
diff changeset
    16
      msg match {
29eb1cd29961 Thy_Info.dependencies: ignore already loaded theories, according to initial prover session status;
wenzelm
parents: 43652
diff changeset
    17
        case XML.Elem(Markup(Markup.LOADED_THEORY, List((Markup.NAME, name))), _) => Some(name)
29eb1cd29961 Thy_Info.dependencies: ignore already loaded theories, according to initial prover session status;
wenzelm
parents: 43652
diff changeset
    18
        case _ => None
29eb1cd29961 Thy_Info.dependencies: ignore already loaded theories, according to initial prover session status;
wenzelm
parents: 43652
diff changeset
    19
      }
29eb1cd29961 Thy_Info.dependencies: ignore already loaded theories, according to initial prover session status;
wenzelm
parents: 43652
diff changeset
    20
  }
29eb1cd29961 Thy_Info.dependencies: ignore already loaded theories, according to initial prover session status;
wenzelm
parents: 43652
diff changeset
    21
}
29eb1cd29961 Thy_Info.dependencies: ignore already loaded theories, according to initial prover session status;
wenzelm
parents: 43652
diff changeset
    22
29eb1cd29961 Thy_Info.dependencies: ignore already loaded theories, according to initial prover session status;
wenzelm
parents: 43652
diff changeset
    23
43651
511df47bcadc some support for theory files within Isabelle/Scala session;
wenzelm
parents:
diff changeset
    24
class Thy_Info(thy_load: Thy_Load)
511df47bcadc some support for theory files within Isabelle/Scala session;
wenzelm
parents:
diff changeset
    25
{
511df47bcadc some support for theory files within Isabelle/Scala session;
wenzelm
parents:
diff changeset
    26
  /* messages */
511df47bcadc some support for theory files within Isabelle/Scala session;
wenzelm
parents:
diff changeset
    27
511df47bcadc some support for theory files within Isabelle/Scala session;
wenzelm
parents:
diff changeset
    28
  private def show_path(names: List[String]): String =
43652
dcd0b667f73d pervasive Basic_Library in Scala;
wenzelm
parents: 43651
diff changeset
    29
    names.map(quote).mkString(" via ")
43651
511df47bcadc some support for theory files within Isabelle/Scala session;
wenzelm
parents:
diff changeset
    30
511df47bcadc some support for theory files within Isabelle/Scala session;
wenzelm
parents:
diff changeset
    31
  private def cycle_msg(names: List[String]): String =
511df47bcadc some support for theory files within Isabelle/Scala session;
wenzelm
parents:
diff changeset
    32
    "Cyclic dependency of " + show_path(names)
511df47bcadc some support for theory files within Isabelle/Scala session;
wenzelm
parents:
diff changeset
    33
511df47bcadc some support for theory files within Isabelle/Scala session;
wenzelm
parents:
diff changeset
    34
  private def required_by(s: String, initiators: List[String]): String =
511df47bcadc some support for theory files within Isabelle/Scala session;
wenzelm
parents:
diff changeset
    35
    if (initiators.isEmpty) ""
511df47bcadc some support for theory files within Isabelle/Scala session;
wenzelm
parents:
diff changeset
    36
    else s + "(required by " + show_path(initiators.reverse) + ")"
511df47bcadc some support for theory files within Isabelle/Scala session;
wenzelm
parents:
diff changeset
    37
511df47bcadc some support for theory files within Isabelle/Scala session;
wenzelm
parents:
diff changeset
    38
511df47bcadc some support for theory files within Isabelle/Scala session;
wenzelm
parents:
diff changeset
    39
  /* dependencies */
511df47bcadc some support for theory files within Isabelle/Scala session;
wenzelm
parents:
diff changeset
    40
511df47bcadc some support for theory files within Isabelle/Scala session;
wenzelm
parents:
diff changeset
    41
  type Deps = Map[String, Exn.Result[(String, Thy_Header.Header)]]  // name -> (text, header)
511df47bcadc some support for theory files within Isabelle/Scala session;
wenzelm
parents:
diff changeset
    42
43673
29eb1cd29961 Thy_Info.dependencies: ignore already loaded theories, according to initial prover session status;
wenzelm
parents: 43652
diff changeset
    43
  private def require_thys(ignored: String => Boolean,
43651
511df47bcadc some support for theory files within Isabelle/Scala session;
wenzelm
parents:
diff changeset
    44
      initiators: List[String], dir: Path, deps: Deps, strs: List[String]): Deps =
43673
29eb1cd29961 Thy_Info.dependencies: ignore already loaded theories, according to initial prover session status;
wenzelm
parents: 43652
diff changeset
    45
    (deps /: strs)(require_thy(ignored, initiators, dir, _, _))
43651
511df47bcadc some support for theory files within Isabelle/Scala session;
wenzelm
parents:
diff changeset
    46
43673
29eb1cd29961 Thy_Info.dependencies: ignore already loaded theories, according to initial prover session status;
wenzelm
parents: 43652
diff changeset
    47
  private def require_thy(ignored: String => Boolean,
29eb1cd29961 Thy_Info.dependencies: ignore already loaded theories, according to initial prover session status;
wenzelm
parents: 43652
diff changeset
    48
      initiators: List[String], dir: Path, deps: Deps, str: String): Deps =
43651
511df47bcadc some support for theory files within Isabelle/Scala session;
wenzelm
parents:
diff changeset
    49
  {
511df47bcadc some support for theory files within Isabelle/Scala session;
wenzelm
parents:
diff changeset
    50
    val path = Path.explode(str)
511df47bcadc some support for theory files within Isabelle/Scala session;
wenzelm
parents:
diff changeset
    51
    val name = path.base.implode
511df47bcadc some support for theory files within Isabelle/Scala session;
wenzelm
parents:
diff changeset
    52
43673
29eb1cd29961 Thy_Info.dependencies: ignore already loaded theories, according to initial prover session status;
wenzelm
parents: 43652
diff changeset
    53
    if (deps.isDefinedAt(name) || ignored(name)) deps
43651
511df47bcadc some support for theory files within Isabelle/Scala session;
wenzelm
parents:
diff changeset
    54
    else {
511df47bcadc some support for theory files within Isabelle/Scala session;
wenzelm
parents:
diff changeset
    55
      val dir1 = dir + path.dir
511df47bcadc some support for theory files within Isabelle/Scala session;
wenzelm
parents:
diff changeset
    56
      try {
511df47bcadc some support for theory files within Isabelle/Scala session;
wenzelm
parents:
diff changeset
    57
        if (initiators.contains(name)) error(cycle_msg(initiators))
511df47bcadc some support for theory files within Isabelle/Scala session;
wenzelm
parents:
diff changeset
    58
        val (text, header) =
511df47bcadc some support for theory files within Isabelle/Scala session;
wenzelm
parents:
diff changeset
    59
          try { thy_load.check_thy(dir1, name) }
511df47bcadc some support for theory files within Isabelle/Scala session;
wenzelm
parents:
diff changeset
    60
          catch {
511df47bcadc some support for theory files within Isabelle/Scala session;
wenzelm
parents:
diff changeset
    61
            case ERROR(msg) =>
511df47bcadc some support for theory files within Isabelle/Scala session;
wenzelm
parents:
diff changeset
    62
              cat_error(msg, "The error(s) above occurred while examining theory " +
43652
dcd0b667f73d pervasive Basic_Library in Scala;
wenzelm
parents: 43651
diff changeset
    63
                quote(name) + required_by("\n", initiators))
43651
511df47bcadc some support for theory files within Isabelle/Scala session;
wenzelm
parents:
diff changeset
    64
          }
43673
29eb1cd29961 Thy_Info.dependencies: ignore already loaded theories, according to initial prover session status;
wenzelm
parents: 43652
diff changeset
    65
        require_thys(ignored, name :: initiators, dir1,
43651
511df47bcadc some support for theory files within Isabelle/Scala session;
wenzelm
parents:
diff changeset
    66
          deps + (name -> Exn.Res(text, header)), header.imports)
511df47bcadc some support for theory files within Isabelle/Scala session;
wenzelm
parents:
diff changeset
    67
      }
511df47bcadc some support for theory files within Isabelle/Scala session;
wenzelm
parents:
diff changeset
    68
      catch { case e: Throwable => deps + (name -> Exn.Exn(e)) }
511df47bcadc some support for theory files within Isabelle/Scala session;
wenzelm
parents:
diff changeset
    69
    }
511df47bcadc some support for theory files within Isabelle/Scala session;
wenzelm
parents:
diff changeset
    70
  }
511df47bcadc some support for theory files within Isabelle/Scala session;
wenzelm
parents:
diff changeset
    71
511df47bcadc some support for theory files within Isabelle/Scala session;
wenzelm
parents:
diff changeset
    72
  def dependencies(dir: Path, str: String): Deps =
43673
29eb1cd29961 Thy_Info.dependencies: ignore already loaded theories, according to initial prover session status;
wenzelm
parents: 43652
diff changeset
    73
    require_thy(thy_load.is_loaded, Nil, dir, Map.empty, str)  // FIXME capture errors in str (!??)
43651
511df47bcadc some support for theory files within Isabelle/Scala session;
wenzelm
parents:
diff changeset
    74
}