equal
deleted
inserted
replaced
114 -- "build process output tail shown to user (in lines, 0 = unlimited)" |
114 -- "build process output tail shown to user (in lines, 0 = unlimited)" |
115 |
115 |
116 option profiling : string = "" |
116 option profiling : string = "" |
117 -- "ML profiling (possible values: time, allocations)" |
117 -- "ML profiling (possible values: time, allocations)" |
118 |
118 |
|
119 option system_heaps : bool = false |
|
120 -- "store session heaps in $ISABELLE_HEAPS_SYSTEM, not $ISABELLE_HEAPS" |
|
121 |
119 |
122 |
120 section "ML System" |
123 section "ML System" |
121 |
124 |
122 option ML_print_depth : int = 20 |
125 option ML_print_depth : int = 20 |
123 -- "ML print depth for toplevel pretty-printing" |
126 -- "ML print depth for toplevel pretty-printing" |