* http://helm.cs.unibo.it/
*)
+ (** multi selection gtkMathView which handle mactions and hyperlinks. Mactions
+ * are handled internally. Hyperlinks are handled by calling an user provided
+ * callback *)
+class type clickable_math_view =
+ object
+ inherit GMathViewAux.multi_selection_math_view
+
+ (** set hyperlink callback. None disable hyperlink handling *)
+ method set_href_callback: (UriManager.uri -> unit) option -> unit
+ end
+
class type proof_viewer =
object
- inherit GMathViewAux.single_selection_math_view
+ inherit clickable_math_view
method load_proof: StatefulProofEngine.proof_status -> unit
end
class type sequent_viewer =
object
- inherit GMathViewAux.multi_selection_math_view
+ inherit clickable_math_view
(** @return the list of selected terms. Selections which are not terms are
* ignored *)
method goto_sequent: int -> unit (* to be called _after_ load_sequents *)
end
+class type cicBrowser =
+ object
+ method load_uri: UriManager.uri -> unit
+ end
+
+(** {2 Constructors} *)
+
val proof_viewer:
?hadjustment:GData.adjustment ->
?vadjustment:GData.adjustment ->
unit ->
proof_viewer
- (** singleton proof_viewer instance.
- * Uses singleton GUI instance *)
-val proof_viewer_instance: unit -> proof_viewer
-
val sequent_viewer:
?hadjustment:GData.adjustment ->
?vadjustment:GData.adjustment ->
unit ->
sequents_viewer
+val cicBrowser: unit -> cicBrowser
+
val mathViewer: unit -> MatitaTypes.mathViewer
+(** {2 Singletons} *)
+
+ (** singleton proof_viewer instance.
+ * Uses singleton GUI instance *)
+val proof_viewer_instance: unit -> proof_viewer
+