- added integrity checks on .moo files

[helm.git] / helm / matita / matitaMathView.ml

diff --git a/helm/matita/matitaMathView.ml b/helm/matita/matitaMathView.ml
index 532c3dd975a3a2fe4d1364dca912273a51562fd0..6074fdae75e51717d83fb9fc437cf31c3251db18 100644 (file)
--- a/helm/matita/matitaMathView.ml
+++ b/helm/matita/matitaMathView.ml
@@ -206,7 +206,7 @@ object (self)
       match href_callback with
       | None -> ()
       | Some f ->
-          (match MatitaMisc.split href_value with
+          (match HExtlib.split href_value with
           | [ uri ] ->  f uri
           | uris ->
               let menu = GMenu.menu () in
@@ -404,11 +404,11 @@ class sequentsViewer ~(notebook:GPack.notebook) ~(cicMathView:cicMathView) () =
     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") ()
+      ~file:(MatitaMisc.image_path "matita_medium.png") ()
       :> GObj.widget)
             
     val logo_with_qed = (GMisc.image
-      ~file:(BuildTimeConf.runtime_base_dir ^ "/logo/matita_small.png") ()
+      ~file:(MatitaMisc.image_path "matita_small.png") ()
       :> GObj.widget)
 
     method load_logo =
@@ -590,9 +590,15 @@ class cicBrowser_impl ~(history:MatitaTypes.mathViewer_entry MatitaMisc.history)
   let handle_error f =
     try
       f ()
-    with exn -> fail (MatitaExcPp.to_string exn)
+    with exn ->
+      if Helm_registry.get_bool "matita.catch_top_level_exn" then
+        fail (MatitaExcPp.to_string exn)
+      else raise exn
   in
   let handle_error' f = (fun () -> handle_error (fun () -> f ())) in
+  let load_easter_egg = lazy (
+    win#easterEggImage#set_file (MatitaMisc.image_path "meegg.png"))
+  in
   object (self)
     inherit scriptAccessor
     
@@ -682,9 +688,9 @@ class cicBrowser_impl ~(history:MatitaTypes.mathViewer_entry MatitaMisc.history)
      * 
      * Use only these functions to switch between the tabs
      *)
-    method private _showList = win#mathOrListNotebook#goto_page 1
     method private _showMath = win#mathOrListNotebook#goto_page 0
-    
+    method private _showList = win#mathOrListNotebook#goto_page 1
+
     method private back () =
       try
         self#_load (self#_historyPrev ())
@@ -698,13 +704,13 @@ class cicBrowser_impl ~(history:MatitaTypes.mathViewer_entry MatitaMisc.history)
       (* loads a uri which can be a cic uri or an about:* uri
       * @param uri string *)
     method private _load ?(force=false) entry =
-      try
+      handle_error (fun () ->
        if entry <> current_entry || entry = `About `Current_proof || force then
         begin
           (match entry with
           | `About `Current_proof -> self#home ()
           | `About `Blank -> self#blank ()
-          | `About `Us -> () (* TODO implement easter egg here :-] *)
+          | `About `Us -> self#egg ()
           | `Check term -> self#_loadCheck term
           | `Cic (term, metasenv) -> self#_loadTermCic term metasenv
           | `Dir dir -> self#_loadDir dir
@@ -714,8 +720,7 @@ class cicBrowser_impl ~(history:MatitaTypes.mathViewer_entry MatitaMisc.history)
               self#_loadList (List.map (fun r -> "obj",
                 UriManager.string_of_uri r) results));
           self#setEntry entry
-        end
-      with exn -> fail (MatitaExcPp.to_string exn)
+        end)
 
     method private blank () =
       self#_showMath;
@@ -725,15 +730,19 @@ class cicBrowser_impl ~(history:MatitaTypes.mathViewer_entry MatitaMisc.history)
       failwith "not implemented _loadCheck";
       self#_showMath
 
+    method private egg () =
+      win#mathOrListNotebook#goto_page 2;
+      Lazy.force load_easter_egg
+
     method private home () =
       self#_showMath;
       match self#script#status.proof_status with
       | Proof  (uri, metasenv, bo, ty) ->
-          let name = UriManager.name_of_uri (MatitaMisc.unopt uri) in
+          let name = UriManager.name_of_uri (HExtlib.unopt uri) in
           let obj = Cic.CurrentProof (name, metasenv, bo, ty, [], []) in
           self#_loadObj obj
       | Incomplete_proof ((uri, metasenv, bo, ty), _) -> 
-          let name = UriManager.name_of_uri (MatitaMisc.unopt uri) in
+          let name = UriManager.name_of_uri (HExtlib.unopt uri) in
           let obj = Cic.CurrentProof (name, metasenv, bo, ty, [], []) in
           self#_loadObj obj
       | _ -> self#blank ()
@@ -789,7 +798,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 = MatitaMisc.trim_blanks txt in
+      let txt = HExtlib.trim_blanks txt in
       let fix_uri txt =
         UriManager.string_of_uri
           (UriManager.strip_xpointer (UriManager.uri_of_string txt))