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