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 MatitaGtkMisc
  31 open CicMathView
  32
  33 module Stack = Continuationals.Stack
  34
  35 let cicBrowsers = ref []
  36
  37 let tab_label meta_markup =
  38   let rec aux =
  39     function
  40     | `Closed m -> sprintf "<s>%s</s>" (aux m)
  41     | `Current m -> sprintf "<b>%s</b>" (aux m)
  42     | `Shift (pos, m) -> sprintf "|<sub>%d</sub>: %s" pos (aux m)
  43     | `Meta n -> sprintf "?%d" n
  44   in
  45   let markup = aux meta_markup in
  46   (GMisc.label ~markup ~show:true ())#coerce
  47
  48 let goal_of_switch = function Stack.Open g | Stack.Closed g -> g
  49
  50 class sequentsViewer ~(notebook:GPack.notebook) ~(cicMathView:cicMathView) () =
  51   object (self)
  52     method cicMathView = cicMathView  (** clickableMathView accessor *)
  53
  54     val mutable pages = 0
  55     val mutable switch_page_callback = None
  56     val mutable page2goal = []  (* associative list: page no -> goal no *)
  57     val mutable goal2page = []  (* the other way round *)
  58     val mutable goal2win = []   (* associative list: goal no -> scrolled win *)
  59     val mutable _metasenv = [],[]
  60     val mutable scrolledWin: GBin.scrolled_window option = None
  61       (* scrolled window to which the sequentViewer is currently attached *)
  62     val logo = (GMisc.image
  63       ~file:(MatitaMisc.image_path "matita_medium.png") ()
  64       :> GObj.widget)
  65
  66     val logo_with_qed = (GMisc.image
  67       ~file:(MatitaMisc.image_path "matita_small.png") ()
  68       :> GObj.widget)
  69
  70     method load_logo =
  71      notebook#set_show_tabs false;
  72      ignore(notebook#append_page logo)
  73
  74     method load_logo_with_qed =
  75      notebook#set_show_tabs false;
  76      ignore(notebook#append_page logo_with_qed)
  77
  78     method reset =
  79       cicMathView#remove_selections;
  80       (match scrolledWin with
  81       | Some w ->
  82           (* removing page from the notebook will destroy all contained widget,
  83           * we do not want the cicMathView to be destroyed as well *)
  84           w#remove cicMathView#coerce;
  85           scrolledWin <- None
  86       | None -> ());
  87       (match switch_page_callback with
  88       | Some id ->
  89           GtkSignal.disconnect notebook#as_widget id;
  90           switch_page_callback <- None
  91       | None -> ());
  92       for _i = 0 to pages do notebook#remove_page 0 done;
  93       notebook#set_show_tabs true;
  94       pages <- 0;
  95       page2goal <- [];
  96       goal2page <- [];
  97       goal2win <- [];
  98       _metasenv <- [],[]
  99
 100     method nload_sequents : 'status. #GrafiteTypes.status as 'status -> unit
 101     = fun (status : #GrafiteTypes.status) ->
 102      let _,_,metasenv,subst,_ = status#obj in
 103       _metasenv <- metasenv,subst;
 104       pages <- 0;
 105       let win goal_switch =
 106         let w =
 107           GBin.scrolled_window ~hpolicy:`AUTOMATIC ~vpolicy:`ALWAYS
 108             ~shadow_type:`IN ~show:true () in
 109         let reparent () =
 110           scrolledWin <- Some w;
 111           (match cicMathView#misc#parent with
 112             | None -> ()
 113             | Some p ->
 114                let parent = GContainer.cast_container p in
 115                 parent#remove cicMathView#coerce);
 116           w#add cicMathView#coerce
 117         in
 118         goal2win <- (goal_switch, reparent) :: goal2win;
 119         w#coerce
 120       in
 121       assert (
 122         let stack_goals = Stack.open_goals status#stack in
 123         let proof_goals = List.map fst metasenv in
 124         if
 125           HExtlib.list_uniq (List.sort compare stack_goals)
 126           <> List.sort compare proof_goals
 127         then begin
 128           prerr_endline ("STACK GOALS = " ^ String.concat " " (List.map string_of_int stack_goals));
 129           prerr_endline ("PROOF GOALS = " ^ String.concat " " (List.map string_of_int proof_goals));
 130           false
 131         end
 132         else true
 133       );
 134       let render_switch =
 135         function Stack.Open i ->`Meta i | Stack.Closed i ->`Closed (`Meta i)
 136       in
 137       let page = ref 0 in
 138       let added_goals = ref [] in
 139         (* goals can be duplicated on the tack due to focus, but we should avoid
 140          * multiple labels in the user interface *)
 141       let add_tab markup goal_switch =
 142         let goal = Stack.goal_of_switch goal_switch in
 143         if not (List.mem goal !added_goals) then begin
 144           ignore(notebook#append_page
 145             ~tab_label:(tab_label markup) (win goal_switch));
 146           page2goal <- (!page, goal_switch) :: page2goal;
 147           goal2page <- (goal_switch, !page) :: goal2page;
 148           incr page;
 149           pages <- pages + 1;
 150           added_goals := goal :: !added_goals
 151         end
 152       in
 153       let add_switch _ _ (_, sw) = add_tab (render_switch sw) sw in
 154       Stack.iter  (** populate notebook with tabs *)
 155         ~env:(fun depth _tag (pos, sw) ->
 156           let markup =
 157             match depth, pos with
 158             | 0, 0 -> `Current (render_switch sw)
 159             | 0, _ -> `Shift (pos, `Current (render_switch sw))
 160             | 1, pos when Stack.head_tag status#stack = `BranchTag ->
 161                 `Shift (pos, render_switch sw)
 162             | _ -> render_switch sw
 163           in
 164           add_tab markup sw)
 165         ~cont:add_switch ~todo:add_switch
 166         status#stack;
 167       switch_page_callback <-
 168         Some (notebook#connect#switch_page ~callback:(fun page ->
 169           let goal_switch =
 170             try List.assoc page page2goal with Not_found -> assert false
 171           in
 172           self#render_page status ~page ~goal_switch))
 173
 174     method private render_page:
 175      'status. #ApplyTransformation.status as 'status -> page:int ->
 176        goal_switch:Stack.switch -> unit
 177      = fun status ~page:_ ~goal_switch ->
 178       (match goal_switch with
 179       | Stack.Open goal ->
 180          let menv,subst = _metasenv in
 181           cicMathView#nload_sequent status menv subst goal
 182       | Stack.Closed _goal ->
 183           let root = Lazy.force closed_goal_mathml in
 184           cicMathView#load_root ~root);
 185       (try
 186         cicMathView#set_selection None;
 187         List.assoc goal_switch goal2win ();
 188         (match cicMathView#misc#parent with
 189            None -> assert false
 190          | Some p ->
 191             (* The text widget dinamycally inserts the text in a separate
 192                thread. We need to wait for it to terminate before we can
 193                move the scrollbar to the end *)
 194             while Glib.Main.pending()do ignore(Glib.Main.iteration false); done;
 195             let w =
 196              new GBin.scrolled_window
 197               (Gobject.try_cast p#as_widget "GtkScrolledWindow") in
 198             (* The double change upper/lower is to trigger the emission of
 199                changed :-( *)
 200             w#hadjustment#set_value w#hadjustment#upper;
 201             w#hadjustment#set_value w#hadjustment#lower;
 202             w#vadjustment#set_value w#vadjustment#lower;
 203             w#vadjustment#set_value
 204              (w#vadjustment#upper -. w#vadjustment#page_size));
 205       with Not_found -> assert false)
 206
 207     method goto_sequent: 'status. #ApplyTransformation.status as 'status -> int -> unit
 208      = fun status goal ->
 209       let goal_switch, page =
 210         try
 211           List.find
 212             (function Stack.Open g, _ | Stack.Closed g, _ -> g = goal)
 213             goal2page
 214         with Not_found -> assert false
 215       in
 216       notebook#goto_page page;
 217       self#render_page status ~page ~goal_switch
 218   end
 219
 220 let blank_uri = BuildTimeConf.blank_uri
 221 let current_proof_uri = BuildTimeConf.current_proof_uri
 222
 223 type term_source =
 224   [ `Ast of NotationPt.term
 225   | `NCic of NCic.term * NCic.context * NCic.metasenv * NCic.substitution
 226   | `String of string
 227   ]
 228
 229 class cicBrowser_impl ~(history:MatitaTypes.mathViewer_entry MatitaMisc.history)
 230   ()
 231 =
 232   let uri_RE =
 233     Pcre.regexp
 234       "^cic:/([^/]+/)*[^/]+\\.(con|ind|var)(#xpointer\\(\\d+(/\\d+)+\\))?$"
 235   in
 236   let dir_RE = Pcre.regexp "^cic:((/([^/]+/)*[^/]+(/)?)|/|)$" in
 237   let is_uri txt = Pcre.pmatch ~rex:uri_RE txt in
 238   let is_dir txt = Pcre.pmatch ~rex:dir_RE txt in
 239   let _gui = MatitaMisc.get_gui () in
 240   let win = new MatitaGeneratedGui.browserWin () in
 241   let _ = win#browserUri#misc#grab_focus () in
 242   let gviz = LablGraphviz.graphviz ~packing:win#graphScrolledWin#add () in
 243   let searchText =
 244     GSourceView3.source_view ~auto_indent:false ~editable:false ()
 245   in
 246   let _ =
 247      win#scrolledwinContent#add (searchText :> GObj.widget);
 248      let callback () =
 249        let text = win#entrySearch#text in
 250        let highlight start end_ =
 251          searchText#source_buffer#move_mark `INSERT ~where:start;
 252          searchText#source_buffer#move_mark `SEL_BOUND ~where:end_;
 253          searchText#scroll_mark_onscreen `INSERT
 254        in
 255        let iter = searchText#source_buffer#get_iter `SEL_BOUND in
 256        match iter#forward_search text with
 257        | None ->
 258            (match searchText#source_buffer#start_iter#forward_search text with
 259            | None -> ()
 260            | Some (start,end_) -> highlight start end_)
 261        | Some (start,end_) -> highlight start end_
 262      in
 263      ignore(win#entrySearch#connect#activate ~callback);
 264      ignore(win#buttonSearch#connect#clicked ~callback);
 265   in
 266   let toplevel = win#toplevel in
 267   let mathView = cicMathView ~packing:win#scrolledBrowser#add () in
 268   let fail message =
 269     MatitaGtkMisc.report_error ~title:"Cic browser" ~message
 270       ~parent:toplevel ()
 271   in
 272   let tags =
 273     [ "dir", GdkPixbuf.from_file (MatitaMisc.image_path "matita-folder.png");
 274       "obj", GdkPixbuf.from_file (MatitaMisc.image_path "matita-object.png") ]
 275   in
 276   let b = (not (Helm_registry.get_bool "matita.debug")) in
 277   let handle_error f =
 278     try
 279       f ()
 280     with exn ->
 281       if b then
 282         fail (snd (MatitaExcPp.to_string exn))
 283       else raise exn
 284   in
 285   let handle_error' f = (fun () -> handle_error (fun () -> f ())) in
 286   let load_easter_egg = lazy (
 287     win#browserImage#set_file (MatitaMisc.image_path "meegg.png"))
 288   in
 289   let load_hints () =
 290       let module Pp = GraphvizPp.Dot in
 291       let filename, oc = Filename.open_temp_file "matita" ".dot" in
 292       let fmt = Format.formatter_of_out_channel oc in
 293       let status = (get_matita_script_current ())#status in
 294       Pp.header
 295         ~name:"Hints"
 296         ~graph_type:"graph"
 297         ~graph_attrs:["overlap", "false"]
 298         ~node_attrs:["fontsize", "9"; "width", ".4";
 299             "height", ".4"; "shape", "box"]
 300         ~edge_attrs:["fontsize", "10"; "len", "2"] fmt;
 301       NCicUnifHint.generate_dot_file status fmt;
 302       Pp.trailer fmt;
 303       Pp.raw "@." fmt;
 304       close_out oc;
 305       gviz#load_graph_from_file ~gviz_cmd:"neato -Tpng" filename;
 306       (*HExtlib.safe_remove filename*)
 307   in
 308   let load_coerchgraph tred () =
 309       let module Pp = GraphvizPp.Dot in
 310       let filename, oc = Filename.open_temp_file "matita" ".dot" in
 311       let fmt = Format.formatter_of_out_channel oc in
 312       Pp.header
 313         ~name:"Coercions"
 314         ~node_attrs:["fontsize", "9"; "width", ".4"; "height", ".4"]
 315         ~edge_attrs:["fontsize", "10"] fmt;
 316       let status = (get_matita_script_current ())#status in
 317       NCicCoercion.generate_dot_file status fmt;
 318       Pp.trailer fmt;
 319       Pp.raw "@." fmt;
 320       close_out oc;
 321       if tred then
 322         gviz#load_graph_from_file
 323           (* gvpack can no longer read the output of -Txdot :-( *)
 324           (*~gviz_cmd:"dot -Txdot | tred |gvpack -gv | dot" filename*)
 325           ~gviz_cmd:"dot -Txdot | tred | dot" filename
 326       else
 327         gviz#load_graph_from_file
 328           (* gvpack can no longer read the output of -Txdot :-( *)
 329           (*~gviz_cmd:"dot -Txdot | gvpack -gv | dot" filename;*)
 330           ~gviz_cmd:"dot -Txdot | dot" filename;
 331       HExtlib.safe_remove filename
 332   in
 333   object (self)
 334     val mutable gviz_uri =
 335       let uri = NUri.uri_of_string "cic:/dummy/dec.con" in
 336       NReference.reference_of_spec uri NReference.Decl;
 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        (* MATITA 1.0 let fmt = Format.formatter_of_out_channel oc in
 488        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           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