equal
deleted
inserted
replaced
89 else |
89 else |
90 let |
90 let |
91 val (text, promise) = Active.dialog_text (); |
91 val (text, promise) = Active.dialog_text (); |
92 val _ = |
92 val _ = |
93 writeln ("Tracing paused. " ^ text "Stop" ^ ", or continue with next " ^ |
93 writeln ("Tracing paused. " ^ text "Stop" ^ ", or continue with next " ^ |
94 text "10" ^ ", " ^ text "100" ^ ", " ^ text "1000" ^ " messages?") |
94 text "100" ^ ", " ^ text "1000" ^ ", " ^ text "10000" ^ " messages?") |
95 val m = Markup.parse_int (Future.join promise) |
95 val m = Markup.parse_int (Future.join promise) |
96 handle Fail _ => error "Stopped"; |
96 handle Fail _ => error "Stopped"; |
97 in |
97 in |
98 Synchronized.change command_tracing_messages |
98 Synchronized.change command_tracing_messages |
99 (Inttab.map_default (id, 0) (fn k => k - m)) |
99 (Inttab.map_default (id, 0) (fn k => k - m)) |