]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/matita/matitaMathView.ml
- avoid catching top level exceptions when the relevant setting in the registry is set
[helm.git] / helm / matita / matitaMathView.ml
index 4bbaaddea52c08dc92738b0bf6503f4b097e5cf4..28bd1caaa7f35ae3244c3fc19ce93d120fddc656 100644 (file)
@@ -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)
@@ -111,10 +100,22 @@ let find_root_id annobj id ids_to_father_ids ids_to_terms ids_to_inner_types =
   | Cic.ACurrentProof (_, _, _, _, bo, ty, _, _) ->
       return_father id (mk_ids (ty :: bo :: inner_types))
   | Cic.AConstant (_, _, _, None, ty, _, _)
-  | Cic.AVariable (_, _, None, ty, _, _) -> return_father id (mk_ids (ty::inner_types))
+  | Cic.AVariable (_, _, None, ty, _, _) ->
+      return_father id (mk_ids (ty::inner_types))
   | Cic.AInductiveDefinition _ ->
       assert false  (* TODO *)
 
+  (** @return string content of a dom node having a single text child node, e.g.
+   * <m:mi xlink:href="...">bool</m:mi> *)
+let string_of_dom_node node =
+  match node#get_firstChild with
+  | None -> ""
+  | Some node ->
+      (try
+        let text = new Gdome.text_of_node node in
+        text#get_data#to_string
+      with GdomeInit.DOMCastException _ -> "")
+
 class clickableMathView obj =
 let text_width = 80 in
 object (self)
@@ -140,18 +141,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 +160,6 @@ object (self)
     false
 
   method private popup_contextual_menu time =
-(*     prerr_endline "popup_contextual_menu"; *)
     match self#string_of_selection with
     | None -> ()
     | Some s ->
@@ -225,18 +222,18 @@ object (self)
   method private choose_selection_cb gdome_elt =
     let (gui: MatitaGuiTypes.gui) = get_gui () in
     let clipboard = GData.clipboard Gdk.Atom.primary in
+    let set_selection elt =
+      self#set_selection (Some elt);
+      self#coerce#misc#add_selection_target
+        ~target:(Gdk.Atom.name Gdk.Atom.string) Gdk.Atom.primary;
+      ignore (self#coerce#misc#grab_selection Gdk.Atom.primary)
+    in
     let rec aux elt =
       if (elt#getAttributeNS ~namespaceURI:DomMisc.helm_ns
             ~localName:xref_ds)#to_string <> ""
-(*         if elt#hasAttributeNS ~namespaceURI:DomMisc.helm_ns ~localName:xref_ds
-        && (elt#getAttributeNS ~namespaceURI:DomMisc.helm_ns
-            ~localName:xref_ds)#to_string <> "" *)
-      then begin
-        self#set_selection (Some elt);
-        self#coerce#misc#add_selection_target
-          ~target:(Gdk.Atom.name Gdk.Atom.string) Gdk.Atom.primary;
-        ignore (self#coerce#misc#grab_selection Gdk.Atom.primary)
-      end else
+      then
+        set_selection elt
+      else
         try
           (match elt#get_parentNode with
           | None -> assert false
@@ -244,6 +241,9 @@ object (self)
         with GdomeInit.DOMCastException _ -> ()
     in
     (match gdome_elt with
+    | Some elt when (elt#getAttributeNS ~namespaceURI:DomMisc.xlink_ns
+        ~localName:href_ds)#to_string <> "" ->
+          set_selection elt
     | Some elt -> aux elt
     | None -> self#set_selection None);
     selection_changed <- true
@@ -272,6 +272,11 @@ object (self)
          (try Hashtbl.find ids_to_terms id with Not_found -> assert false)
 
   method private string_of_node node =
+    if node#hasAttributeNS ~namespaceURI:DomMisc.xlink_ns ~localName:href_ds
+    then string_of_dom_node node
+    else self#string_of_id_node node
+
+  method private string_of_id_node node =
     let get_id (node: Gdome.element) =
       let xref_attr =
         node#getAttributeNS ~namespaceURI:DomMisc.helm_ns ~localName:xref_ds
@@ -398,9 +403,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:(MatitaMisc.image_path "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:(MatitaMisc.image_path "matita_small.png") ()
+      :> GObj.widget)
 
     method load_logo =
      notebook#set_show_tabs false;
@@ -421,19 +430,19 @@ class sequentsViewer ~(notebook:GPack.notebook) ~(cicMathView:cicMathView) () =
           w#remove cicMathView#coerce;
           scrolledWin <- None
       | None -> ());
-      for i = 0 to pages do notebook#remove_page 0 done;
+      (match switch_page_callback with
+      | Some id ->
+          GtkSignal.disconnect notebook#as_widget id;
+          switch_page_callback <- None
+      | None -> ());
+      for i = 0 to pages do notebook#remove_page 0 done; 
       notebook#set_show_tabs true;
       pages <- 0;
       page2goal <- [];
       goal2page <- [];
       goal2win <- [];
-      _metasenv <- [];
+      _metasenv <- []; 
       self#script#setGoal ~-1;
-      (match switch_page_callback with
-      | Some id ->
-          GtkSignal.disconnect notebook#as_widget id;
-          switch_page_callback <- None
-      | None -> ())
 
     method load_sequents (status: ProofEngineTypes.status) =
       let ((_, metasenv, _, _), goal) = status in
@@ -443,7 +452,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 () =
@@ -581,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
     
@@ -673,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 ())
@@ -689,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
@@ -705,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;
@@ -716,6 +730,10 @@ 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
@@ -780,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 = 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 +810,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