equal
deleted
inserted
replaced
30 { |
30 { |
31 val thys = |
31 val thys = |
32 using(store.open_database(session_name))(db => |
32 using(store.open_database(session_name))(db => |
33 { |
33 { |
34 db.transaction { |
34 db.transaction { |
35 Export.read_theory_names(db, session_name).iterator.map(_._1).toSet.iterator. |
35 Export.read_theory_names(db, session_name).map((theory_name: String) => |
36 map((theory_name: String) => |
36 read_theory(db, session_name, theory_name, types = types, consts = consts)) |
37 read_theory(db, session_name, theory_name, types = types, consts = consts)).toList |
|
38 } |
37 } |
39 }) |
38 }) |
40 |
39 |
41 val graph0 = |
40 val graph0 = |
42 (Graph.string[Theory] /: thys) { case (g, thy) => g.new_node(thy.name, thy) } |
41 (Graph.string[Theory] /: thys) { case (g, thy) => g.new_node(thy.name, thy) } |