equal
deleted
inserted
replaced
102 -- "ML exception trace for toplevel command execution" |
102 -- "ML exception trace for toplevel command execution" |
103 |
103 |
104 public option ML_debugger : bool = false |
104 public option ML_debugger : bool = false |
105 -- "ML debugger instrumentation for newly compiled code" |
105 -- "ML debugger instrumentation for newly compiled code" |
106 |
106 |
107 public option ML_debugger_active : bool = true |
|
108 -- "ML debugger active at run-time, for code compiled with debugger instrumentation" |
|
109 |
|
110 public option ML_statistics : bool = true |
107 public option ML_statistics : bool = true |
111 -- "ML run-time system statistics" |
108 -- "ML run-time system statistics" |
112 |
109 |
113 |
110 |
114 section "Editor Reactivity" |
111 section "Editor Reactivity" |