tuned signature;
authorwenzelm
Tue Aug 21 13:29:34 2012 +0200 (2012-08-21)
changeset 48871c82720f054c3
parent 48870 4accee106f0f
child 48872 6124e0d1120a
tuned signature;
src/Pure/Thy/thy_info.scala
     1.1 --- a/src/Pure/Thy/thy_info.scala	Tue Aug 21 12:15:25 2012 +0200
     1.2 +++ b/src/Pure/Thy/thy_info.scala	Tue Aug 21 13:29:34 2012 +0200
     1.3 @@ -25,7 +25,13 @@
     1.4    /* dependencies */
     1.5  
     1.6    type Dep = (Document.Node.Name, Document.Node.Header)
     1.7 -  private type Required = (List[Dep], Set[Document.Node.Name])
     1.8 +  private sealed case class Required(
     1.9 +    deps: List[Dep] = Nil,
    1.10 +    seen: Set[Document.Node.Name] = Set.empty)
    1.11 +  {
    1.12 +    def :: (dep: Dep): Required = copy(deps = dep :: deps)
    1.13 +    def + (name: Document.Node.Name): Required = copy(seen = seen + name)
    1.14 +  }
    1.15  
    1.16    private def require_thys(initiators: List[Document.Node.Name],
    1.17        required: Required, names: List[Document.Node.Name]): Required =
    1.18 @@ -34,9 +40,8 @@
    1.19    private def require_thy(initiators: List[Document.Node.Name],
    1.20        required: Required, name: Document.Node.Name): Required =
    1.21    {
    1.22 -    val (deps, seen) = required
    1.23 -    if (seen(name)) required
    1.24 -    else if (thy_load.loaded_theories(name.theory)) (deps, seen + name)
    1.25 +    if (required.seen(name)) required
    1.26 +    else if (thy_load.loaded_theories(name.theory)) required + name
    1.27      else {
    1.28        try {
    1.29          if (initiators.contains(name)) error(cycle_msg(initiators))
    1.30 @@ -47,17 +52,15 @@
    1.31                cat_error(msg, "The error(s) above occurred while examining theory " +
    1.32                  quote(name.theory) + required_by(initiators))
    1.33            }
    1.34 -        val (deps1, seen1) =
    1.35 -          require_thys(name :: initiators, (deps, seen + name), header.imports)
    1.36 -        ((name, header) :: deps1, seen1)
    1.37 +        (name, header) :: require_thys(name :: initiators, required + name, header.imports)
    1.38        }
    1.39        catch {
    1.40          case e: Throwable =>
    1.41 -          ((name, Document.Node.bad_header(Exn.message(e))) :: deps, seen + name)
    1.42 +          (name, Document.Node.bad_header(Exn.message(e))) :: (required + name)
    1.43        }
    1.44      }
    1.45    }
    1.46  
    1.47    def dependencies(names: List[Document.Node.Name]): List[Dep] =
    1.48 -    require_thys(Nil, (Nil, Set.empty), names)._1.reverse
    1.49 +    require_thys(Nil, Required(), names).deps.reverse
    1.50  }