equal
deleted
inserted
replaced
490 val build_options = |
490 val build_options = |
491 options + |
491 options + |
492 "ML_statistics" + |
492 "ML_statistics" + |
493 "completion_limit=0" + |
493 "completion_limit=0" + |
494 "editor_tracing_messages=0" + |
494 "editor_tracing_messages=0" + |
|
495 "pide_exports=false" + |
495 "pide_reports=false" |
496 "pide_reports=false" |
496 |
497 |
497 val store = Sessions.store(build_options) |
498 val store = Sessions.store(build_options) |
498 |
499 |
499 Isabelle_Fonts.init() |
500 Isabelle_Fonts.init() |