X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2FmatitaMisc.mli;h=07a327cc90a2cf0c3c44eb81aedc054f70eb7240;hb=refs%2Fheads%2Fmaster;hp=eec60932d69a0db08a5083c95543fcfa59c73d38;hpb=2c01ff6094173915e7023076ea48b5804dca7778;p=helm.git diff --git a/matita/matita/matitaMisc.mli b/matita/matita/matitaMisc.mli index eec60932d..07a327cc9 100644 --- a/matita/matita/matitaMisc.mli +++ b/matita/matita/matitaMisc.mli @@ -35,7 +35,8 @@ val is_proof_object: string -> bool * it *) val append_phrase_sep: string -> string -val normalize_dir: string -> string (** add trailing "/" if missing *) + (** add trailing "/" if missing *) +val normalize_dir: string -> string val strip_suffix: suffix:string -> string -> string (** @return tl tail of a list starting at a given element @@ -50,8 +51,12 @@ type 'a memento class type ['a] history = object ('b) method add : 'a -> unit - method next : 'a (** @raise History_failure *) - method previous : 'a (** @raise History_failure *) + + (** @raise History_failure *) + method next : 'a + + (** @raise History_failure *) + method previous : 'a method load: 'a memento -> unit method save: 'a memento method is_begin: bool @@ -74,8 +79,20 @@ val singleton: (unit -> 'a) -> (unit -> 'a) (** given the base name of an image, returns its full path *) val image_path: string -> string - (** 2>/dev/null, HLog = (fun _ -> ()) *) -val shutup: unit -> unit - (** outputs the preamble of a generated .ma file *) val out_preamble: out_channel -> unit + +val left_button: int +val right_button: int + +(** {2 Global changes} *) + +val observe_font_size: (int -> unit) -> unit +val get_current_font_size: unit -> int +val increase_font_size: unit -> unit +val decrease_font_size: unit -> unit +val reset_font_size: unit -> unit + +(** CSC: these functions should completely disappear (bad design) *) +val set_gui: MatitaGuiTypes.gui -> unit +val get_gui: unit -> MatitaGuiTypes.gui