type ng_status =
| ProofMode of NTacStatus.tac_status
- | CommandMode of NEstatus.extra_status
+ | CommandMode of NEstatus.status
type status = {
moo_content_rev: GrafiteMarshal.moo;
ng_status: ng_status;
}
-let get_lexicon x =
- match x.ng_status with
- | ProofMode t -> t.NTacStatus.istatus.NTacStatus.estatus.NEstatus.lstatus
- | CommandMode e -> e.NEstatus.lstatus
-;;
-
-let set_lexicon new_lexicon_status new_grafite_status =
- { new_grafite_status with ng_status =
- match new_grafite_status.ng_status with
- | CommandMode estatus ->
- CommandMode
- { estatus with NEstatus.lstatus = new_lexicon_status }
- | ProofMode t ->
- ProofMode
- { t with NTacStatus.istatus =
- { t.NTacStatus.istatus with NTacStatus.estatus =
- { t.NTacStatus.istatus.NTacStatus.estatus with NEstatus.lstatus =
- new_lexicon_status }}}}
-;;
-
let get_estatus x =
match x.ng_status with
| ProofMode t -> t.NTacStatus.istatus.NTacStatus.estatus
| CommandMode _ -> CommandMode e}
;;
-let get_dstatus x = (get_estatus x).NEstatus.rstatus;;
-
-let set_dstatus h x =
- let estatus = get_estatus x in
- set_estatus { estatus with NEstatus.rstatus = h } x
-;;
-
let get_current_proof status =
match status.proof_status with
| Incomplete_proof { proof = p } -> p