X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fmatita%2FmatitaMathView.ml;h=5fe955b3ea5f8124e428b0a7fd28f1815472ee26;hb=6b8da04f526b3484dc92f61a23a8e61e63422c13;hp=7aa54f2c74ed03a3407bc4b4d18e5165f67c6da3;hpb=393b5943416585d0612ec62b795ceee34adb8dd7;p=helm.git

diff --git a/helm/matita/matitaMathView.ml b/helm/matita/matitaMathView.ml
index 7aa54f2c7..5fe955b3e 100644
--- a/helm/matita/matitaMathView.ml
+++ b/helm/matita/matitaMathView.ml
@@ -1,4 +1,4 @@
-(* Copyright (C) 2000-2002, HELM Team.
+(* Copyright (C) 2004-2005, HELM Team.
  * 
  * This file is part of HELM, an Hypertextual, Electronic
  * Library of Mathematics, developed at the Computer Science
@@ -25,26 +25,27 @@
 
 open Printf
 
-open MatitaCicMisc
 open MatitaTypes
 
-(* List utility functions *)
-exception Skip
-
 let list_map_fail f =
- let rec aux =
-  function
-     [] -> []
-   | he::tl ->
-      try
-       let he' = f he in
-        he'::(aux tl)
-      with Skip ->
-       (aux tl)
- in
+  let rec aux = function
+    | [] -> []
+    | he::tl ->
+        try
+          let he' = f he in
+          he'::(aux tl)
+        with Exit ->
+          (aux tl)
+  in
   aux
 
-class clickable_math_view obj =
+(** inherit from this class if you want to access current script *)
+class scriptAccessor =
+object (self)
+  method private script = MatitaScript.instance ()
+end
+
+class clickableMathView obj =
   let href = Gdome.domString "href" in
   let xref = Gdome.domString "xref" in
   object (self)
@@ -85,18 +86,18 @@ class clickable_math_view obj =
       | None   -> self#set_selection None
   end
 
-let clickable_math_view ?hadjustment ?vadjustment ?font_size ?log_verbosity =
+let clickableMathView ?hadjustment ?vadjustment ?font_size ?log_verbosity =
   GtkBase.Widget.size_params
     ~cont:(OgtkMathViewProps.pack_return (fun p ->
       OgtkMathViewProps.set_params
-        (new clickable_math_view (GtkMathViewProps.MathView_GMetaDOM.create p))
+        (new clickableMathView (GtkMathViewProps.MathView_GMetaDOM.create p))
         ~font_size:None ~log_verbosity:None))
     []
 
-class sequent_viewer obj =
+class sequentViewer obj =
   object(self)
 
-    inherit clickable_math_view obj
+    inherit clickableMathView obj
 
     val mutable current_infos = None
 
@@ -113,9 +114,7 @@ class sequent_viewer obj =
           else
             match current_infos with
             | Some (ids_to_terms,_,_) ->
-                (try
-                  Hashtbl.find ids_to_terms xpath
-                 with _ -> raise Skip)
+                (try Hashtbl.find ids_to_terms xpath with _ -> raise Exit)
             | None -> assert false) (* "ERROR: No current term!!!" *)
         selections
 
@@ -132,9 +131,7 @@ class sequent_viewer obj =
           else
             match current_infos with
             | Some (_,_,ids_to_hypotheses) ->
-                (try
-                  Hashtbl.find ids_to_hypotheses xpath
-                with _ -> raise Skip)
+                (try Hashtbl.find ids_to_hypotheses xpath with _ -> raise Exit)
             | None -> assert false) (* "ERROR: No current term!!!" *)
         selections
   
@@ -151,19 +148,12 @@ class sequent_viewer obj =
     self#load_root ~root:mathml#get_documentElement
  end
 
-
-class sequents_viewer ~(notebook:GPack.notebook)
-  ~(sequent_viewer:sequent_viewer) ()
+class sequentsViewer ~(notebook:GPack.notebook)
+  ~(sequentViewer:sequentViewer) ()
 =
-  let tab_label metano =
-    (GMisc.label ~text:(sprintf "?%d" metano) ~show:true ())#coerce
-  in
-  let set_goal goal =
-    let currentProof = MatitaProof.instance () in
-    assert (currentProof#onGoing ());
-    currentProof#proof#set_goal goal
-  in
   object (self)
+    inherit scriptAccessor
+
     val mutable pages = 0
     val mutable switch_page_callback = None
     val mutable page2goal = []  (* associative list: page no -> goal no *)
@@ -171,14 +161,17 @@ class sequents_viewer ~(notebook:GPack.notebook)
     val mutable goal2win = []   (* associative list: goal no -> scrolled win *)
     val mutable _metasenv = []
     val mutable scrolledWin: GBin.scrolled_window option = None
-      (* scrolled window to which the sequent_viewer is currently attached *)
+      (* scrolled window to which the sequentViewer is currently attached *)
+
+    method private tab_label metano =
+      (GMisc.label ~text:(sprintf "?%d" metano) ~show:true ())#coerce
 
     method reset =
       (match scrolledWin with
       | Some w ->
           (* removing page from the notebook will destroy all contained widget,
-          * we do not want the sequent_viewer to be destroyed as well *)
-          w#remove sequent_viewer#coerce;
+          * we do not want the sequentViewer to be destroyed as well *)
+          w#remove sequentViewer#coerce;
           scrolledWin <- None
       | None -> ());
       for i = 1 to pages do notebook#remove_page 0 done;
@@ -187,16 +180,19 @@ class sequents_viewer ~(notebook:GPack.notebook)
       goal2page <- [];
       goal2win <- [];
       _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 metasenv =
+    method load_sequents (status: ProofEngineTypes.status) =
+      let ((_, metasenv, _, _), goal) = status in
       let sequents_no = List.length metasenv in
       _metasenv <- metasenv;
       pages <- sequents_no;
+      self#script#setGoal goal;
       let win metano =
         let w =
           GBin.scrolled_window ~hpolicy:`AUTOMATIC ~vpolicy:`AUTOMATIC
@@ -204,9 +200,9 @@ class sequents_viewer ~(notebook:GPack.notebook)
         in
         let reparent () =
           scrolledWin <- Some w;
-          match sequent_viewer#misc#parent with
-          | None -> w#add sequent_viewer#coerce
-          | Some _ -> sequent_viewer#misc#reparent w#coerce
+          match sequentViewer#misc#parent with
+          | None -> w#add sequentViewer#coerce
+          | Some _ -> sequentViewer#misc#reparent w#coerce
         in
         goal2win <- (metano, reparent) :: goal2win;
         w#coerce
@@ -217,7 +213,7 @@ class sequents_viewer ~(notebook:GPack.notebook)
           page2goal <- (!page, metano) :: page2goal;
           goal2page <- (metano, !page) :: goal2page;
           incr page;
-          notebook#append_page ~tab_label:(tab_label metano) (win metano))
+          notebook#append_page ~tab_label:(self#tab_label metano) (win metano))
         metasenv;
       switch_page_callback <-
         Some (notebook#connect#switch_page ~callback:(fun page ->
@@ -226,14 +222,14 @@ class sequents_viewer ~(notebook:GPack.notebook)
               List.assoc page page2goal
             with Not_found -> assert false
           in
-          set_goal goal;
+          self#script#setGoal goal;
           self#render_page ~page ~goal))
 
     method private render_page ~page ~goal =
-      sequent_viewer#load_sequent _metasenv goal;
+      sequentViewer#load_sequent _metasenv goal;
       try
         List.assoc goal goal2win ();
-        sequent_viewer#set_selection None
+        sequentViewer#set_selection None
       with Not_found -> assert false
 
     method goto_sequent goal =
@@ -261,28 +257,67 @@ type 'widget constructor =
   unit ->
     'widget
 
-let sequent_viewer ?hadjustment ?vadjustment ?font_size ?log_verbosity =
+let sequentViewer ?hadjustment ?vadjustment ?font_size ?log_verbosity =
   GtkBase.Widget.size_params
     ~cont:(OgtkMathViewProps.pack_return (fun p ->
       OgtkMathViewProps.set_params
-        (new sequent_viewer (GtkMathViewProps.MathView_GMetaDOM.create p))
+        (new sequentViewer (GtkMathViewProps.MathView_GMetaDOM.create p))
         ~font_size ~log_verbosity))
     []
 
 let blank_uri = BuildTimeConf.blank_uri
 let current_proof_uri = BuildTimeConf.current_proof_uri
 
+type term_source =
+  [ `Ast of DisambiguateTypes.term
+  | `Cic of Cic.term * Cic.metasenv
+  | `String of string
+  ]
+
 exception Browser_failure of string
 
 let cicBrowsers = ref []
 
-class cicBrowser ~(history:string MatitaMisc.history) () =
+class type cicBrowser =
+object
+  method load: MatitaTypes.mathViewer_entry -> unit
+  (* method loadList: string list -> MatitaTypes.mathViewer_entry-> unit *)
+  method loadInput: string -> unit
+end
+
+class cicBrowser_impl ~(history:MatitaTypes.mathViewer_entry MatitaMisc.history)
+  ()
+=
   let term_RE = Pcre.regexp "^term:(.*)" in
+  let whelp_RE = Pcre.regexp "^\\s*whelp" 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 gui = MatitaGui.instance () in
   let win = 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 =
+    let q' = String.lowercase q in
+    let rec aux i = function
+      | [] -> failwith ("Whelp query '" ^ q ^ "' not found")
+      | h::_ when String.lowercase h = q' -> i
+      | _::tl -> aux (i+1) tl
+    in
+    combo#set_active (aux 0 queries);
+    win#queryInputText#set_text input
+  in
+  let set_whelp_query txt =
+    let query, arg = 
+      try
+        let q = Pcre.extract ~rex:whelp_query_RE txt in
+        q.(1), q.(2)
+      with Invalid_argument _ -> failwith "Malformed Whelp query"
+    in
+    activate_combo_query arg query
+  in
   let toplevel = win#toplevel in
-  let mathView = sequent_viewer ~packing:win#scrolledBrowser#add () 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 ());
@@ -295,11 +330,38 @@ class cicBrowser ~(history:string MatitaMisc.history) () =
   in
   let handle_error' f = fun () -> handle_error f in  (* used in callbacks *)
   object (self)
+    inherit scriptAccessor
+    
+    (* Whelp bar queries *)
+
     initializer
+      activate_combo_query "" "locate";
+      win#comboVbox#add (combo :> GObj.widget);
+      let start_query () = 
+        let query = String.lowercase (List.nth queries combo#active) in
+        let input = win#queryInputText#text in
+        let statement = "whelp " ^ query ^ " " ^ input ^ "." in
+        (MatitaScript.instance ())#advance ~statement ()
+      in
+      ignore(win#queryInputText#connect#activate ~callback:start_query);
+      ignore(combo#connect#changed ~callback:start_query);
+      win#whelpImage2#set_file "icons/whelp.png";
+      win#whelpBarToggleButton#set_active false;   
+      win#whelpBarBox#misc#hide ();
+      win#mathOrListNotebook#set_show_tabs false;
+      MatitaGtkMisc.connect_toggle_button win#whelpBarToggleButton 
+        (fun () -> 
+          if win#whelpBarToggleButton#active then
+            win#whelpBarBox#misc#show ()
+          else
+            win#whelpBarBox#misc#hide ());
+
+      win#browserForwardButton#misc#set_sensitive false;
+      win#browserBackButton#misc#set_sensitive false;
       ignore (win#browserUri#connect#activate (handle_error' (fun () ->
-        self#_loadUri win#browserUri#text)));
+        self#loadInput win#browserUri#text)));
       ignore (win#browserHomeButton#connect#clicked (handle_error' (fun () ->
-        self#_loadUri current_proof_uri)));
+        self#_load (`About `Current_proof))));
       ignore (win#browserRefreshButton#connect#clicked
         (handle_error' self#refresh));
       ignore (win#browserBackButton#connect#clicked (handle_error' self#back));
@@ -313,104 +375,146 @@ class cicBrowser ~(history:string MatitaMisc.history) () =
         then
           GMain.quit ();
         false));
+      ignore(win#whelpResultTreeview#connect#row_activated 
+        ~callback:(fun _ _ ->
+          let selection = self#_getWhelpResultTreeviewSelection () in
+          let txt = 
+            if String.sub selection 0 5 = "cic:/" then
+              selection
+            else
+              win#browserUri#text ^ selection 
+          in
+          self#loadInput txt));
       mathView#set_href_callback (Some (fun uri ->
-        handle_error (fun () -> self#_loadUri uri)));
-      self#_loadUri ~add_to_history:false blank_uri;
-      toplevel#show ();
-
-    val disambiguator = MatitaDisambiguator.instance ()
-    val currentProof = MatitaProof.instance ()
+        handle_error (fun () -> self#_load (`Uri uri))));
+      self#_load (`About `Blank);
+      toplevel#show ()
 
-    val mutable current_uri = ""
+    val mutable current_entry = `About `Blank 
     val mutable current_infos = None
     val mutable current_mathml = None
 
+    val model = new MatitaGtkMisc.stringListModel win#whelpResultTreeview
+
+    method private _getWhelpResultTreeviewSelection () =
+      match model#easy_selection () with
+          | [u] -> u
+          | _ -> assert false
+
+    (** history RATIONALE 
+     *
+     * all operations about history are done using _historyFoo
+     *
+     * only toplevel function like load loadInput can call
+     * _historyAdd
+     *)
+          
+    method private _historyAdd item = 
+      history#add item;
+      win#browserBackButton#misc#set_sensitive true;
+      win#browserForwardButton#misc#set_sensitive false
+
+    method private _historyPrev () =
+      let item = history#previous in
+      if history#is_begin then win#browserBackButton#misc#set_sensitive false;
+      win#browserForwardButton#misc#set_sensitive true;
+      item
+    
+    method private _historyNext () =
+      let item = history#next in
+      if history#is_end then win#browserForwardButton#misc#set_sensitive false;
+      win#browserBackButton#misc#set_sensitive true;
+      item
+
+    (** notebook RATIONALE 
+     * 
+     * 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 back () =
       try
-        self#_loadUri ~add_to_history:false history#previous
+        self#_load (self#_historyPrev ())
       with MatitaMisc.History_failure -> ()
 
     method private forward () =
       try
-        self#_loadUri ~add_to_history:false history#next
+        self#_load (self#_historyNext ())
       with MatitaMisc.History_failure -> ()
 
       (* loads a uri which can be a cic uri or an about:* uri
       * @param uri string *)
-    method private _loadUri ?(add_to_history = true) uri =
+    method private _load entry =
       try
-        if current_uri <> uri || uri = current_proof_uri then begin
-          (match uri with
-          | uri when uri = blank_uri -> self#blank ()
-          | uri when uri = current_proof_uri -> self#home ()
-          | uri when Pcre.pmatch ~rex:term_RE uri ->
-              self#loadTerm (`String (Pcre.extract ~rex:term_RE uri).(1))
-          | uri when Pcre.pmatch ~rex:trailing_slash_RE uri -> self#loadDir uri
-          | _ -> self#loadUriManagerUri (UriManager.uri_of_string uri));
-          self#setUri uri;
-          if add_to_history then history#add uri
-        end
+          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 (UriManager.uri_of_string uri)
+            | `Whelp (query, results) -> 
+                set_whelp_query query;
+                self#_loadList results);
+            self#setEntry entry
+          end
       with
-      | UriManager.IllFormedUri _ -> fail (sprintf "invalid uri: %s" uri)
-      | CicEnvironment.Object_not_found _ ->
-          fail (sprintf "object not found: %s" uri)
+      | 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
 
-    method loadUri uri =
-      handle_error (fun () -> self#_loadUri ~add_to_history:true uri)
-
     method private blank () =
+      self#_showMath;
       mathView#load_root (MatitaMisc.empty_mathml ())#get_documentElement
 
+    method private _loadCheck term =
+      failwith "not implemented _loadCheck";
+      self#_showMath
+
     method private home () =
-      if currentProof#onGoing () then
-        self#loadObj (cicCurrentProof currentProof#proof#proof)
-      else
-        raise (Browser_failure "no on going proof")
+      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 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 obj = Cic.CurrentProof (name, metasenv, bo, ty, [], []) in
+          self#_loadObj obj
+      | _ -> self#blank ()
 
       (** loads a cic uri from the environment
       * @param uri UriManager.uri *)
-    method private loadUriManagerUri uri =
+    method private _loadUriManagerUri uri =
       let uri = UriManager.strip_xpointer uri in
       let (obj, _) = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
-      self#loadObj obj
-
-    method private loadDir dir =
-      let mathml = MatitaMisc.empty_boxml () in
+      self#_loadObj obj
+      
+    method private _loadDir dir = 
       let content = Http_getter.ls dir in
-      let root = mathml#get_documentElement in
-      let new_box_elt name =
-        mathml#createElementNS ~namespaceURI:(Some Misc.boxml_ns)
-          ~qualifiedName:(Gdome.domString ("b:" ^ name))
+      let l = List.map (function 
+        | Http_getter_types.Ls_section sec -> sec            
+        | Http_getter_types.Ls_object obj -> obj.Http_getter_types.uri
+        ) content
       in
-      let new_text content = mathml#createTextNode (Gdome.domString content) in
-      let b_v = new_box_elt "v" in
-      List.iter
-        (fun item ->
-          let b_text = new_box_elt "text" in
-          let uri, elt =
-            match item with
-            | Http_getter_types.Ls_section subdir ->
-                (dir ^ subdir ^ "/"), (new_text (subdir ^ "/"))
-            | Http_getter_types.Ls_object obj ->
-                (dir ^ obj.Http_getter_types.uri),
-                (new_text obj.Http_getter_types.uri)
-          in
-          b_text#setAttributeNS ~namespaceURI:(Some Misc.xlink_ns)
-            ~qualifiedName:(Gdome.domString "xlink:href")
-            ~value:(Gdome.domString uri);
-          ignore (b_v#appendChild ~newChild:(b_text :> Gdome.node));
-          ignore (b_text#appendChild ~newChild:(elt :> Gdome.node)))
-        content;
-      ignore (root#appendChild ~newChild:(b_v :> Gdome.node));
-(*       Misc.domImpl#saveDocumentToFile ~doc:mathml ~name:"pippo" (); *)
-      mathView#load_root ~root:root
-
-    method private setUri uri =
-        win#browserUri#set_text uri;
-        current_uri <- uri
-
-    method private loadObj obj =
+      self#_loadList l
+
+    method private setEntry entry =
+      win#browserUri#set_text (string_of_entry entry);
+      current_entry <- entry
+
+    method private _loadObj obj =
+      self#_showMath; 
+      (* this must be _before_ loading the document, since 
+       * 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,_,_))) =
@@ -418,94 +522,131 @@ class cicBrowser ~(history:string MatitaMisc.history) () =
       in
       current_infos <- Some (ids_to_terms, ids_to_father_ids,
         ids_to_conjectures, ids_to_hypotheses);
-      match current_mathml with
+      (match current_mathml with
       | Some current_mathml when use_diff ->
           mathView#freeze;
           XmlDiff.update_dom ~from:current_mathml mathml;
           mathView#thaw
       |  _ ->
           mathView#load_root ~root:mathml#get_documentElement;
-          current_mathml <- Some mathml
-
-    method private _loadTerm s =
-      self#_loadTermAst (disambiguator#parserr#parseTerm (Stream.of_string s))
+          current_mathml <- Some mathml);
 
-    method private _loadTermAst ast =
-      let (_, _, term, _) =
-        MatitaCicMisc.disambiguate ~disambiguator ~currentProof ast
-      in
-      self#_loadTermCic term
-
-    method private _loadTermCic term =
-      let (context, metasenv) =
-        MatitaCicMisc.get_context_and_metasenv currentProof
-      in
+    method private _loadTermCic term metasenv =
+      let context = self#script#proofContext in
       let dummyno = CicMkImplicit.new_meta metasenv [] in
       let sequent = (dummyno, context, term) in
-      mathView#load_sequent (sequent :: metasenv) dummyno
-
-    method loadTerm (src:MatitaTypes.term_source) =
-      handle_error (fun () ->
-        (match src with
-        | `Ast ast -> self#_loadTermAst ast
-        | `Cic cic -> self#_loadTermCic cic
-        | `String s -> self#_loadTerm s);
-        self#setUri "check")
-
+      mathView#load_sequent (sequent :: metasenv) dummyno;
+      self#_showMath
+
+    method private _loadList l =
+      model#list_store#clear ();
+      List.iter model#easy_append l;
+      self#_showList
+    
+    (** { public methods, all must call _load!! } *)
+      
+    method load uri =
+      handle_error (fun () -> self#_load uri);
+      self#_historyAdd uri
+
+    (**  this is what the browser does when you enter a string an hit enter *)
+    method loadInput txt = 
+      let add_terminating_slash s =
+        if not(Pcre.pmatch ~rex:trailing_slash_RE s) && 
+           not(Pcre.pmatch ~rex:has_xpointer_RE s) then s^"/" else s
+      in
+      let is_uri txt = 
+        try 
+          let u = UriManager.strip_xpointer (UriManager.uri_of_string txt) in
+          ignore(Http_getter.resolve' u); true
+        with
+        | Http_getter_types.Key_not_found _ 
+        | Http_getter_types.Unresolvable_URI _ -> false
+        | UriManager.IllFormedUri u -> failwith ("Malformed URI '" ^ u ^ "'")
+      in
+      let is_whelp txt = Pcre.pmatch ~rex:whelp_RE txt in
+      if is_whelp txt then
+        begin
+          set_whelp_query txt;  
+          
+            
+          (MatitaScript.instance ())#advance ~statement:(txt^".") ()
+        end
+      else
+        begin
+          let entry = 
+            if is_uri txt then
+              (`Uri txt)
+            else
+              (`Dir (add_terminating_slash txt))
+          in
+          self#_load entry;
+          self#_historyAdd entry
+        end
+      
+        
       (** {2 methods used by constructor only} *)
 
     method win = win
     method history = history
-    method currentUri = current_uri
+    method currentEntry = current_entry
     method refresh () =
-      if current_uri = current_proof_uri then
-      self#_loadUri ~add_to_history:false current_proof_uri
-
+      if current_entry = `About `Current_proof then
+      self#_load (`About `Current_proof) 
   end
 
-let sequents_viewer ~(notebook:GPack.notebook)
-  ~(sequent_viewer:sequent_viewer) ()
+  
+let sequentsViewer ~(notebook:GPack.notebook)
+  ~(sequentViewer:sequentViewer) ()
 =
-  new sequents_viewer ~notebook ~sequent_viewer ()
+  new sequentsViewer ~notebook ~sequentViewer ()
 
 let cicBrowser () =
   let size = BuildTimeConf.browser_history_size in
   let rec aux history =
-    let browser = new cicBrowser ~history () in
+    let browser = new cicBrowser_impl ~history () in
     let win = browser#win in
     ignore (win#browserNewButton#connect#clicked (fun () ->
       let history =
-        new MatitaMisc.browser_history ~memento:history#save size ""
+        new MatitaMisc.browser_history ~memento:history#save size
+          (`About `Blank)
       in
       let newBrowser = aux history in
-      newBrowser#loadUri browser#currentUri));
+      newBrowser#load browser#currentEntry));
 (*
       (* attempt (failed) to close windows on CTRL-W ... *)
     MatitaGtkMisc.connect_key win#browserWinEventBox#event ~modifiers:[`CONTROL]
       GdkKeysyms._W (fun () -> win#toplevel#destroy ());
 *)
     cicBrowsers := browser :: !cicBrowsers;
-    (browser :> MatitaTypes.cicBrowser)
+    (browser :> cicBrowser)
   in
-  let history = new MatitaMisc.browser_history size blank_uri in
+  let history = new MatitaMisc.browser_history size (`About `Blank) in
   aux history
 
 let refresh_all_browsers () = List.iter (fun b -> b#refresh ()) !cicBrowsers
 
-class mathViewer =
-  object
-    method checkTerm (src:MatitaTypes.term_source) =
-      (cicBrowser ())#loadTerm src
-  end
-
-let mathViewer () = new mathViewer
-
-let default_sequent_viewer () = sequent_viewer ~show:true ()
-let sequent_viewer_instance = MatitaMisc.singleton default_sequent_viewer
+let default_sequentViewer () = sequentViewer ~show:true ()
+let sequentViewer_instance = MatitaMisc.singleton default_sequentViewer
 
-let default_sequents_viewer () =
+let default_sequentsViewer () =
   let gui = MatitaGui.instance () in
-  let sequent_viewer = sequent_viewer_instance () in
-  sequents_viewer ~notebook:gui#main#sequentsNotebook ~sequent_viewer ()
-let sequents_viewer_instance = MatitaMisc.singleton default_sequents_viewer
+  let sequentViewer = sequentViewer_instance () in
+  sequentsViewer ~notebook:gui#main#sequentsNotebook ~sequentViewer ()
+let sequentsViewer_instance = MatitaMisc.singleton default_sequentsViewer
 
+let mathViewer () = 
+  object(self)
+    method private get_browser reuse = 
+      if reuse then
+        (match !cicBrowsers with
+        | [] -> cicBrowser ()
+        | b :: _ -> (b :> cicBrowser))
+      else
+        (cicBrowser ())
+          
+    method show_entry ?(reuse=false) t = (self#get_browser reuse)#load t
+      
+    method show_uri_list ?(reuse=false) ~entry l =
+      (self#get_browser reuse)#load entry
+  end