operations for graph display;
authorwenzelm
Mon Oct 09 21:43:27 2017 +0200 (19 months ago)
changeset 66823f529719cc47d
parent 66822 4642cf4a7ebb
child 66824 49a3a0a6ffaf
operations for graph display;
src/Pure/Admin/afp.scala
src/Pure/General/graph_display.scala
src/Pure/Thy/sessions.scala
     1.1 --- a/src/Pure/Admin/afp.scala	Mon Oct 09 21:12:22 2017 +0200
     1.2 +++ b/src/Pure/Admin/afp.scala	Mon Oct 09 21:43:27 2017 +0200
     1.3 @@ -70,6 +70,9 @@
     1.4      val afp_sessions: Sessions.T,
     1.5      val entries_graph: Graph[String, Unit])
     1.6    {
     1.7 +    def entries_graph_display: Graph_Display.Graph =
     1.8 +      Graph_Display.make_graph(entries_graph)
     1.9 +
    1.10      def entries_json_text: String =
    1.11        (for (entry <- entries)
    1.12        yield {
     2.1 --- a/src/Pure/General/graph_display.scala	Mon Oct 09 21:12:22 2017 +0200
     2.2 +++ b/src/Pure/General/graph_display.scala	Mon Oct 09 21:43:27 2017 +0200
     2.3 @@ -60,5 +60,13 @@
     2.4          import XML.Decode._
     2.5          list(pair(pair(string, pair(string, x => x)), list(string)))(body)
     2.6        })
     2.7 +
     2.8 +  def make_graph[A](
     2.9 +    graph: isabelle.Graph[String, A],
    2.10 +    name: (String, A) => String = (x: String, a: A) => x): Graph =
    2.11 +  {
    2.12 +    val entries =
    2.13 +      (for ((x, (a, (ps, _))) <- graph.iterator) yield ((x, (name(x, a), Nil)), ps.toList)).toList
    2.14 +    build_graph(entries)
    2.15 +  }
    2.16  }
    2.17 -
     3.1 --- a/src/Pure/Thy/sessions.scala	Mon Oct 09 21:12:22 2017 +0200
     3.2 +++ b/src/Pure/Thy/sessions.scala	Mon Oct 09 21:43:27 2017 +0200
     3.3 @@ -479,6 +479,9 @@
     3.4        val build_graph: Graph[String, Info],
     3.5        val imports_graph: Graph[String, Info])
     3.6    {
     3.7 +    def build_graph_display: Graph_Display.Graph = Graph_Display.make_graph(build_graph)
     3.8 +    def imports_graph_display: Graph_Display.Graph = Graph_Display.make_graph(imports_graph)
     3.9 +
    3.10      def apply(name: String): Info = imports_graph.get_node(name)
    3.11      def get(name: String): Option[Info] =
    3.12        if (imports_graph.defined(name)) Some(imports_graph.get_node(name)) else None