91 breakgain: Double = Pretty.default_breakgain, |
91 breakgain: Double = Pretty.default_breakgain, |
92 metric: Pretty.Metric = Symbol.Metric, |
92 metric: Pretty.Metric = Symbol.Metric, |
93 unicode_symbols: Boolean = false): Unit = |
93 unicode_symbols: Boolean = false): Unit = |
94 { |
94 { |
95 val store = Sessions.store(options) |
95 val store = Sessions.store(options) |
96 |
|
97 val resources = Resources.empty |
96 val resources = Resources.empty |
98 val session = new Session(options, resources) |
97 val session = new Session(options, resources) |
99 |
98 |
100 using(store.open_database_context())(db_context => |
99 using(store.open_database_context())(db_context => |
101 { |
100 { |
107 store.read_build(db, session_name).map(info => (theories, errors, info.return_code)) |
106 store.read_build(db, session_name).map(info => (theories, errors, info.return_code)) |
108 }) |
107 }) |
109 result match { |
108 result match { |
110 case None => error("Missing build database for session " + quote(session_name)) |
109 case None => error("Missing build database for session " + quote(session_name)) |
111 case Some((used_theories, errors, rc)) => |
110 case Some((used_theories, errors, rc)) => |
112 val bad_theories = theories.filterNot(used_theories.toSet) |
111 theories.filterNot(used_theories.toSet) match { |
113 if (bad_theories.nonEmpty) error("Unknown theories " + commas_quote(bad_theories)) |
112 case Nil => |
114 |
113 case bad => error("Unknown theories " + commas_quote(bad)) |
|
114 } |
115 val print_theories = |
115 val print_theories = |
116 if (theories.isEmpty) used_theories else used_theories.filter(theories.toSet) |
116 if (theories.isEmpty) used_theories else used_theories.filter(theories.toSet) |
117 for (thy <- print_theories) { |
117 for (thy <- print_theories) { |
118 val thy_heading = "\nTheory " + quote(thy) + ":" |
118 val thy_heading = "\nTheory " + quote(thy) + ":" |
119 read_theory(db_context, resources, session_name, thy, unicode_symbols = unicode_symbols) |
119 read_theory(db_context, resources, session_name, thy, unicode_symbols = unicode_symbols) |