equal
deleted
inserted
replaced
61 list(pair(pair(string, pair(string, x => x)), list(string)))(body) |
61 list(pair(pair(string, pair(string, x => x)), list(string)))(body) |
62 }) |
62 }) |
63 |
63 |
64 def make_graph[A]( |
64 def make_graph[A]( |
65 graph: isabelle.Graph[String, A], |
65 graph: isabelle.Graph[String, A], |
|
66 isolated: Boolean = false, |
66 name: (String, A) => String = (x: String, a: A) => x): Graph = |
67 name: (String, A) => String = (x: String, a: A) => x): Graph = |
67 { |
68 { |
68 val entries = |
69 val entries = |
69 (for ((x, (a, (ps, _))) <- graph.iterator) yield ((x, (name(x, a), Nil)), ps.toList)).toList |
70 (for { (x, (a, (ps, _))) <- graph.iterator if isolated || !graph.is_isolated(x) } |
|
71 yield ((x, (name(x, a), Nil)), ps.toList)).toList |
70 build_graph(entries) |
72 build_graph(entries) |
71 } |
73 } |
72 } |
74 } |