method addObserver : (GrafiteTypes.status -> unit) -> unit
+ (** {2 Unicode handling} *)
+ method nextSimilarSymbol: unit
+
+ (** {2 Undo/redo} *)
+
+ method safe_undo: unit
+ method safe_redo: unit
+
(** {2 History} *)
+ method activate : unit
method advance : ?statement:string -> unit -> unit
method retract : unit -> unit
method goto: [`Top | `Bottom | `Cursor] -> unit -> unit
method reset: unit -> unit
method template: unit -> unit
+ (** {2 Selections / clipboards handling} *)
+
+ method markupSelected: bool
+ method canCopy: bool
+ method canCut: bool
+ method canDelete: bool
+ (*CSC: WRONG CODE: we should look in the clipboard instead! *)
+ method canPaste: bool
+ method canPastePattern: bool
+
+ method copy: unit -> unit
+ method cut: unit -> unit
+ method delete: unit -> unit
+ method paste: unit -> unit
+ method pastePattern: unit -> unit
+
(** {2 Load/save} *)
method has_name: bool
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
- method filename : string
-
- (** {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
(** misc *)
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
- (** @param set_star callback used to set the modified symbol (usually a star
- * "*") on the side of a script name *)
val script:
- source_view:GSourceView2.source_view ->
- mathviewer: MatitaTypes.mathViewer->
- urichooser: (UriManager.uri list -> UriManager.uri list) ->
+ urichooser:
+ (GSourceView2.source_view -> NReference.reference list ->
+ NReference.reference list) ->
ask_confirmation:
(title:string -> message:string -> [`YES | `NO | `CANCEL]) ->
- set_star: (bool -> unit) ->
+ parent:GBin.scrolled_window ->
+ tab_label:GMisc.label ->
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 *)
+val destroy: int -> unit
val current: unit -> script
+val at_page: int -> script
+val iter_scripts: (script -> unit) -> unit