X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fmatita%2FmatitaMathView.ml;h=586ff14796938f4c82b2ccd5ec6837c06f6ef2e0;hb=3a12950125e7a4a792546aacea40505f3cecae89;hp=de08f538ebf2e4ee181c2a0a76197c42807a1a2e;hpb=ea525d45c3005d239ab964f88afadc98b08fcae9;p=helm.git

diff --git a/helm/matita/matitaMathView.ml b/helm/matita/matitaMathView.ml
index de08f538e..586ff1479 100644
--- a/helm/matita/matitaMathView.ml
+++ b/helm/matita/matitaMathView.ml
@@ -28,17 +28,6 @@ open Printf
 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)
@@ -140,18 +129,15 @@ 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;
@@ -162,7 +148,6 @@ object (self)
     false
 
   method private popup_contextual_menu time =
-(*     prerr_endline "popup_contextual_menu"; *)
     match self#string_of_selection with
     | None -> ()
     | Some s ->
@@ -398,9 +383,13 @@ class sequentsViewer ~(notebook:GPack.notebook) ~(cicMathView:cicMathView) () =
     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:(BuildTimeConf.runtime_base_dir ^ "/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;
@@ -443,7 +432,7 @@ class sequentsViewer ~(notebook:GPack.notebook) ~(cicMathView:cicMathView) () =
       self#script#setGoal goal;
       let win metano =
         let w =
-          GBin.scrolled_window ~hpolicy:`AUTOMATIC ~vpolicy:`AUTOMATIC
+          GBin.scrolled_window ~hpolicy:`AUTOMATIC ~vpolicy:`ALWAYS
             ~shadow_type:`IN ~show:true ()
         in
         let reparent () =
@@ -780,7 +769,7 @@ class cicBrowser_impl ~(history:MatitaTypes.mathViewer_entry MatitaMisc.history)
 
     (**  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))
@@ -792,7 +781,7 @@ class cicBrowser_impl ~(history:MatitaTypes.mathViewer_entry MatitaMisc.history)
         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