exception No_goal_left
exception Uri_redefinition
- (** can't undo/redo one or more actions *)
-exception History_failure
-
type event = [ `Proof_changed | `Proof_completed ]
+val all_events: event list
+
+ (** from our point of view a status is the status of an incomplete proof, thus
+ * we have an optional goal which is None if the proof is not yet completed
+ * (i.e. some goal is still open) *)
+type proof_status = ProofEngineTypes.proof * ProofEngineTypes.goal option
+
(** Proof observer. First callback argument is Some extended_status
* when a 'real 'change of the proof happened and None when Proof_changed event
- * was triggered by a time travel by the means of undo/redo actions. Embedded
- * status is the status _before_ the current change. Second status is the
- * status reached _after_ the current change. *)
-type 'a observer =
- (ProofEngineTypes.status * 'a) option -> (ProofEngineTypes.status * 'a) ->
- unit
+ * was triggered by a time travel by the means of undo/redo actions or by an
+ * external "#notify" invocation. Embedded status is the status _before_ the
+ * current change. Second status is the status reached _after_ the current
+ * change. *)
+type 'a observer = (proof_status * 'a) option -> (proof_status * 'a) -> unit
(** needed to detach previously attached observers *)
type observer_id
(** {2 OO interface} *)
class ['a] status:
+ ?history_size:int -> (** default 20 *)
?uri:UriManager.uri ->
- typ:Cic.term -> ?body:Cic.term -> ?metasenv:Cic.metasenv ->
- (ProofEngineTypes.proof * ProofEngineTypes.goal option -> 'a) ->
- (ProofEngineTypes.status * 'a -> ProofEngineTypes.status -> 'a) ->
+ typ:Cic.term -> body:Cic.term -> metasenv:Cic.metasenv ->
+ (proof_status -> 'a) -> (* init data *)
+ (proof_status * 'a -> proof_status -> 'a) -> (* update data *)
unit ->
object
method body: Cic.term
method typ: Cic.term
+ (** change metasenv _without_ triggering any notification *)
+ method set_metasenv: Cic.metasenv -> unit
+
(** goal -> conjecture
* @raise CicUtil.Meta_not_found *)
method conjecture: int -> Cic.conjecture
method proof_completed: bool
method goal: int (** @raise No_goal_left *)
- method set_goal: int -> unit (** @raise No_goal_left *)
+ method set_goal: int -> unit (** @raise Data_failure *)
method uri: UriManager.uri option
method set_uri: UriManager.uri -> unit (** @raise Uri_redefinition *)
method detach_observer: observer_id -> unit
+ (** force a notification to all observer, old status is passed as None *)
+ method notify: unit
+
end
val trivial_status:
?uri:UriManager.uri ->
- typ:Cic.term -> ?body:Cic.term -> ?metasenv:Cic.metasenv ->
+ typ:Cic.term -> body:Cic.term -> metasenv:Cic.metasenv ->
unit ->
unit status