X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fmatita%2FmatitaMathView.ml;h=f81b2a2266677b43773d606608979792a604e412;hb=5c56a926588a63ceac31e6ddd6e3eeb02fadf3a9;hp=776a9ada579ce8748e8867ad98a1e22e27809ed5;hpb=a7b90d2494f7d580faa54ecd2835bd4649129763;p=helm.git

diff --git a/helm/matita/matitaMathView.ml b/helm/matita/matitaMathView.ml
index 776a9ada5..f81b2a226 100644
--- a/helm/matita/matitaMathView.ml
+++ b/helm/matita/matitaMathView.ml
@@ -26,18 +26,7 @@
 open Printf
 
 open MatitaTypes
-
-let list_map_fail f =
-  let rec aux = function
-    | [] -> []
-    | he::tl ->
-        try
-          let he' = f he in
-          he'::(aux tl)
-        with Exit ->
-          (aux tl)
-  in
-  aux
+open MatitaGtkMisc
 
 let add_trailing_slash =
   let rex = Pcre.regexp "/$" in
@@ -57,6 +46,12 @@ object (self)
 end
 
 let cicBrowsers = ref []
+let gui_instance = ref None
+let set_gui gui = gui_instance := Some gui
+let get_gui () =
+  match !gui_instance with
+  | None -> assert false
+  | Some gui -> gui
 
 let default_font_size () =
   Helm_registry.get_opt_default Helm_registry.int
@@ -66,52 +61,217 @@ let increase_font_size () = incr current_font_size
 let decrease_font_size () = decr current_font_size
 let reset_font_size () = current_font_size := default_font_size ()
 
+  (* is there any lablgtk2 constant corresponding to the various mouse
+   * buttons??? *)
+let left_button = 1
+let middle_button = 2
+let right_button = 3
+
+let near (x1, y1) (x2, y2) =
+  let distance = sqrt (((x2 -. x1) ** 2.) +. ((y2 -. y1) ** 2.)) in
+  (distance < 4.)
+
+let href_ds = Gdome.domString "href"
+let xref_ds = Gdome.domString "xref"
+
 class clickableMathView obj =
-  let href = Gdome.domString "href" in
-  let xref = Gdome.domString "xref" in
-  object (self)
-    inherit GMathViewAux.multi_selection_math_view obj
+let text_width = 80 in
+object (self)
+  inherit GMathViewAux.multi_selection_math_view obj
+
+  val mutable href_callback: (string -> unit) option = None
+  method set_href_callback f = href_callback <- f
+
+  val mutable _cic_info = None
+  method private set_cic_info info = _cic_info <- info
+  method private cic_info =
+    match _cic_info with
+    | Some info -> info
+    | None -> assert false
+
+  initializer
+    self#set_font_size !current_font_size;
+    ignore (self#connect#selection_changed self#choose_selection_cb);
+    ignore (self#event#connect#button_press self#button_press_cb);
+    ignore (self#event#connect#button_release self#button_release_cb);
+    ignore (self#event#connect#selection_clear self#selection_clear_cb);
+    ignore (self#coerce#misc#connect#selection_get self#selection_get_cb);
+    self#coerce#misc#add_selection_target
+      ~target:(Gdk.Atom.name Gdk.Atom.string) Gdk.Atom.primary
+
+  val mutable button_press_x = -1.
+  val mutable button_press_y = -1.
+  val mutable selection_changed = false
+(*   val mutable ignore_next_selection_clear = false *)
+
+  method private selection_get_cb ctxt ~info ~time =
+    (match self#get_selections with
+    | [] -> ()
+    | node :: _ -> ctxt#return (self#string_of_node node))
+
+  method private selection_clear_cb sel_event =
+    self#remove_selections;
+    false
+
+  method private button_press_cb gdk_button =
+    let button = GdkEvent.Button.button gdk_button in
+    if  button = left_button then begin
+      button_press_x <- GdkEvent.Button.x gdk_button;
+      button_press_y <- GdkEvent.Button.y gdk_button;
+      selection_changed <- false
+    end else if button = right_button then
+      self#popup_contextual_menu (GdkEvent.Button.time gdk_button);
+    false
+
+  method private popup_contextual_menu time =
+    match self#string_of_selection with
+    | None -> ()
+    | Some s ->
+        let clipboard = GData.clipboard Gdk.Atom.clipboard in
+        let menu = GMenu.menu () in
+        let copy_menu_item =
+          GMenu.image_menu_item
+            ~label:"_Copy" ~stock:`COPY ~packing:menu#append ()
+        in
+        connect_menu_item copy_menu_item (fun () -> clipboard#set_text s);
+        menu#popup ~button:right_button ~time
+
+  method private button_release_cb gdk_button =
+    let clipboard = GData.clipboard Gdk.Atom.primary in
+    if GdkEvent.Button.button gdk_button = left_button then begin
+      let button_release_x = GdkEvent.Button.x gdk_button in
+      let button_release_y = GdkEvent.Button.y gdk_button in
+      if selection_changed then
+        ()
+      else  (* selection _not_ changed *)
+        if near (button_press_x, button_press_y)
+          (button_release_x, button_release_y)
+        then
+          let x = int_of_float button_press_x in
+          let y = int_of_float button_press_y in
+          (match self#get_element_at x y with
+          | None -> ()
+          | Some elt ->
+              let namespaceURI = DomMisc.xlink_ns in
+              let localName = href_ds in
+              if elt#hasAttributeNS ~namespaceURI ~localName then
+                self#invoke_href_callback
+                  (elt#getAttributeNS ~namespaceURI ~localName)#to_string
+                  gdk_button
+              else
+                ignore (self#action_toggle elt));
+    end;
+    false
+
+  method private invoke_href_callback href_value gdk_button =
+    let button = GdkEvent.Button.button gdk_button in
+    if button = left_button then
+      let time = GdkEvent.Button.time gdk_button in
+      match href_callback with
+      | None -> ()
+      | Some f ->
+          (match MatitaMisc.split href_value with
+          | [ uri ] ->  f uri
+          | uris ->
+              let menu = GMenu.menu () in
+              List.iter
+                (fun uri ->
+                  let menu_item =
+                    GMenu.menu_item ~label:uri ~packing:menu#append ()
+                  in
+                  connect_menu_item menu_item (fun () -> f uri))
+                uris;
+              menu#popup ~button ~time)
+
+  method private choose_selection_cb gdome_elt =
+    let (gui: MatitaGuiTypes.gui) = get_gui () in
+    let clipboard = GData.clipboard 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);
+        ignore (self#coerce#misc#grab_selection Gdk.Atom.primary)
+      end else
+        try
+          (match elt#get_parentNode with
+          | None -> assert false
+          | Some p -> aux (new Gdome.element_of_node p))
+        with GdomeInit.DOMCastException _ -> ()
+    in
+    (match gdome_elt with
+    | Some elt -> aux elt
+    | None -> self#set_selection None);
+    selection_changed <- true
 
-    val mutable href_callback: (string -> unit) option = None
-    method set_href_callback f = href_callback <- f
+  method update_font_size = self#set_font_size !current_font_size
 
-    initializer
-      current_font_size := default_font_size ();
-      self#set_font_size !current_font_size;
-      ignore (self#connect#selection_changed self#choose_selection);
-      ignore (self#connect#click (fun (gdome_elt, _, _, _) ->
-        match gdome_elt with
-        | Some elt  (* element is an hyperlink, use href_callback on it *)
-          when elt#hasAttributeNS ~namespaceURI:Misc.xlink_ns ~localName:href ->
-            (match href_callback with
-            | None -> ()
-            | Some f ->
-                let uri =
-                  elt#getAttributeNS ~namespaceURI:Misc.xlink_ns ~localName:href
-                in
-                f (uri#to_string))
-        | Some elt -> ignore (self#action_toggle elt)
-        | None -> ()))
-    method private choose_selection gdome_elt =
-      let rec aux elt =
-        if elt#hasAttributeNS ~namespaceURI:Misc.helm_ns ~localName:xref then
-          self#set_selection (Some elt)
-        else
-          try
-            (match elt#get_parentNode with
-            | None -> assert false
-            | Some p -> aux (new Gdome.element_of_node p))
-          with GdomeInit.DOMCastException _ -> ()
-(*             debug_print "trying to select above the document root" *)
+  method private get_term_by_id context id =
+    let ids_to_terms, ids_to_hypotheses = self#cic_info in
+    try
+      `Term (Hashtbl.find ids_to_terms id)
+    with Not_found ->
+      try
+        let hyp = Hashtbl.find ids_to_hypotheses id in
+        let context' = MatitaMisc.list_tl_at hyp context in
+        `Hyp context'
+      with Not_found -> assert false
+    
+  method private string_of_node node =
+    let get_id (node: Gdome.element) =
+      let xref_attr =
+        node#getAttributeNS ~namespaceURI:DomMisc.helm_ns ~localName:xref_ds
+      in
+      xref_attr#to_string
+    in
+    let script = MatitaScript.instance () in
+    let metasenv = script#proofMetasenv in
+    let context = script#proofContext in
+    let conclusion = script#proofConclusion in
+(* TODO: code for patterns
+    let conclusion = (MatitaScript.instance ())#proofConclusion in
+    let conclusion_pattern =
+      ProofEngineHelpers.pattern_of ~term:conclusion cic_terms
+    in
+*)
+    let dummy_goal = ~-1 in
+    let string_of_cic_sequent cic_sequent =
+      let acic_sequent, _, _, ids_to_inner_sorts, _ =
+        Cic2acic.asequent_of_sequent metasenv cic_sequent
+      in
+      let _, _, _, annterm = acic_sequent in
+      let ast, ids_to_uris =
+        CicNotationRew.ast_of_acic ids_to_inner_sorts annterm
       in
-      match gdome_elt with
-      | Some elt -> aux elt
-      | None   -> self#set_selection None
+      let pped_ast = CicNotationRew.pp_ast ast in
+      let markup = CicNotationPres.render ids_to_uris pped_ast in
+      BoxPp.render_to_string text_width markup
+    in
+    let term = self#get_term_by_id context (get_id node) in
+    let cic_sequent =
+      match term with
+      | `Term t ->
+          let context' =
+            ProofEngineHelpers.locate_in_conjecture t
+              (dummy_goal, context, conclusion)
+          in
+          dummy_goal, context', t
+      | `Hyp context -> dummy_goal, context, Cic.Rel 1
+    in
+    string_of_cic_sequent cic_sequent
 
-    method update_font_size = 
-      self#set_font_size !current_font_size
-      
-  end
+  method string_of_selections =
+    List.map self#string_of_node (List.rev self#get_selections)
+
+  method string_of_selection =
+    match self#get_selections with
+    | [] -> None
+    | node :: _ -> Some (self#string_of_node node)
+
+end
 
 let clickableMathView ?hadjustment ?vadjustment ?font_size ?log_verbosity =
   GtkBase.Widget.size_params
@@ -122,56 +282,18 @@ let clickableMathView ?hadjustment ?vadjustment ?font_size ?log_verbosity =
     []
 
 class sequentViewer obj =
-  object(self)
-
-    inherit clickableMathView obj
+object (self)
+  inherit clickableMathView obj
 
-    val mutable current_infos = None
-    
-    method get_selected_terms =
-      let selections = self#get_selections in
-      list_map_fail
-        (fun node ->
-          let xpath =
-            ((node : Gdome.element)#getAttributeNS
-              ~namespaceURI:Misc.helm_ns
-              ~localName:(Gdome.domString "xref"))#to_string
-          in
-          if xpath = "" then assert false (* "ERROR: No xref found!!!" *)
-          else
-            match current_infos with
-            | Some (ids_to_terms,_,_) ->
-                (try Hashtbl.find ids_to_terms xpath with _ -> raise Exit)
-            | None -> assert false) (* "ERROR: No current term!!!" *)
-        selections
-
-    method get_selected_hypotheses =
-      let selections = self#get_selections in
-      list_map_fail
-        (fun node ->
-          let xpath =
-            ((node : Gdome.element)#getAttributeNS
-              ~namespaceURI:Misc.helm_ns
-              ~localName:(Gdome.domString "xref"))#to_string
-          in
-          if xpath = "" then assert false (* "ERROR: No xref found!!!" *)
-          else
-            match current_infos with
-            | Some (_,_,ids_to_hypotheses) ->
-                (try Hashtbl.find ids_to_hypotheses xpath with _ -> raise Exit)
-            | None -> assert false) (* "ERROR: No current term!!!" *)
-        selections
-  
   method load_sequent metasenv metano =
     let sequent = CicUtil.lookup_meta metano metasenv in
-    let (mathml,(_,(ids_to_terms, ids_to_father_ids, ids_to_hypotheses,_))) =
+    let (mathml, (_, (ids_to_terms, _, ids_to_hypotheses,_ ))) =
       ApplyTransformation.mml_of_cic_sequent metasenv sequent
     in
-    current_infos <- Some (ids_to_terms, ids_to_father_ids, ids_to_hypotheses);
-(*
-    debug_print "load_sequent: dumping MathML to ./prova";
-    ignore (Misc.domImpl#saveDocumentToFile ~name:"./prova" ~doc:mathml ());
-*)
+    self#set_cic_info (Some (ids_to_terms, ids_to_hypotheses));
+    let name = "sequent_viewer.xml" in
+    MatitaLog.debug ("load_sequent: dumping MathML to ./" ^ name);
+    ignore (DomMisc.domImpl#saveDocumentToFile ~name ~doc:mathml ());
     self#load_root ~root:mathml#get_documentElement
  end
 
@@ -229,7 +351,14 @@ class sequentsViewer ~(notebook:GPack.notebook)
           scrolledWin <- Some w;
           match sequentViewer#misc#parent with
           | None -> w#add sequentViewer#coerce
-          | Some _ -> sequentViewer#misc#reparent w#coerce
+          | Some parent ->
+             let parent =
+              match sequentViewer#misc#parent with
+                 None -> assert false
+               | Some p -> GContainer.cast_container p
+             in
+              parent#remove sequentViewer#coerce;
+              w#add sequentViewer#coerce
         in
         goal2win <- (metano, reparent) :: goal2win;
         w#coerce
@@ -301,14 +430,11 @@ type term_source =
   | `String of string
   ]
 
-exception Browser_failure of string
-
-class type cicBrowser =
-object
-  method load: MatitaTypes.mathViewer_entry -> unit
-  (* method loadList: string list -> MatitaTypes.mathViewer_entry-> unit *)
-  method loadInput: string -> unit
-end
+let reloadable = function
+  | `About `Current_proof
+  | `Dir _ ->
+      true
+  | _ -> false
 
 class cicBrowser_impl ~(history:MatitaTypes.mathViewer_entry MatitaMisc.history)
   ()
@@ -317,17 +443,17 @@ class cicBrowser_impl ~(history:MatitaTypes.mathViewer_entry MatitaMisc.history)
   let whelp_RE = Pcre.regexp "^\\s*whelp" in
   let uri_RE =
     Pcre.regexp
-      "^cic:/(\\w+/)*\\w+\\.(con|ind|var)(#xpointer\\(\\d+(/\\d+)+\\))?$"
+      "^cic:/([^/]+/)*[^/]+\\.(con|ind|var)(#xpointer\\(\\d+(/\\d+)+\\))?$"
   in
-  let dir_RE = Pcre.regexp "^cic:((/(\\w+/)*\\w+(/)?)|/|)$" in
+  let dir_RE = Pcre.regexp "^cic:((/([^/]+/)*[^/]+(/)?)|/|)$" in
   let whelp_query_RE = Pcre.regexp "^\\s*whelp\\s+([^\\s]+)\\s+(.*)$" in
   let trailing_slash_RE = Pcre.regexp "/$" in
   let has_xpointer_RE = Pcre.regexp "#xpointer\\(\\d+/\\d+(/\\d+)?\\)$" in
   let is_whelp txt = Pcre.pmatch ~rex:whelp_RE txt in
   let is_uri txt = Pcre.pmatch ~rex:uri_RE txt in
   let is_dir txt = Pcre.pmatch ~rex:dir_RE txt in
-  let gui = MatitaGui.instance () in
-  let win = gui#newBrowserWin () in
+  let gui = get_gui () in
+  let (win: MatitaGuiTypes.browserWin) = gui#newBrowserWin () in
   let queries = ["Locate";"Hint";"Match";"Elim";"Instance"] in
   let combo,_ = GEdit.combo_box_text ~strings:queries () in
   let activate_combo_query input q =
@@ -351,9 +477,9 @@ class cicBrowser_impl ~(history:MatitaTypes.mathViewer_entry MatitaMisc.history)
   in
   let toplevel = win#toplevel in
   let mathView = sequentViewer ~packing:win#scrolledBrowser#add () in
-  let fail msg =
-    ignore (MatitaGtkMisc.ask_confirmation ~gui:(MatitaGui.instance ())
-      ~title:"Cic browser" ~msg ~cancel:false ());
+  let fail message = 
+    MatitaGtkMisc.report_error ~title:"Cic browser" ~message 
+      ~parent:toplevel ()  
   in
   let tags =
     [ "dir", GdkPixbuf.from_file (MatitaMisc.image_path "matita-folder.png");
@@ -362,8 +488,7 @@ class cicBrowser_impl ~(history:MatitaTypes.mathViewer_entry MatitaMisc.history)
   let handle_error f =
     try
       f ()
-    with exn ->
-      fail (sprintf "Uncaught exception:\n%s" (Printexc.to_string exn))
+    with exn -> fail (MatitaExcPp.to_string exn)
   in
   let handle_error' f = (fun () -> handle_error (fun () -> f ())) in
   object (self)
@@ -405,9 +530,11 @@ class cicBrowser_impl ~(history:MatitaTypes.mathViewer_entry MatitaMisc.history)
           GMain.quit ();
         false));
       ignore(win#whelpResultTreeview#connect#row_activated 
-        ~callback:(fun _ _ -> self#loadInput (self#_getSelectedUri ())));
+        ~callback:(fun _ _ ->
+          handle_error (fun () -> self#loadInput (self#_getSelectedUri ()))));
       mathView#set_href_callback (Some (fun uri ->
-        handle_error (fun () -> self#load (`Uri (UriManager.uri_of_string uri)))));
+        handle_error (fun () ->
+          self#load (`Uri (UriManager.uri_of_string uri)))));
       self#_load (`About `Blank);
       toplevel#show ()
 
@@ -418,10 +545,15 @@ class cicBrowser_impl ~(history:MatitaTypes.mathViewer_entry MatitaMisc.history)
     val model =
       new MatitaGtkMisc.taggedStringListModel tags win#whelpResultTreeview
 
+    val mutable lastDir = ""  (* last loaded "directory" *)
+
+    method mathView = (mathView :> MatitaGuiTypes.clickableMathView)
+
     method private _getSelectedUri () =
       match model#easy_selection () with
       | [sel] when is_uri sel -> sel  (* absolute URI selected *)
-      | [sel] -> win#browserUri#entry#text ^ sel  (* relative URI selected *)
+(*       | [sel] -> win#browserUri#entry#text ^ sel  |+ relative URI selected +| *)
+      | [sel] -> lastDir ^ sel
       | _ -> assert false
 
     (** history RATIONALE 
@@ -468,25 +600,22 @@ class cicBrowser_impl ~(history:MatitaTypes.mathViewer_entry MatitaMisc.history)
       * @param uri string *)
     method private _load entry =
       try
-          if entry <> current_entry || entry = `About `Current_proof then begin
-            (match entry with
-            | `About `Current_proof -> self#home ()
-            | `About `Blank -> self#blank ()
-            | `About `Us -> () (* TODO implement easter egg here :-] *)
-            | `Check term -> self#_loadCheck term
-            | `Cic (term, metasenv) -> self#_loadTermCic term metasenv
-            | `Dir dir -> self#_loadDir dir
-            | `Uri uri -> self#_loadUriManagerUri uri
-            | `Whelp (query, results) -> 
-                set_whelp_query query;
-                self#_loadList (List.map (fun r -> "obj", UriManager.string_of_uri r) results));
-            self#setEntry entry
-          end
-      with
-      | UriManager.IllFormedUri uri -> fail (sprintf "invalid uri: %s" uri)
-      | CicEnvironment.Object_not_found uri ->
-          fail (sprintf "object not found: %s" (UriManager.string_of_uri uri))
-      | Browser_failure msg -> fail msg
+        if entry <> current_entry || reloadable entry then begin
+          (match entry with
+          | `About `Current_proof -> self#home ()
+          | `About `Blank -> self#blank ()
+          | `About `Us -> () (* TODO implement easter egg here :-] *)
+          | `Check term -> self#_loadCheck term
+          | `Cic (term, metasenv) -> self#_loadTermCic term metasenv
+          | `Dir dir -> self#_loadDir dir
+          | `Uri uri -> self#_loadUriManagerUri uri
+          | `Whelp (query, results) -> 
+              set_whelp_query query;
+              self#_loadList (List.map (fun r -> "obj",
+                UriManager.string_of_uri r) results));
+          self#setEntry entry
+        end
+      with exn -> fail (MatitaExcPp.to_string exn)
 
     method private blank () =
       self#_showMath;
@@ -519,13 +648,15 @@ class cicBrowser_impl ~(history:MatitaTypes.mathViewer_entry MatitaMisc.history)
     method private _loadDir dir = 
       let content = Http_getter.ls dir in
       let l =
-        List.map
-          (function 
-            | Http_getter_types.Ls_section s -> "dir", s
-            | Http_getter_types.Ls_object o -> "obj", o.Http_getter_types.uri)
-          content
+        List.fast_sort
+          Pervasives.compare
+          (List.map
+            (function 
+              | Http_getter_types.Ls_section s -> "dir", s
+              | Http_getter_types.Ls_object o -> "obj", o.Http_getter_types.uri)
+            content)
       in
-      if l = [] then raise (Browser_failure "no such directory");
+      lastDir <- dir;
       self#_loadList l
 
     method private setEntry entry =
@@ -538,18 +669,21 @@ class cicBrowser_impl ~(history:MatitaTypes.mathViewer_entry MatitaMisc.history)
        * if the widget is not mapped (hidden by the notebook)
        * the document is not rendered *)
       let use_diff = false in (* ZACK TODO use XmlDiff when re-rendering? *)
-      let (mathml, (_,(ids_to_terms, ids_to_father_ids, ids_to_conjectures,
-           ids_to_hypotheses,_,_))) =
+      let (mathml, (_,((ids_to_terms, ids_to_father_ids, ids_to_conjectures,
+           ids_to_hypotheses, ids_to_inner_sorts, ids_to_inner_types) as info)))
+      =
         ApplyTransformation.mml_of_cic_object obj
       in
-      current_infos <- Some (ids_to_terms, ids_to_father_ids,
-        ids_to_conjectures, ids_to_hypotheses);
+      current_infos <- Some info;
       (match current_mathml with
       | Some current_mathml when use_diff ->
           mathView#freeze;
           XmlDiff.update_dom ~from:current_mathml mathml;
           mathView#thaw
       |  _ ->
+          let name = "cic_browser.xml" in
+          MatitaLog.debug ("cic_browser: dumping MathML to ./" ^ name);
+          ignore (DomMisc.domImpl#saveDocumentToFile ~name ~doc:mathml ());
           mathView#load_root ~root:mathml#get_documentElement;
           current_mathml <- Some mathml);
 
@@ -589,7 +723,7 @@ class cicBrowser_impl ~(history:MatitaTypes.mathViewer_entry MatitaMisc.history)
               (try
                 entry_of_string txt
               with Invalid_argument _ ->
-                raise (Browser_failure (sprintf "unsupported uri: %s" txt)))
+                command_error (sprintf "unsupported uri: %s" txt))
         in
         self#_load entry;
         self#_historyAdd entry
@@ -605,10 +739,9 @@ class cicBrowser_impl ~(history:MatitaTypes.mathViewer_entry MatitaMisc.history)
     method history = history
     method currentEntry = current_entry
     method refresh () =
-      if current_entry = `About `Current_proof then
-      self#_load (`About `Current_proof) 
-  end
+      if reloadable current_entry then self#_load current_entry
 
+  end
   
 let sequentsViewer ~(notebook:GPack.notebook)
   ~(sequentViewer:sequentViewer) ()
@@ -633,7 +766,7 @@ let cicBrowser () =
       GdkKeysyms._W (fun () -> win#toplevel#destroy ());
 *)
     cicBrowsers := browser :: !cicBrowsers;
-    (browser :> cicBrowser)
+    (browser :> MatitaGuiTypes.cicBrowser)
   in
   let history = new MatitaMisc.browser_history size (`About `Blank) in
   aux history
@@ -642,7 +775,7 @@ let default_sequentViewer () = sequentViewer ~show:true ()
 let sequentViewer_instance = MatitaMisc.singleton default_sequentViewer
 
 let default_sequentsViewer () =
-  let gui = MatitaGui.instance () in
+  let gui = get_gui () in
   let sequentViewer = sequentViewer_instance () in
   sequentsViewer ~notebook:gui#main#sequentsNotebook ~sequentViewer ()
 let sequentsViewer_instance = MatitaMisc.singleton default_sequentsViewer
@@ -653,7 +786,7 @@ let mathViewer () =
       if reuse then
         (match !cicBrowsers with
         | [] -> cicBrowser ()
-        | b :: _ -> (b :> cicBrowser))
+        | b :: _ -> (b :> MatitaGuiTypes.cicBrowser))
       else
         (cicBrowser ())
           
@@ -669,3 +802,24 @@ let update_font_sizes () =
   List.iter (fun b -> b#updateFontSize) !cicBrowsers;
   (sequentViewer_instance ())#update_font_size
 
+let get_math_views () =
+  ((sequentViewer_instance ()) :> MatitaGuiTypes.clickableMathView)
+  :: (List.map (fun b -> b#mathView) !cicBrowsers)
+
+let get_selections () =
+  if (MatitaScript.instance ())#onGoingProof () then
+    let rec aux =
+      function
+      | [] -> None
+      | mv :: tl ->
+          (match mv#string_of_selections with
+          | [] -> aux tl
+          | sels -> Some sels)
+    in
+    aux (get_math_views ())
+  else
+    None
+
+let reset_selections () =
+  List.iter (fun mv -> mv#remove_selections) (get_math_views ())
+