1 (* Copyright (C) 2004, HELM Team.
3 * This file is part of HELM, an Hypertextual, Electronic
4 * Library of Mathematics, developed at the Computer Science
5 * Department, University of Bologna, Italy.
7 * HELM is free software; you can redistribute it and/or
8 * modify it under the terms of the GNU General Public License
9 * as published by the Free Software Foundation; either version 2
10 * of the License, or (at your option) any later version.
12 * HELM is distributed in the hope that it will be useful,
13 * but WITHOUT ANY WARRANTY; without even the implied warranty of
14 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
15 * GNU General Public License for more details.
17 * You should have received a copy of the GNU General Public License
18 * along with HELM; if not, write to the Free Software
19 * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
22 * For details, see the HELM World-Wide-Web page,
23 * http://helm.cs.unibo.it/
26 (** Stateful handling of proof status *)
28 exception No_goal_left
29 exception Uri_redefinition
31 (** can't undo/redo one or more actions *)
32 exception History_failure
34 type event = [ `Proof_changed | `Proof_completed ]
36 (** Proof observer. First callback argument is Some extended_status
37 * when a 'real 'change of the proof happened and None when Proof_changed event
38 * was triggered by a time travel by the means of undo/redo actions. Embedded
39 * status is the status _before_ the current change. Second status is the
40 * status reached _after_ the current change. *)
42 (ProofEngineTypes.status * 'a) option -> (ProofEngineTypes.status * 'a) ->
45 (** needed to detach previously attached observers *)
48 (** tactic application failed. @see apply_tactic *)
49 exception Tactic_failure of exn
51 (** one or more observers failed. @see apply_tactic *)
52 exception Observer_failures of (observer_id * exn) list
54 (** failure while updating internal data (: 'a). @see apply_tactic *)
55 exception Data_failure of exn
57 (** {2 OO interface} *)
60 ?uri:UriManager.uri ->
61 typ:Cic.term -> ?body:Cic.term -> ?metasenv:Cic.metasenv ->
62 (ProofEngineTypes.proof * ProofEngineTypes.goal option -> 'a) ->
63 (ProofEngineTypes.status * 'a -> ProofEngineTypes.status -> 'a) ->
67 method proof: ProofEngineTypes.proof
68 method metasenv: Cic.metasenv
72 (** goal -> conjecture
73 * @raise CicUtil.Meta_not_found *)
74 method conjecture: int -> Cic.conjecture
76 method proof_completed: bool
77 method goal: int (** @raise No_goal_left *)
78 method set_goal: int -> unit (** @raise No_goal_left *)
80 method uri: UriManager.uri option
81 method set_uri: UriManager.uri -> unit (** @raise Uri_redefinition *)
83 (** @raise Tactic_failure
84 * @raise Observer_failures
87 * In case of tactic failure, internal status is left unchanged.
88 * In case of observer failures internal status will be changed and is
89 * granted that all observer will be invoked collecting their failures.
90 * In case of data failure, internal status is left unchanged (rolling back
91 * last tactic application if needed)
93 method apply_tactic: ProofEngineTypes.tactic -> unit
95 method undo: ?steps:int -> unit -> unit
96 method redo: ?steps:int -> unit -> unit
98 method attach_observer:
99 ?interested_in:(event list) -> 'a observer -> observer_id
101 method detach_observer: observer_id -> unit
106 ?uri:UriManager.uri ->
107 typ:Cic.term -> ?body:Cic.term -> ?metasenv:Cic.metasenv ->