+ let changed_lexicon = ref false in
+ let wrap f x = changed_lexicon := true; f x in
+ let grafite_status =
+ match grafite_status.GrafiteTypes.ng_status with
+ | GrafiteTypes.CommandMode _ ->
+ { grafite_status with GrafiteTypes.ng_status =
+ GrafiteTypes.CommandMode lexicon_status }
+ | GrafiteTypes.ProofMode s ->
+ { grafite_status with GrafiteTypes.ng_status =
+ GrafiteTypes.ProofMode
+ { s with NTacStatus.istatus = { s.NTacStatus.istatus with NTacStatus.lstatus = lexicon_status }}}
+ in