tuned signature, clarified modules;
authorwenzelm
Wed Apr 15 15:27:45 2015 +0200 (2015-04-15)
changeset 6007755cb9462e602
parent 60076 e24f59cba23c
child 60078 019347f8dc88
tuned signature, clarified modules;
src/Pure/Thy/present.scala
src/Pure/Thy/thy_info.scala
src/Pure/Tools/build.scala
     1.1 --- a/src/Pure/Thy/present.scala	Wed Apr 15 14:54:25 2015 +0200
     1.2 +++ b/src/Pure/Thy/present.scala	Wed Apr 15 15:27:45 2015 +0200
     1.3 @@ -12,6 +12,32 @@
     1.4  
     1.5  object Present
     1.6  {
     1.7 +  /* session graph */
     1.8 +
     1.9 +  def session_graph(
    1.10 +    parent_session: String,
    1.11 +    parent_loaded: String => Boolean,
    1.12 +    deps: List[Thy_Info.Dep]): Graph_Display.Graph =
    1.13 +  {
    1.14 +    val parent_session_node =
    1.15 +      Graph_Display.Node("[" + parent_session + "]", "session." + parent_session)
    1.16 +
    1.17 +    def node(name: Document.Node.Name): Graph_Display.Node =
    1.18 +      if (parent_loaded(name.theory)) parent_session_node
    1.19 +      else Graph_Display.Node(name.theory, "theory." + name.theory)
    1.20 +
    1.21 +    (Graph_Display.empty_graph /: deps) {
    1.22 +      case (g, dep) =>
    1.23 +        if (parent_loaded(dep.name.theory)) g
    1.24 +        else {
    1.25 +          val a = node(dep.name)
    1.26 +          val bs = dep.header.imports.map({ case (name, _) => node(name) })
    1.27 +          ((g /: (a :: bs))(_.default_node(_, Nil)) /: bs)(_.add_edge(_, a))
    1.28 +        }
    1.29 +    }
    1.30 +  }
    1.31 +
    1.32 +
    1.33    /* maintain chapter index -- NOT thread-safe */
    1.34  
    1.35    private val index_path = Path.basic("index.html")
    1.36 @@ -48,4 +74,3 @@
    1.37      File.write(dir + index_path, HTML.chapter_index(chapter, sessions))
    1.38    }
    1.39  }
    1.40 -
     2.1 --- a/src/Pure/Thy/thy_info.scala	Wed Apr 15 14:54:25 2015 +0200
     2.2 +++ b/src/Pure/Thy/thy_info.scala	Wed Apr 15 15:27:45 2015 +0200
     2.3 @@ -7,6 +7,15 @@
     2.4  package isabelle
     2.5  
     2.6  
     2.7 +object Thy_Info
     2.8 +{
     2.9 +  /* dependencies */
    2.10 +
    2.11 +  sealed case class Dep(
    2.12 +    name: Document.Node.Name,
    2.13 +    header: Document.Node.Header)
    2.14 +}
    2.15 +
    2.16  class Thy_Info(resources: Resources)
    2.17  {
    2.18    /* messages */
    2.19 @@ -24,29 +33,18 @@
    2.20  
    2.21    /* dependencies */
    2.22  
    2.23 -  sealed case class Dep(
    2.24 -    name: Document.Node.Name,
    2.25 -    header: Document.Node.Header)
    2.26 -  {
    2.27 -    def loaded_files(syntax: Prover.Syntax): List[String] =
    2.28 -    {
    2.29 -      val string = resources.with_thy_reader(name, reader => Symbol.decode(reader.source.toString))
    2.30 -      resources.loaded_files(syntax, string)
    2.31 -    }
    2.32 -  }
    2.33 -
    2.34    object Dependencies
    2.35    {
    2.36      val empty = new Dependencies(Nil, Nil, Multi_Map.empty, Multi_Map.empty)
    2.37    }
    2.38  
    2.39    final class Dependencies private(
    2.40 -    rev_deps: List[Dep],
    2.41 +    rev_deps: List[Thy_Info.Dep],
    2.42      val keywords: Thy_Header.Keywords,
    2.43      val seen_names: Multi_Map[String, Document.Node.Name],
    2.44      val seen_positions: Multi_Map[String, Position.T])
    2.45    {
    2.46 -    def :: (dep: Dep): Dependencies =
    2.47 +    def :: (dep: Thy_Info.Dep): Dependencies =
    2.48        new Dependencies(dep :: rev_deps, dep.header.keywords ::: keywords,
    2.49          seen_names, seen_positions)
    2.50  
    2.51 @@ -58,7 +56,7 @@
    2.52          seen_positions + (name.theory -> pos))
    2.53      }
    2.54  
    2.55 -    def deps: List[Dep] = rev_deps.reverse
    2.56 +    def deps: List[Thy_Info.Dep] = rev_deps.reverse
    2.57  
    2.58      def errors: List[String] =
    2.59      {
    2.60 @@ -84,33 +82,16 @@
    2.61  
    2.62      def loaded_files: List[Path] =
    2.63      {
    2.64 -      val dep_files =
    2.65 -        Par_List.map(
    2.66 -          (dep: Dep) =>
    2.67 -            dep.loaded_files(syntax).map(a => Path.explode(dep.name.master_dir) + Path.explode(a)),
    2.68 -          rev_deps)
    2.69 +      def loaded(dep: Thy_Info.Dep): List[Path] =
    2.70 +      {
    2.71 +        val string = resources.with_thy_reader(dep.name,
    2.72 +          reader => Symbol.decode(reader.source.toString))
    2.73 +        resources.loaded_files(syntax, string).
    2.74 +          map(a => Path.explode(dep.name.master_dir) + Path.explode(a))
    2.75 +      }
    2.76 +      val dep_files = Par_List.map(loaded _, rev_deps)
    2.77        ((Nil: List[Path]) /: dep_files) { case (acc_files, files) => files ::: acc_files }
    2.78      }
    2.79 -
    2.80 -    def deps_graph(parent_session: String, parent_loaded: String => Boolean): Graph_Display.Graph =
    2.81 -    {
    2.82 -      val parent_session_node =
    2.83 -        Graph_Display.Node("[" + parent_session + "]", "session." + parent_session)
    2.84 -
    2.85 -      def node(name: Document.Node.Name): Graph_Display.Node =
    2.86 -        if (parent_loaded(name.theory)) parent_session_node
    2.87 -        else Graph_Display.Node(name.theory, "theory." + name.theory)
    2.88 -
    2.89 -      (Graph_Display.empty_graph /: rev_deps) {
    2.90 -        case (g, dep) =>
    2.91 -          if (parent_loaded(dep.name.theory)) g
    2.92 -          else {
    2.93 -            val a = node(dep.name)
    2.94 -            val bs = dep.header.imports.map({ case (name, _) => node(name) })
    2.95 -            ((g /: (a :: bs))(_.default_node(_, Nil)) /: bs)(_.add_edge(_, a))
    2.96 -          }
    2.97 -      }
    2.98 -    }
    2.99    }
   2.100  
   2.101    private def require_thys(session: String, initiators: List[Document.Node.Name],
   2.102 @@ -136,11 +117,12 @@
   2.103          val header =
   2.104            try { resources.check_thy(session, name, Token.Pos.file(name.node)).cat_errors(message) }
   2.105            catch { case ERROR(msg) => cat_error(msg, message) }
   2.106 -        Dep(name, header) :: require_thys(session, name :: initiators, required1, header.imports)
   2.107 +        Thy_Info.Dep(name, header) ::
   2.108 +          require_thys(session, name :: initiators, required1, header.imports)
   2.109        }
   2.110        catch {
   2.111          case e: Throwable =>
   2.112 -          Dep(name, Document.Node.bad_header(Exn.message(e))) :: required1
   2.113 +          Thy_Info.Dep(name, Document.Node.bad_header(Exn.message(e))) :: required1
   2.114        }
   2.115      }
   2.116    }
     3.1 --- a/src/Pure/Tools/build.scala	Wed Apr 15 14:54:25 2015 +0200
     3.2 +++ b/src/Pure/Tools/build.scala	Wed Apr 15 15:27:45 2015 +0200
     3.3 @@ -512,7 +512,8 @@
     3.4  
     3.5              val sources = all_files.map(p => (p, SHA1.digest(p.file)))
     3.6  
     3.7 -            val session_graph = thy_deps.deps_graph(info.parent getOrElse "", loaded_theories0)
     3.8 +            val session_graph =
     3.9 +              Present.session_graph(info.parent getOrElse "", loaded_theories0, thy_deps.deps)
    3.10  
    3.11              val content =
    3.12                Session_Content(loaded_theories, known_theories, keywords, syntax,