| changeset 72692 | 22aeec526ffd |
| parent 72683 | b5e6f0d137a7 |
| child 72693 | 0201ae367518 |
| 72691:2126cf946086 | 72692:22aeec526ffd |
|---|---|
200 { |
200 { |
201 val build_options = |
201 val build_options = |
202 options + |
202 options + |
203 "completion_limit=0" + |
203 "completion_limit=0" + |
204 "editor_tracing_messages=0" + |
204 "editor_tracing_messages=0" + |
205 "pide_reports=false" |
205 "pide_reports=false" // FIXME |
206 |
206 |
207 val store = Sessions.store(build_options) |
207 val store = Sessions.store(build_options) |
208 |
208 |
209 Isabelle_Fonts.init() |
209 Isabelle_Fonts.init() |
210 |
210 |