method error_tag : GText.tag
(** @return current status *)
- method grafite_status: GrafiteTypes.status
+ method status: GrafiteTypes.status
(** {2 Observers} *)
(** {2 History} *)
+ method activate : unit
method advance : ?statement:string -> unit -> unit
method retract : unit -> unit
method goto: [`Top | `Bottom | `Cursor] -> unit -> unit
method include_paths: string list
method assignFileName : string option -> unit (* to the current active file *)
method loadFromFile : string -> unit
- method loadFromString : string -> unit
method saveToFile : unit -> unit
- (** {2 Current proof} (if any) *)
-
- method stack: Continuationals.Stack.t (** @raise Statement_error *)
-
- method setGoal: int option -> unit
- method goal: int option
-
(** end of script, true if the whole script has been executed *)
method eos: bool
method bos: bool
method clean_dirty_lock: unit
method set_star: bool -> unit
method source_view: GSourceView2.source_view
+ method has_parent: GObj.widget -> bool
(* debug *)
method dump : unit -> unit
end
val script:
- urichooser: (GSourceView2.source_view -> NReference.reference list -> NReference.reference list) ->
- ask_confirmation:
- (title:string -> message:string -> [`YES | `NO | `CANCEL]) ->
- unit ->
- script
-
-(* each time script above is called an internal ref is set, instance will return
- * the value of this ref *)
-(* TODO Zack: orrible solution until we found a better one for having a single
- * access point for the script *)
+ parent:GBin.scrolled_window -> tab_label:GMisc.label -> unit -> script
+
+val destroy: int -> unit
val current: unit -> script
+val at_page: int -> script
+val iter_scripts: (script -> unit) -> unit