equal
deleted
inserted
replaced
73 fun update_tracing () = |
73 fun update_tracing () = |
74 (case Position.parse_id (Position.thread_data ()) of |
74 (case Position.parse_id (Position.thread_data ()) of |
75 NONE => () |
75 NONE => () |
76 | SOME id => |
76 | SOME id => |
77 let |
77 let |
78 val (n, ok) = |
78 val ok = |
79 Synchronized.change_result tracing_messages (fn tab => |
79 Synchronized.change_result tracing_messages (fn tab => |
80 let |
80 let |
81 val n = the_default 0 (Inttab.lookup tab id) + 1; |
81 val n = the_default 0 (Inttab.lookup tab id) + 1; |
82 val ok = n <= Options.default_int "editor_tracing_messages"; |
82 val ok = n <= Options.default_int "editor_tracing_messages"; |
83 in ((n, ok), Inttab.update (id, n) tab) end); |
83 in (ok, Inttab.update (id, n) tab) end); |
84 in |
84 in |
85 if ok then () |
85 if ok then () |
86 else |
86 else |
87 let |
87 let |
88 val (text, promise) = Active.dialog_text (); |
88 val (text, promise) = Active.dialog_text (); |