let scratch = ref Context.empty