equal
deleted
inserted
replaced
414 Reference Toplevel.debug (default false) controls detailed printing |
414 Reference Toplevel.debug (default false) controls detailed printing |
415 and tracing of low-level exceptions; Toplevel.profiling (default 0) |
415 and tracing of low-level exceptions; Toplevel.profiling (default 0) |
416 controls execution profiling -- set to 1 for time and 2 for space |
416 controls execution profiling -- set to 1 for time and 2 for space |
417 (both increase the runtime). |
417 (both increase the runtime). |
418 |
418 |
|
419 * Isar session: The initial use of ROOT.ML is now always timed, |
|
420 i.e. the log will show the actual process times, in contrast to the |
|
421 elapsed wall-clock time that the outer shell wrapper produces. |
|
422 |
419 * Pure: structure OrdList (cf. Pure/General/ord_list.ML) provides a |
423 * Pure: structure OrdList (cf. Pure/General/ord_list.ML) provides a |
420 reasonably efficient light-weight implementation of sets as lists. |
424 reasonably efficient light-weight implementation of sets as lists. |
421 |
425 |
422 * Pure: more efficient orders for basic syntactic entities: added |
426 * Pure: more efficient orders for basic syntactic entities: added |
423 fast_string_ord, fast_indexname_ord, fast_term_ord; changed sort_ord |
427 fast_string_ord, fast_indexname_ord, fast_term_ord; changed sort_ord |