46 { |
46 { |
47 db.transaction { |
47 db.transaction { |
48 for (theory <- Export.read_theory_names(db, session)) |
48 for (theory <- Export.read_theory_names(db, session)) |
49 yield { |
49 yield { |
50 progress.echo("Reading theory " + theory) |
50 progress.echo("Reading theory " + theory) |
51 if (theory == Thy_Header.PURE) read_pure_theory(store, cache = Some(cache)) |
51 read_theory(Export.Provider.database(db, session, theory), |
52 else { |
52 session, theory, types = types, consts = consts, |
53 read_theory(Export.Provider.database(db, session, theory), |
53 axioms = axioms, thms = thms, classes = classes, locales = locales, |
54 session, theory, types = types, consts = consts, |
54 locale_dependencies = locale_dependencies, classrel = classrel, arities = arities, |
55 axioms = axioms, thms = thms, classes = classes, locales = locales, |
55 typedefs = typedefs, cache = Some(cache)) |
56 locale_dependencies = locale_dependencies, classrel = classrel, arities = arities, |
|
57 typedefs = typedefs, cache = Some(cache)) |
|
58 } |
|
59 } |
56 } |
60 } |
57 } |
61 })) |
58 })) |
62 |
59 |
63 val graph0 = |
60 val graph0 = |
128 arities: Boolean = true, |
125 arities: Boolean = true, |
129 typedefs: Boolean = true, |
126 typedefs: Boolean = true, |
130 cache: Option[Term.Cache] = None): Theory = |
127 cache: Option[Term.Cache] = None): Theory = |
131 { |
128 { |
132 val parents = |
129 val parents = |
133 provider(export_prefix + "parents") match { |
130 if (theory_name == Thy_Header.PURE) Nil |
134 case Some(entry) => split_lines(entry.uncompressed().text) |
131 else { |
135 case None => |
132 provider(export_prefix + "parents") match { |
136 error("Missing theory export in session " + quote(session_name) + ": " + |
133 case Some(entry) => split_lines(entry.uncompressed().text) |
137 quote(theory_name)) |
134 case None => |
|
135 error("Missing theory export in session " + quote(session_name) + ": " + |
|
136 quote(theory_name)) |
|
137 } |
138 } |
138 } |
139 val theory = |
139 val theory = |
140 Theory(theory_name, parents, |
140 Theory(theory_name, parents, |
141 if (types) read_types(provider) else Nil, |
141 if (types) read_types(provider) else Nil, |
142 if (consts) read_consts(provider) else Nil, |
142 if (consts) read_consts(provider) else Nil, |