equal
deleted
inserted
replaced
69 let |
69 let |
70 val ok = |
70 val ok = |
71 Synchronized.change_result tracing_messages (fn tab => |
71 Synchronized.change_result tracing_messages (fn tab => |
72 let |
72 let |
73 val n = the_default 0 (Inttab.lookup tab exec_id) + 1; |
73 val n = the_default 0 (Inttab.lookup tab exec_id) + 1; |
74 val ok = n <= Options.default_int "editor_tracing_messages"; |
74 val limit = Options.default_int "editor_tracing_messages"; |
|
75 val ok = limit <= 0 orelse n <= limit; |
75 in (ok, Inttab.update (exec_id, n) tab) end); |
76 in (ok, Inttab.update (exec_id, n) tab) end); |
76 in |
77 in |
77 if ok then () |
78 if ok then () |
78 else |
79 else |
79 let |
80 let |