open MatitaTypes
open MatitaGtkMisc
-let add_trailing_slash =
- let rex = Pcre.regexp "/$" in
- fun s ->
- if Pcre.pmatch ~rex s then s
- else s ^ "/"
-
-let strip_blanks =
- let rex = Pcre.regexp "^\\s*([^\\s]*)\\s*$" in
- fun s ->
- (Pcre.extract ~rex s).(1)
-
(** inherit from this class if you want to access current script *)
class scriptAccessor =
object (self)
val mutable selection_changed = false
method private selection_get_cb ctxt ~info ~time =
-(* prerr_endline "selection_get_cb"; *)
(match self#get_selections with
| [] -> ()
| node :: _ -> ctxt#return (self#string_of_node node))
method private selection_clear_cb sel_event =
-(* prerr_endline "selection_clear_cb"; *)
self#remove_selections;
false
method private button_press_cb gdk_button =
-(* prerr_endline "button_press_cb"; *)
let button = GdkEvent.Button.button gdk_button in
if button = left_button then begin
button_press_x <- GdkEvent.Button.x gdk_button;
false
method private popup_contextual_menu time =
-(* prerr_endline "popup_contextual_menu"; *)
match self#string_of_selection with
| None -> ()
| Some s ->
val mutable _metasenv = []
val mutable scrolledWin: GBin.scrolled_window option = None
(* scrolled window to which the sequentViewer is currently attached *)
- val logo = (GMisc.image ~file:(BuildTimeConf.runtime_base_dir ^ "/logo/matita_medium.png") () :> GObj.widget)
+ val logo = (GMisc.image
+ ~file:(BuildTimeConf.runtime_base_dir ^ "/logo/matita_medium.png") ()
+ :> GObj.widget)
- val logo_with_qed = (GMisc.image ~file:"logo/matita_small.png" () :> GObj.widget)
+ val logo_with_qed = (GMisc.image
+ ~file:(BuildTimeConf.runtime_base_dir ^ "/logo/matita_small.png") ()
+ :> GObj.widget)
method load_logo =
notebook#set_show_tabs false;
(** this is what the browser does when you enter a string an hit enter *)
method loadInput txt =
- let txt = strip_blanks txt in
+ let txt = MatitaMisc.trim_blanks txt in
let fix_uri txt =
UriManager.string_of_uri
(UriManager.strip_xpointer (UriManager.uri_of_string txt))
let entry =
match txt with
| txt when is_uri txt -> `Uri (UriManager.uri_of_string (fix_uri txt))
- | txt when is_dir txt -> `Dir (add_trailing_slash txt)
+ | txt when is_dir txt -> `Dir (MatitaMisc.normalize_dir txt)
| txt ->
(try
entry_of_string txt