]> matita.cs.unibo.it Git - helm.git/blob - matita/matita/matitaMathView.ml
some advances on reduction
[helm.git] / matita / matita / matitaMathView.ml
1 (* Copyright (C) 2004-2005, HELM Team.
2  * 
3  * This file is part of HELM, an Hypertextual, Electronic
4  * Library of Mathematics, developed at the Computer Science
5  * Department, University of Bologna, Italy.
6  * 
7  * HELM is free software; you can redistribute it and/or
8  * modify it under the terms of the GNU General Public License
9  * as published by the Free Software Foundation; either version 2
10  * of the License, or (at your option) any later version.
11  * 
12  * HELM is distributed in the hope that it will be useful,
13  * but WITHOUT ANY WARRANTY; without even the implied warranty of
14  * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
15  * GNU General Public License for more details.
16  *
17  * You should have received a copy of the GNU General Public License
18  * along with HELM; if not, write to the Free Software
19  * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
20  * MA  02111-1307, USA.
21  * 
22  * For details, see the HELM World-Wide-Web page,
23  * http://cs.unibo.it/helm/.
24  *)
25
26 (* $Id$ *)
27
28 open Printf
29
30 open GrafiteTypes
31 open MatitaGtkMisc
32 open MatitaGuiTypes
33 open CicMathView
34
35 module Stack = Continuationals.Stack
36
37 let cicBrowsers = ref []
38
39 let tab_label meta_markup =
40   let rec aux =
41     function
42     | `Closed m -> sprintf "<s>%s</s>" (aux m)
43     | `Current m -> sprintf "<b>%s</b>" (aux m)
44     | `Shift (pos, m) -> sprintf "|<sub>%d</sub>: %s" pos (aux m)
45     | `Meta n -> sprintf "?%d" n
46   in
47   let markup = aux meta_markup in
48   (GMisc.label ~markup ~show:true ())#coerce
49
50 let goal_of_switch = function Stack.Open g | Stack.Closed g -> g
51
52 class sequentsViewer ~(notebook:GPack.notebook) ~(cicMathView:cicMathView) () =
53   object (self)
54     method cicMathView = cicMathView  (** clickableMathView accessor *)
55
56     val mutable pages = 0
57     val mutable switch_page_callback = None
58     val mutable page2goal = []  (* associative list: page no -> goal no *)
59     val mutable goal2page = []  (* the other way round *)
60     val mutable goal2win = []   (* associative list: goal no -> scrolled win *)
61     val mutable _metasenv = [],[]
62     val mutable scrolledWin: GBin.scrolled_window option = None
63       (* scrolled window to which the sequentViewer is currently attached *)
64     val logo = (GMisc.image
65       ~file:(MatitaMisc.image_path "matita_medium.png") ()
66       :> GObj.widget)
67             
68     val logo_with_qed = (GMisc.image
69       ~file:(MatitaMisc.image_path "matita_small.png") ()
70       :> GObj.widget)
71
72     method load_logo =
73      notebook#set_show_tabs false;
74      ignore(notebook#append_page logo)
75
76     method load_logo_with_qed =
77      notebook#set_show_tabs false;
78      ignore(notebook#append_page logo_with_qed)
79
80     method reset =
81       cicMathView#remove_selections;
82       (match scrolledWin with
83       | Some w ->
84           (* removing page from the notebook will destroy all contained widget,
85           * we do not want the cicMathView to be destroyed as well *)
86           w#remove cicMathView#coerce;
87           scrolledWin <- None
88       | None -> ());
89       (match switch_page_callback with
90       | Some id ->
91           GtkSignal.disconnect notebook#as_widget id;
92           switch_page_callback <- None
93       | None -> ());
94       for i = 0 to pages do notebook#remove_page 0 done; 
95       notebook#set_show_tabs true;
96       pages <- 0;
97       page2goal <- [];
98       goal2page <- [];
99       goal2win <- [];
100       _metasenv <- [],[]
101
102     method nload_sequents : 'status. #GrafiteTypes.status as 'status -> unit
103     = fun (status : #GrafiteTypes.status) ->
104      let _,_,metasenv,subst,_ = status#obj in
105       _metasenv <- metasenv,subst;
106       pages <- 0;
107       let win goal_switch =
108         let w =
109           GBin.scrolled_window ~hpolicy:`AUTOMATIC ~vpolicy:`ALWAYS
110             ~shadow_type:`IN ~show:true () in
111         let reparent () =
112           scrolledWin <- Some w;
113           (match cicMathView#misc#parent with
114             | None -> ()
115             | Some parent ->
116                let parent =
117                 match cicMathView#misc#parent with
118                    None -> assert false
119                  | Some p -> GContainer.cast_container p
120                in
121                 parent#remove cicMathView#coerce);
122           w#add cicMathView#coerce
123         in
124         goal2win <- (goal_switch, reparent) :: goal2win;
125         w#coerce
126       in
127       assert (
128         let stack_goals = Stack.open_goals status#stack in
129         let proof_goals = List.map fst metasenv in
130         if
131           HExtlib.list_uniq (List.sort Pervasives.compare stack_goals)
132           <> List.sort Pervasives.compare proof_goals
133         then begin
134           prerr_endline ("STACK GOALS = " ^ String.concat " " (List.map string_of_int stack_goals));
135           prerr_endline ("PROOF GOALS = " ^ String.concat " " (List.map string_of_int proof_goals));
136           false
137         end
138         else true
139       );
140       let render_switch =
141         function Stack.Open i ->`Meta i | Stack.Closed i ->`Closed (`Meta i)
142       in
143       let page = ref 0 in
144       let added_goals = ref [] in
145         (* goals can be duplicated on the tack due to focus, but we should avoid
146          * multiple labels in the user interface *)
147       let add_tab markup goal_switch =
148         let goal = Stack.goal_of_switch goal_switch in
149         if not (List.mem goal !added_goals) then begin
150           ignore(notebook#append_page 
151             ~tab_label:(tab_label markup) (win goal_switch));
152           page2goal <- (!page, goal_switch) :: page2goal;
153           goal2page <- (goal_switch, !page) :: goal2page;
154           incr page;
155           pages <- pages + 1;
156           added_goals := goal :: !added_goals
157         end
158       in
159       let add_switch _ _ (_, sw) = add_tab (render_switch sw) sw in
160       Stack.iter  (** populate notebook with tabs *)
161         ~env:(fun depth tag (pos, sw) ->
162           let markup =
163             match depth, pos with
164             | 0, 0 -> `Current (render_switch sw)
165             | 0, _ -> `Shift (pos, `Current (render_switch sw))
166             | 1, pos when Stack.head_tag status#stack = `BranchTag ->
167                 `Shift (pos, render_switch sw)
168             | _ -> render_switch sw
169           in
170           add_tab markup sw)
171         ~cont:add_switch ~todo:add_switch
172         status#stack;
173       switch_page_callback <-
174         Some (notebook#connect#switch_page ~callback:(fun page ->
175           let goal_switch =
176             try List.assoc page page2goal with Not_found -> assert false
177           in
178           self#render_page status ~page ~goal_switch))
179
180     method private render_page:
181      'status. #ApplyTransformation.status as 'status -> page:int ->
182        goal_switch:Stack.switch -> unit
183      = fun status ~page ~goal_switch ->
184       (match goal_switch with
185       | Stack.Open goal ->
186          let menv,subst = _metasenv in
187           cicMathView#nload_sequent status menv subst goal
188       | Stack.Closed goal ->
189           let root = Lazy.force closed_goal_mathml in
190           cicMathView#load_root ~root);
191       (try
192         cicMathView#set_selection None;
193         List.assoc goal_switch goal2win ();
194         (match cicMathView#misc#parent with
195            None -> assert false
196          | Some p ->
197             (* The text widget dinamycally inserts the text in a separate
198                thread. We need to wait for it to terminate before we can
199                move the scrollbar to the end *)
200             while Glib.Main.pending()do ignore(Glib.Main.iteration false); done;
201             let w =
202              new GBin.scrolled_window
203               (Gobject.try_cast p#as_widget "GtkScrolledWindow") in
204             (* The double change upper/lower is to trigger the emission of
205                changed :-( *)
206             w#hadjustment#set_value w#hadjustment#upper;
207             w#hadjustment#set_value w#hadjustment#lower;
208             w#vadjustment#set_value w#vadjustment#lower;
209             w#vadjustment#set_value
210              (w#vadjustment#upper -. w#vadjustment#page_size));
211       with Not_found -> assert false)
212
213     method goto_sequent: 'status. #ApplyTransformation.status as 'status -> int -> unit
214      = fun status goal ->
215       let goal_switch, page =
216         try
217           List.find
218             (function Stack.Open g, _ | Stack.Closed g, _ -> g = goal)
219             goal2page
220         with Not_found -> assert false
221       in
222       notebook#goto_page page;
223       self#render_page status ~page ~goal_switch
224   end
225
226 let blank_uri = BuildTimeConf.blank_uri
227 let current_proof_uri = BuildTimeConf.current_proof_uri
228
229 type term_source =
230   [ `Ast of NotationPt.term
231   | `NCic of NCic.term * NCic.context * NCic.metasenv * NCic.substitution
232   | `String of string
233   ]
234
235 class cicBrowser_impl ~(history:MatitaTypes.mathViewer_entry MatitaMisc.history)
236   ()
237 =
238   let uri_RE =
239     Pcre.regexp
240       "^cic:/([^/]+/)*[^/]+\\.(con|ind|var)(#xpointer\\(\\d+(/\\d+)+\\))?$"
241   in
242   let dir_RE = Pcre.regexp "^cic:((/([^/]+/)*[^/]+(/)?)|/|)$" in
243   let is_uri txt = Pcre.pmatch ~rex:uri_RE txt in
244   let is_dir txt = Pcre.pmatch ~rex:dir_RE txt in
245   let gui = MatitaMisc.get_gui () in
246   let win = new MatitaGeneratedGui.browserWin () in
247   let _ = win#browserUri#misc#grab_focus () in
248   let gviz = LablGraphviz.graphviz ~packing:win#graphScrolledWin#add () in
249   let searchText = 
250     GSourceView2.source_view ~auto_indent:false ~editable:false ()
251   in
252   let _ =
253      win#scrolledwinContent#add (searchText :> GObj.widget);
254      let callback () = 
255        let text = win#entrySearch#text in
256        let highlight start end_ =
257          searchText#source_buffer#move_mark `INSERT ~where:start;
258          searchText#source_buffer#move_mark `SEL_BOUND ~where:end_;
259          searchText#scroll_mark_onscreen `INSERT
260        in
261        let iter = searchText#source_buffer#get_iter `SEL_BOUND in
262        match iter#forward_search text with
263        | None -> 
264            (match searchText#source_buffer#start_iter#forward_search text with
265            | None -> ()
266            | Some (start,end_) -> highlight start end_)
267        | Some (start,end_) -> highlight start end_
268      in
269      ignore(win#entrySearch#connect#activate ~callback);
270      ignore(win#buttonSearch#connect#clicked ~callback);
271   in
272   let toplevel = win#toplevel in
273   let mathView = cicMathView ~packing:win#scrolledBrowser#add () in
274   let fail message = 
275     MatitaGtkMisc.report_error ~title:"Cic browser" ~message 
276       ~parent:toplevel ()  
277   in
278   let tags =
279     [ "dir", GdkPixbuf.from_file (MatitaMisc.image_path "matita-folder.png");
280       "obj", GdkPixbuf.from_file (MatitaMisc.image_path "matita-object.png") ]
281   in
282   let b = (not (Helm_registry.get_bool "matita.debug")) in
283   let handle_error f =
284     try
285       f ()
286     with exn ->
287       if b then
288         fail (snd (MatitaExcPp.to_string exn))
289       else raise exn
290   in
291   let handle_error' f = (fun () -> handle_error (fun () -> f ())) in
292   let load_easter_egg = lazy (
293     win#browserImage#set_file (MatitaMisc.image_path "meegg.png"))
294   in
295   let load_hints () =
296       let module Pp = GraphvizPp.Dot in
297       let filename, oc = Filename.open_temp_file "matita" ".dot" in
298       let fmt = Format.formatter_of_out_channel oc in
299       let status = (get_matita_script_current ())#status in
300       Pp.header 
301         ~name:"Hints"
302         ~graph_type:"graph"
303         ~graph_attrs:["overlap", "false"]
304         ~node_attrs:["fontsize", "9"; "width", ".4"; 
305             "height", ".4"; "shape", "box"]
306         ~edge_attrs:["fontsize", "10"; "len", "2"] fmt;
307       NCicUnifHint.generate_dot_file status fmt;
308       Pp.trailer fmt;
309       Pp.raw "@." fmt;
310       close_out oc;
311       gviz#load_graph_from_file ~gviz_cmd:"neato -Tpng" filename;
312       (*HExtlib.safe_remove filename*)
313   in
314   let load_coerchgraph tred () = 
315       let module Pp = GraphvizPp.Dot in
316       let filename, oc = Filename.open_temp_file "matita" ".dot" in
317       let fmt = Format.formatter_of_out_channel oc in
318       Pp.header 
319         ~name:"Coercions"
320         ~node_attrs:["fontsize", "9"; "width", ".4"; "height", ".4"]
321         ~edge_attrs:["fontsize", "10"] fmt;
322       let status = (get_matita_script_current ())#status in
323       NCicCoercion.generate_dot_file status fmt;
324       Pp.trailer fmt;
325       Pp.raw "@." fmt;
326       close_out oc;
327       if tred then
328         gviz#load_graph_from_file 
329           ~gviz_cmd:"dot -Txdot | tred |gvpack -gv | dot" filename
330       else
331         gviz#load_graph_from_file 
332           ~gviz_cmd:"dot -Txdot | gvpack -gv | dot" filename;
333       HExtlib.safe_remove filename
334   in
335   object (self)
336     val mutable gviz_uri = NReference.reference_of_string "cic:/dummy.dec";
337
338     val dep_contextual_menu = GMenu.menu ()
339
340     initializer
341       win#mathOrListNotebook#set_show_tabs false;
342       win#browserForwardButton#misc#set_sensitive false;
343       win#browserBackButton#misc#set_sensitive false;
344       ignore (win#browserUri#connect#activate (handle_error' (fun () ->
345         self#loadInput win#browserUri#text)));
346       ignore (win#browserHomeButton#connect#clicked (handle_error' (fun () ->
347         self#load (`About `Current_proof))));
348       ignore (win#browserRefreshButton#connect#clicked
349         (handle_error' (self#refresh ~force:true)));
350       ignore (win#browserBackButton#connect#clicked (handle_error' self#back));
351       ignore (win#browserForwardButton#connect#clicked
352         (handle_error' self#forward));
353       ignore (win#toplevel#event#connect#delete (fun _ ->
354         let my_id = Oo.id self in
355         cicBrowsers := List.filter (fun b -> Oo.id b <> my_id) !cicBrowsers;
356         false));
357       ignore(win#whelpResultTreeview#connect#row_activated 
358         ~callback:(fun _ _ ->
359           handle_error (fun () -> self#loadInput (self#_getSelectedUri ()))));
360       mathView#set_href_callback (Some (fun uri ->
361         handle_error (fun () ->
362          let uri = `NRef (NReference.reference_of_string uri) in
363           self#load uri)));
364       gviz#connect_href (fun button_ev attrs ->
365         let time = GdkEvent.Button.time button_ev in
366         let uri = List.assoc "href" attrs in
367         gviz_uri <- NReference.reference_of_string uri;
368         match GdkEvent.Button.button button_ev with
369         | button when button = MatitaMisc.left_button -> self#load (`NRef gviz_uri)
370         | button when button = MatitaMisc.right_button ->
371             dep_contextual_menu#popup ~button ~time
372         | _ -> ());
373       connect_menu_item win#browserCloseMenuItem (fun () ->
374         let my_id = Oo.id self in
375         cicBrowsers := List.filter (fun b -> Oo.id b <> my_id) !cicBrowsers;
376         win#toplevel#misc#hide(); win#toplevel#destroy ());
377       connect_menu_item win#browserUrlMenuItem (fun () ->
378         win#browserUri#misc#grab_focus ());
379
380       self#_load (`About `Blank);
381       toplevel#show ()
382
383     val mutable current_entry = `About `Blank 
384
385       (** @return None if no object uri can be built from the current entry *)
386     method private currentCicUri =
387       match current_entry with
388       | `NRef uri -> Some uri
389       | _ -> None
390
391     val model =
392       new MatitaGtkMisc.taggedStringListModel tags win#whelpResultTreeview
393
394     val mutable lastDir = ""  (* last loaded "directory" *)
395
396     method mathView = mathView
397
398     method private _getSelectedUri () =
399       match model#easy_selection () with
400       | [sel] when is_uri sel -> sel  (* absolute URI selected *)
401 (*       | [sel] -> win#browserUri#entry#text ^ sel  |+ relative URI selected +| *)
402       | [sel] -> lastDir ^ sel
403       | _ -> assert false
404
405     (** history RATIONALE 
406      *
407      * All operations about history are done using _historyFoo.
408      * Only toplevel functions (ATM load and loadInput) call _historyAdd.
409      *)
410           
411     method private _historyAdd item = 
412       history#add item;
413       win#browserBackButton#misc#set_sensitive true;
414       win#browserForwardButton#misc#set_sensitive false
415
416     method private _historyPrev () =
417       let item = history#previous in
418       if history#is_begin then win#browserBackButton#misc#set_sensitive false;
419       win#browserForwardButton#misc#set_sensitive true;
420       item
421     
422     method private _historyNext () =
423       let item = history#next in
424       if history#is_end then win#browserForwardButton#misc#set_sensitive false;
425       win#browserBackButton#misc#set_sensitive true;
426       item
427
428     (** notebook RATIONALE 
429      * 
430      * Use only these functions to switch between the tabs
431      *)
432     method private _showMath = win#mathOrListNotebook#goto_page   0
433     method private _showList = win#mathOrListNotebook#goto_page   1
434     method private _showEgg  = win#mathOrListNotebook#goto_page   2
435     method private _showGviz = win#mathOrListNotebook#goto_page   3
436     method private _showSearch = win#mathOrListNotebook#goto_page 4
437
438     method private back () =
439       try
440         self#_load (self#_historyPrev ())
441       with MatitaMisc.History_failure -> ()
442
443     method private forward () =
444       try
445         self#_load (self#_historyNext ())
446       with MatitaMisc.History_failure -> ()
447
448       (* loads a uri which can be a cic uri or an about:* uri
449       * @param uri string *)
450     method private _load ?(force=false) entry =
451       handle_error (fun () ->
452        if entry <> current_entry || entry = `About `Current_proof || entry =
453          `About `Coercions || entry = `About `CoercionsFull || force then
454         begin
455           (match entry with
456           | `About `Current_proof -> self#home ()
457           | `About `Blank -> self#blank ()
458           | `About `Us -> self#egg ()
459           | `About `CoercionsFull -> self#coerchgraph false ()
460           | `About `Coercions -> self#coerchgraph true ()
461           | `About `Hints -> self#hints ()
462           | `About `TeX -> self#tex ()
463           | `About `Grammar -> self#grammar () 
464           | `Check term -> self#_loadCheck term
465           | `NCic (term, ctx, metasenv, subst) -> 
466                self#_loadTermNCic term metasenv subst ctx
467           | `Dir dir -> self#_loadDir dir
468           | `NRef nref -> self#_loadNReference nref);
469           self#setEntry entry
470         end)
471
472     method private blank () =
473       self#_showMath;
474       mathView#load_root (Lazy.force empty_mathml)
475
476     method private _loadCheck term =
477       failwith "not implemented _loadCheck";
478 (*       self#_showMath *)
479
480     method private egg () =
481       self#_showEgg;
482       Lazy.force load_easter_egg
483
484     method private redraw_gviz ?center_on () =
485       if Sys.command "which dot" = 0 then
486        let tmpfile, oc = Filename.open_temp_file "matita" ".dot" in
487        let fmt = Format.formatter_of_out_channel oc in
488        (* MATITA 1.0 MetadataDeps.DepGraph.render fmt gviz_graph;*)
489        close_out oc;
490        gviz#load_graph_from_file ~gviz_cmd:"tred | dot" tmpfile;
491        (match center_on with
492        | None -> ()
493        | Some uri -> gviz#center_on_href (NReference.string_of_reference uri));
494        HExtlib.safe_remove tmpfile
495       else
496        MatitaGtkMisc.report_error ~title:"graphviz error"
497         ~message:("Graphviz is not installed but is necessary to render "^
498          "the graph of dependencies amoung objects. Please install it.")
499         ~parent:win#toplevel ()
500
501     method private dependencies direction uri () =
502       assert false (* MATITA 1.0
503       let dbd = LibraryDb.instance () in
504       let graph =
505         match direction with
506         | `Fwd -> MetadataDeps.DepGraph.direct_deps ~dbd uri
507         | `Back -> MetadataDeps.DepGraph.inverse_deps ~dbd uri in
508       gviz_graph <- graph;  (** XXX check this for memory consuption *)
509       self#redraw_gviz ~center_on:uri ();
510       self#_showGviz *)
511
512     method private coerchgraph tred () =
513       load_coerchgraph tred ();
514       self#_showGviz
515
516     method private hints () =
517       load_hints ();
518       self#_showGviz
519
520     method private tex () =
521       let b = Buffer.create 1000 in
522       Printf.bprintf b "UTF-8 equivalence classes (rotate with ALT-L):\n\n";
523       List.iter 
524         (fun l ->
525            List.iter (fun sym ->
526              Printf.bprintf b "  %s" (Glib.Utf8.from_unichar sym) 
527            ) l;
528            Printf.bprintf b "\n";
529         )
530         (List.sort 
531           (fun l1 l2 -> compare (List.hd l1) (List.hd l2))
532           (Virtuals.get_all_eqclass ()));
533       Printf.bprintf b "\n\nVirtual keys (trigger with ALT-L):\n\n";
534       List.iter 
535         (fun tag, items -> 
536            Printf.bprintf b "  %s:\n" tag;
537            List.iter 
538              (fun names, symbol ->
539                 Printf.bprintf b "  \t%s\t%s\n" 
540                   (Glib.Utf8.from_unichar symbol)
541                   (String.concat ", " names))
542              (List.sort 
543                (fun (_,a) (_,b) -> compare a b)
544                items);
545            Printf.bprintf b "\n")
546         (List.sort 
547           (fun (a,_) (b,_) -> compare a b)
548           (Virtuals.get_all_virtuals ()));
549       self#_loadText (Buffer.contents b)
550
551     method private _loadText text =
552       searchText#source_buffer#set_text text;
553       win#entrySearch#misc#grab_focus ();
554       self#_showSearch
555
556     method private grammar () =
557       self#_loadText
558        (Print_grammar.ebnf_of_term (get_matita_script_current ())#status);
559
560     method private home () =
561       self#_showMath;
562       let status = (get_matita_script_current ())#status in
563        match status#ng_mode with
564           `ProofMode -> self#_loadNObj status status#obj
565         | _ -> self#blank ()
566
567     method private _loadNReference (NReference.Ref (uri,_)) =
568       let status = (get_matita_script_current ())#status in
569       let obj = NCicEnvironment.get_checked_obj status uri in
570       self#_loadNObj status obj
571
572     method private _loadDir dir = 
573       let content = Http_getter.ls ~local:false dir in
574       let l =
575         List.fast_sort
576           Pervasives.compare
577           (List.map
578             (function 
579               | Http_getter_types.Ls_section s -> "dir", s
580               | Http_getter_types.Ls_object o -> "obj", o.Http_getter_types.uri)
581             content)
582       in
583       lastDir <- dir;
584       self#_loadList l
585
586     method private setEntry entry =
587       win#browserUri#set_text (MatitaTypes.string_of_entry entry);
588       current_entry <- entry
589
590     method private _loadNObj status obj =
591       (* showMath must be done _before_ loading the document, since if the
592        * widget is not mapped (hidden by the notebook) the document is not
593        * rendered *)
594       self#_showMath;
595       mathView#load_nobject status obj
596
597     method private _loadTermNCic term m s c =
598       let d = 0 in
599       let m = (0,([],c,term))::m in
600       let status = (get_matita_script_current ())#status in
601       mathView#nload_sequent status m s d;
602       self#_showMath
603
604     method private _loadList l =
605       model#list_store#clear ();
606       List.iter (fun (tag, s) -> model#easy_append ~tag s) l;
607       self#_showList
608
609     (** { public methods, all must call _load!! } *)
610       
611     method load entry =
612       handle_error (fun () -> self#_load entry; self#_historyAdd entry)
613
614     (**  this is what the browser does when you enter a string an hit enter *)
615     method loadInput txt =
616       let txt = HExtlib.trim_blanks txt in
617       (* (* ZACK: what the heck? *)
618       let fix_uri txt =
619         UriManager.string_of_uri
620           (UriManager.strip_xpointer (UriManager.uri_of_string txt))
621       in
622       *)
623         let entry =
624           match txt with
625           | txt when is_uri txt ->
626               `NRef (NReference.reference_of_string ((*fix_uri*) txt))
627           | txt when is_dir txt -> `Dir (MatitaMisc.normalize_dir txt)
628           | txt ->
629              (try
630                MatitaTypes.entry_of_string txt
631               with Invalid_argument _ ->
632                raise
633                 (GrafiteTypes.Command_error(sprintf "unsupported uri: %s" txt)))
634         in
635         self#_load entry;
636         self#_historyAdd entry
637
638       (** {2 methods used by constructor only} *)
639
640     method win = win
641     method history = history
642     method currentEntry = current_entry
643     method refresh ~force () = self#_load ~force current_entry
644
645   end
646   
647 let sequentsViewer ~(notebook:GPack.notebook) ~(cicMathView:cicMathView) ():
648   MatitaGuiTypes.sequentsViewer
649 =
650   (new sequentsViewer ~notebook ~cicMathView ():> MatitaGuiTypes.sequentsViewer)
651
652 let new_cicBrowser () =
653   let size = BuildTimeConf.browser_history_size in
654   let rec aux history =
655     let browser = new cicBrowser_impl ~history () in
656     let win = browser#win in
657     ignore (win#browserNewButton#connect#clicked (fun () ->
658       let history =
659         new MatitaMisc.browser_history ~memento:history#save size
660           (`About `Blank)
661       in
662       let newBrowser = aux history in
663       newBrowser#load browser#currentEntry));
664 (*
665       (* attempt (failed) to close windows on CTRL-W ... *)
666     MatitaGtkMisc.connect_key win#browserWinEventBox#event ~modifiers:[`CONTROL]
667       GdkKeysyms._W (fun () -> win#toplevel#destroy ());
668 *)
669     cicBrowsers := browser :: !cicBrowsers;
670     browser
671   in
672   let history = new MatitaMisc.browser_history size (`About `Blank) in
673   aux history
674
675 (** @param reuse if set reused last opened cic browser otherwise 
676 *  opens a new one. default is false *)
677 let cicBrowser ?(reuse=false) t =
678  let browser =
679   if reuse then
680    (match !cicBrowsers with [] -> new_cicBrowser () | b :: _ -> b)
681   else
682    new_cicBrowser ()
683  in
684   match t with
685      None -> ()
686    | Some t -> browser#load t
687 ;;
688
689 let default_cicMathView () =
690  let res = cicMathView ~show:true () in
691   res#set_href_callback
692     (Some (fun uri ->
693       let uri = `NRef (NReference.reference_of_string uri) in
694        cicBrowser (Some uri)));
695   res
696
697 let cicMathView_instance =
698  MatitaMisc.singleton default_cicMathView
699
700 let default_sequentsViewer notebook =
701   let cicMathView = cicMathView_instance () in
702   sequentsViewer ~notebook ~cicMathView ()
703
704 let sequentsViewer_instance =
705  let already_used = ref false in
706   fun notebook ->
707    if !already_used then assert false
708    else
709     (already_used := true;
710      default_sequentsViewer notebook)
711
712 let refresh_all_browsers () =
713   List.iter (fun b -> b#refresh ~force:false ()) !cicBrowsers
714
715 let get_math_views () =
716   (cicMathView_instance ()) :: (List.map (fun b -> b#mathView) !cicBrowsers)
717
718 let find_selection_owner () =
719   let rec aux =
720     function
721     | [] -> raise Not_found
722     | mv :: tl ->
723         (match mv#get_selections with
724         | [] -> aux tl
725         | sel :: _ -> mv)
726   in
727   aux (get_math_views ())
728
729 let has_selection () =
730   try ignore (find_selection_owner ()); true
731   with Not_found -> false
732
733 let math_view_clipboard = ref None (* associative list target -> string *)
734 let has_clipboard () = !math_view_clipboard <> None
735 let empty_clipboard () = math_view_clipboard := None
736
737 let copy_selection () =
738   try
739     math_view_clipboard :=
740       Some ((find_selection_owner ())#strings_of_selection)
741   with Not_found -> failwith "no selection"
742
743 let paste_clipboard paste_kind =
744   match !math_view_clipboard with
745   | None -> failwith "empty clipboard"
746   | Some cb ->
747       (try List.assoc paste_kind cb with Not_found -> assert false)
748