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