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