equal
deleted
inserted
replaced
398 (Simplifier.set_trace_ops |
398 (Simplifier.set_trace_ops |
399 {trace_invoke = fn {depth, term} => recurse "Simplifier invoked" depth term, |
399 {trace_invoke = fn {depth, term} => recurse "Simplifier invoked" depth term, |
400 trace_apply = simp_apply}) |
400 trace_apply = simp_apply}) |
401 |
401 |
402 val _ = |
402 val _ = |
403 Isabelle_Process.protocol_command "Simplifier_Trace.reply" |
403 Protocol_Command.define "Simplifier_Trace.reply" |
404 (fn [serial_string, reply] => |
404 (fn [serial_string, reply] => |
405 let |
405 let |
406 val serial = Value.parse_int serial_string |
406 val serial = Value.parse_int serial_string |
407 val result = |
407 val result = |
408 Synchronized.change_result futures |
408 Synchronized.change_result futures |