helm/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 open Printf
  27
  28 open MatitaTypes
  29
  30 let add_trailing_slash =
  31   let rex = Pcre.regexp "/$" in
  32   fun s ->
  33     if Pcre.pmatch ~rex s then s
  34     else s ^ "/"
  35
  36 let strip_blanks =
  37   let rex = Pcre.regexp "^\\s*([^\\s]*)\\s*$" in
  38   fun s ->
  39     (Pcre.extract ~rex s).(1)
  40
  41 (** inherit from this class if you want to access current script *)
  42 class scriptAccessor =
  43 object (self)
  44   method private script = MatitaScript.instance ()
  45 end
  46
  47 let cicBrowsers = ref []
  48
  49 let default_font_size () =
  50   Helm_registry.get_opt_default Helm_registry.int
  51     ~default:BuildTimeConf.default_font_size "matita.font_size"
  52 let current_font_size = ref ~-1
  53 let increase_font_size () = incr current_font_size
  54 let decrease_font_size () = decr current_font_size
  55 let reset_font_size () = current_font_size := default_font_size ()
  56
  57   (* is there any lablgtk2 constant corresponding to the left mouse button??? *)
  58 let left_button = 1
  59
  60 let near (x1, y1) (x2, y2) =
  61   let distance = sqrt (((x2 -. x1) ** 2.) +. ((y2 -. y1) ** 2.)) in
  62   (distance < 4.)
  63
  64 let href_ds = Gdome.domString "href"
  65 let xref_ds = Gdome.domString "xref"
  66
  67
  68 class clickableMathView obj =
  69   let text_width = 80 in
  70   object (self)
  71     inherit GMathViewAux.multi_selection_math_view obj
  72
  73     val mutable href_callback: (string -> unit) option = None
  74     method set_href_callback f = href_callback <- f
  75
  76     val mutable _cic_info = None
  77     method private set_cic_info info = _cic_info <- info
  78     method private cic_info =
  79       match _cic_info with
  80       | Some info -> info
  81       | None -> assert false
  82
  83     initializer
  84       self#set_font_size !current_font_size;
  85       ignore (self#connect#selection_changed self#choose_selection);
  86       ignore (self#event#connect#button_press self#button_press);
  87       ignore (self#event#connect#button_release self#button_release);
  88 (*       ignore (self#connect#click (fun (gdome_elt, _, _, _) ->
  89         match gdome_elt with
  90         | Some elt  |+ element is an hyperlink, use href_callback on it +|
  91           when elt#hasAttributeNS ~namespaceURI:DomMisc.xlink_ns ~localName:href ->
  92             (match href_callback with
  93             | None -> ()
  94             | Some f ->
  95                 let uri =
  96                   elt#getAttributeNS ~namespaceURI:DomMisc.xlink_ns ~localName:href
  97                 in
  98                 f (uri#to_string))
  99         | Some elt -> ignore (self#action_toggle elt)
 100         | None -> ())) *)
 101
 102     val mutable button_press_x = -1.
 103     val mutable button_press_y = -1.
 104     val mutable selection_changed = false
 105
 106     method private button_press gdk_button =
 107       if GdkEvent.Button.button gdk_button = left_button then begin
 108         button_press_x <- GdkEvent.Button.x gdk_button;
 109         button_press_y <- GdkEvent.Button.y gdk_button;
 110         selection_changed <- false
 111       end;
 112       false
 113
 114     method private button_release gdk_button =
 115       if GdkEvent.Button.button gdk_button = left_button then begin
 116         let button_release_x = GdkEvent.Button.x gdk_button in
 117         let button_release_y = GdkEvent.Button.y gdk_button in
 118         (if near (button_press_x, button_press_y)
 119           (button_release_x, button_release_y)
 120           && not selection_changed
 121         then
 122           let x = int_of_float button_press_x in
 123           let y = int_of_float button_press_y in
 124           (match self#get_element_at x y with
 125           | None -> ()
 126           | Some elt ->
 127               let namespaceURI = DomMisc.xlink_ns in
 128               let localName = href_ds in
 129               if elt#hasAttributeNS ~namespaceURI ~localName then
 130                 self#invoke_href_callback
 131                   (elt#getAttributeNS ~namespaceURI ~localName)#to_string
 132                   gdk_button
 133               else
 134                 ignore (self#action_toggle elt)));
 135       end;
 136       false
 137
 138     method private invoke_href_callback href_value gdk_button =
 139       let button = GdkEvent.Button.button gdk_button in
 140       if button = left_button then
 141         let time = GdkEvent.Button.time gdk_button in
 142         match href_callback with
 143         | None -> ()
 144         | Some f ->
 145             (match MatitaMisc.split href_value with
 146             | [ uri ] ->  f uri
 147             | uris ->
 148                 let menu = GMenu.menu () in
 149                 List.iter
 150                   (fun uri ->
 151                     let menu_item =
 152                       GMenu.menu_item ~label:uri ~packing:menu#append ()
 153                     in
 154                     ignore (menu_item#connect#activate (fun () -> f uri)))
 155                   uris;
 156                 menu#popup ~button ~time)
 157
 158     method private choose_selection gdome_elt =
 159       let rec aux elt =
 160         if (elt#getAttributeNS ~namespaceURI:DomMisc.helm_ns
 161               ~localName:xref_ds)#to_string <> ""
 162 (*         if elt#hasAttributeNS ~namespaceURI:DomMisc.helm_ns ~localName:xref_ds
 163           && (elt#getAttributeNS ~namespaceURI:DomMisc.helm_ns
 164               ~localName:xref_ds)#to_string <> "" *)
 165         then
 166           self#set_selection (Some elt)
 167         else
 168           try
 169             (match elt#get_parentNode with
 170             | None -> assert false
 171             | Some p -> aux (new Gdome.element_of_node p))
 172           with GdomeInit.DOMCastException _ -> ()
 173 (*             debug_print "trying to select above the document root" *)
 174       in
 175       (match gdome_elt with
 176       | Some elt -> aux elt
 177       | None   -> self#set_selection None);
 178       selection_changed <- true
 179
 180     method update_font_size =
 181       self#set_font_size !current_font_size
 182
 183     method private get_term_by_id context id =
 184       let ids_to_terms, ids_to_hypotheses = self#cic_info in
 185       try
 186         `Term (Hashtbl.find ids_to_terms id)
 187       with Not_found ->
 188         try
 189           let hyp = Hashtbl.find ids_to_hypotheses id in
 190           let context' = MatitaMisc.list_tl_at hyp context in
 191           `Hyp context'
 192         with Not_found -> assert false
 193
 194     method string_of_selected_terms =
 195       let get_id (node: Gdome.element) =
 196         let xref_attr =
 197           node#getAttributeNS ~namespaceURI:DomMisc.helm_ns ~localName:xref_ds
 198         in
 199         xref_attr#to_string
 200       in
 201       let script = MatitaScript.instance () in
 202       let metasenv = script#proofMetasenv in
 203       let context = script#proofContext in
 204       let conclusion = script#proofConclusion in
 205       let cic_terms =
 206         List.map
 207           (fun node -> self#get_term_by_id context (get_id node))
 208           self#get_selections
 209       in
 210 (* TODO: code for patterns
 211       let conclusion = (MatitaScript.instance ())#proofConclusion in
 212       let conclusion_pattern =
 213         ProofEngineHelpers.pattern_of ~term:conclusion cic_terms
 214       in
 215 *)
 216       let dummy_goal = ~-1 in
 217       let cic_sequent =
 218         match cic_terms with
 219         | [] -> assert false
 220         | `Term t :: _ ->
 221             let context' =
 222               ProofEngineHelpers.locate_in_conjecture t
 223                 (dummy_goal, context, conclusion)
 224             in
 225             dummy_goal, context', t
 226         | `Hyp context :: _ -> dummy_goal, context, Cic.Rel 1
 227       in
 228 (* TODO: code for patterns
 229       (* TODO context shouldn't be empty *)
 230       let cic_sequent = ~-1, [], conclusion_pattern in
 231 *)
 232       let acic_sequent, _, _, ids_to_inner_sorts, _ =
 233         Cic2acic.asequent_of_sequent metasenv cic_sequent
 234       in
 235       let _, _, _, annterm = acic_sequent in
 236       let ast, ids_to_uris =
 237         CicNotationRew.ast_of_acic ids_to_inner_sorts annterm
 238       in
 239       let pped_ast = CicNotationRew.pp_ast ast in
 240       let markup = CicNotationPres.render ids_to_uris pped_ast in
 241       BoxPp.render_to_string text_width markup
 242
 243   end
 244
 245 let clickableMathView ?hadjustment ?vadjustment ?font_size ?log_verbosity =
 246   GtkBase.Widget.size_params
 247     ~cont:(OgtkMathViewProps.pack_return (fun p ->
 248       OgtkMathViewProps.set_params
 249         (new clickableMathView (GtkMathViewProps.MathView_GMetaDOM.create p))
 250         ~font_size:None ~log_verbosity:None))
 251     []
 252
 253 class sequentViewer obj =
 254 object (self)
 255   inherit clickableMathView obj
 256
 257   method load_sequent metasenv metano =
 258     let sequent = CicUtil.lookup_meta metano metasenv in
 259     let (mathml, (_, (ids_to_terms, _, ids_to_hypotheses,_ ))) =
 260       ApplyTransformation.mml_of_cic_sequent metasenv sequent
 261     in
 262     self#set_cic_info (Some (ids_to_terms, ids_to_hypotheses));
 263     let name = "sequent_viewer.xml" in
 264     prerr_endline ("load_sequent: dumping MathML to ./" ^ name);
 265     ignore (DomMisc.domImpl#saveDocumentToFile ~name ~doc:mathml ());
 266     self#load_root ~root:mathml#get_documentElement
 267  end
 268
 269 class sequentsViewer ~(notebook:GPack.notebook)
 270   ~(sequentViewer:sequentViewer) ()
 271 =
 272   object (self)
 273     inherit scriptAccessor
 274
 275     val mutable pages = 0
 276     val mutable switch_page_callback = None
 277     val mutable page2goal = []  (* associative list: page no -> goal no *)
 278     val mutable goal2page = []  (* the other way round *)
 279     val mutable goal2win = []   (* associative list: goal no -> scrolled win *)
 280     val mutable _metasenv = []
 281     val mutable scrolledWin: GBin.scrolled_window option = None
 282       (* scrolled window to which the sequentViewer is currently attached *)
 283
 284     method private tab_label metano =
 285       (GMisc.label ~text:(sprintf "?%d" metano) ~show:true ())#coerce
 286
 287     method reset =
 288       (match scrolledWin with
 289       | Some w ->
 290           (* removing page from the notebook will destroy all contained widget,
 291           * we do not want the sequentViewer to be destroyed as well *)
 292           w#remove sequentViewer#coerce;
 293           scrolledWin <- None
 294       | None -> ());
 295       for i = 1 to pages do notebook#remove_page 0 done;
 296       pages <- 0;
 297       page2goal <- [];
 298       goal2page <- [];
 299       goal2win <- [];
 300       _metasenv <- [];
 301       self#script#setGoal ~-1;
 302       (match switch_page_callback with
 303       | Some id ->
 304           GtkSignal.disconnect notebook#as_widget id;
 305           switch_page_callback <- None
 306       | None -> ())
 307
 308     method load_sequents (status: ProofEngineTypes.status) =
 309       let ((_, metasenv, _, _), goal) = status in
 310       let sequents_no = List.length metasenv in
 311       _metasenv <- metasenv;
 312       pages <- sequents_no;
 313       self#script#setGoal goal;
 314       let parentref = ref None in
 315       let win metano =
 316         let w =
 317           GBin.scrolled_window ~hpolicy:`AUTOMATIC ~vpolicy:`AUTOMATIC
 318             ~shadow_type:`IN ~show:true ()
 319         in
 320         let reparent () =
 321           scrolledWin <- Some w;
 322           match sequentViewer#misc#parent with
 323           | None -> w#add sequentViewer#coerce; parentref := Some w
 324           | Some parent ->
 325              let parent =
 326               match !parentref with None -> assert false | Some p -> p in
 327              parent#remove sequentViewer#coerce;
 328              w#add sequentViewer#coerce;
 329              parentref := Some w;
 330         in
 331         goal2win <- (metano, reparent) :: goal2win;
 332         w#coerce
 333       in
 334       let page = ref 0 in
 335       List.iter
 336         (fun (metano, _, _) ->
 337           page2goal <- (!page, metano) :: page2goal;
 338           goal2page <- (metano, !page) :: goal2page;
 339           incr page;
 340           notebook#append_page ~tab_label:(self#tab_label metano) (win metano))
 341         metasenv;
 342       switch_page_callback <-
 343         Some (notebook#connect#switch_page ~callback:(fun page ->
 344           let goal =
 345             try
 346               List.assoc page page2goal
 347             with Not_found -> assert false
 348           in
 349           self#script#setGoal goal;
 350           self#render_page ~page ~goal))
 351
 352     method private render_page ~page ~goal =
 353       sequentViewer#load_sequent _metasenv goal;
 354       try
 355         List.assoc goal goal2win ();
 356         sequentViewer#set_selection None
 357       with Not_found -> assert false
 358
 359     method goto_sequent goal =
 360       let page =
 361         try
 362           List.assoc goal goal2page
 363         with Not_found -> assert false
 364       in
 365       notebook#goto_page page;
 366       self#render_page page goal
 367
 368   end
 369
 370  (** constructors *)
 371
 372 type 'widget constructor =
 373   ?hadjustment:GData.adjustment ->
 374   ?vadjustment:GData.adjustment ->
 375   ?font_size:int ->
 376   ?log_verbosity:int ->
 377   ?width:int ->
 378   ?height:int ->
 379   ?packing:(GObj.widget -> unit) ->
 380   ?show:bool ->
 381   unit ->
 382     'widget
 383
 384 let sequentViewer ?hadjustment ?vadjustment ?font_size ?log_verbosity =
 385   GtkBase.Widget.size_params
 386     ~cont:(OgtkMathViewProps.pack_return (fun p ->
 387       OgtkMathViewProps.set_params
 388         (new sequentViewer (GtkMathViewProps.MathView_GMetaDOM.create p))
 389         ~font_size ~log_verbosity))
 390     []
 391
 392 let blank_uri = BuildTimeConf.blank_uri
 393 let current_proof_uri = BuildTimeConf.current_proof_uri
 394
 395 type term_source =
 396   [ `Ast of DisambiguateTypes.term
 397   | `Cic of Cic.term * Cic.metasenv
 398   | `String of string
 399   ]
 400
 401 class type cicBrowser =
 402 object
 403   method load: MatitaTypes.mathViewer_entry -> unit
 404   (* method loadList: string list -> MatitaTypes.mathViewer_entry-> unit *)
 405   method loadInput: string -> unit
 406 end
 407
 408 let reloadable = function
 409   | `About `Current_proof
 410   | `Dir _ ->
 411       true
 412   | _ -> false
 413
 414 class cicBrowser_impl ~(history:MatitaTypes.mathViewer_entry MatitaMisc.history)
 415   ()
 416 =
 417   let term_RE = Pcre.regexp "^term:(.*)" in
 418   let whelp_RE = Pcre.regexp "^\\s*whelp" in
 419   let uri_RE =
 420     Pcre.regexp
 421       "^cic:/([^/]+/)*[^/]+\\.(con|ind|var)(#xpointer\\(\\d+(/\\d+)+\\))?$"
 422   in
 423   let dir_RE = Pcre.regexp "^cic:((/([^/]+/)*[^/]+(/)?)|/|)$" in
 424   let whelp_query_RE = Pcre.regexp "^\\s*whelp\\s+([^\\s]+)\\s+(.*)$" in
 425   let trailing_slash_RE = Pcre.regexp "/$" in
 426   let has_xpointer_RE = Pcre.regexp "#xpointer\\(\\d+/\\d+(/\\d+)?\\)$" in
 427   let is_whelp txt = Pcre.pmatch ~rex:whelp_RE txt in
 428   let is_uri txt = Pcre.pmatch ~rex:uri_RE txt in
 429   let is_dir txt = Pcre.pmatch ~rex:dir_RE txt in
 430   let gui = MatitaGui.instance () in
 431   let win = gui#newBrowserWin () in
 432   let queries = ["Locate";"Hint";"Match";"Elim";"Instance"] in
 433   let combo,_ = GEdit.combo_box_text ~strings:queries () in
 434   let activate_combo_query input q =
 435     let q' = String.lowercase q in
 436     let rec aux i = function
 437       | [] -> failwith ("Whelp query '" ^ q ^ "' not found")
 438       | h::_ when String.lowercase h = q' -> i
 439       | _::tl -> aux (i+1) tl
 440     in
 441     combo#set_active (aux 0 queries);
 442     win#queryInputText#set_text input
 443   in
 444   let set_whelp_query txt =
 445     let query, arg =
 446       try
 447         let q = Pcre.extract ~rex:whelp_query_RE txt in
 448         q.(1), q.(2)
 449       with Invalid_argument _ -> failwith "Malformed Whelp query"
 450     in
 451     activate_combo_query arg query
 452   in
 453   let toplevel = win#toplevel in
 454   let mathView = sequentViewer ~packing:win#scrolledBrowser#add () in
 455   let fail message =
 456     MatitaGtkMisc.report_error ~title:"Cic browser" ~message
 457       ~parent:toplevel ()
 458   in
 459   let tags =
 460     [ "dir", GdkPixbuf.from_file (MatitaMisc.image_path "matita-folder.png");
 461       "obj", GdkPixbuf.from_file (MatitaMisc.image_path "matita-object.png") ]
 462   in
 463   let handle_error f =
 464     try
 465       f ()
 466     with exn -> fail (MatitaExcPp.to_string exn)
 467   in
 468   let handle_error' f = (fun () -> handle_error (fun () -> f ())) in
 469   object (self)
 470     inherit scriptAccessor
 471
 472     (* Whelp bar queries *)
 473
 474     initializer
 475       activate_combo_query "" "locate";
 476       win#whelpBarComboVbox#add combo#coerce;
 477       let start_query () =
 478         let query = String.lowercase (List.nth queries combo#active) in
 479         let input = win#queryInputText#text in
 480         let statement = "whelp " ^ query ^ " " ^ input ^ "." in
 481         (MatitaScript.instance ())#advance ~statement ()
 482       in
 483       ignore(win#queryInputText#connect#activate ~callback:start_query);
 484       ignore(combo#connect#changed ~callback:start_query);
 485       win#whelpBarImage#set_file (MatitaMisc.image_path "whelp.png");
 486       win#mathOrListNotebook#set_show_tabs false;
 487
 488       win#browserForwardButton#misc#set_sensitive false;
 489       win#browserBackButton#misc#set_sensitive false;
 490       ignore (win#browserUri#entry#connect#activate (handle_error' (fun () ->
 491         self#loadInput win#browserUri#entry#text)));
 492       ignore (win#browserHomeButton#connect#clicked (handle_error' (fun () ->
 493         self#load (`About `Current_proof))));
 494       ignore (win#browserRefreshButton#connect#clicked
 495         (handle_error' self#refresh));
 496       ignore (win#browserBackButton#connect#clicked (handle_error' self#back));
 497       ignore (win#browserForwardButton#connect#clicked
 498         (handle_error' self#forward));
 499       ignore (win#toplevel#event#connect#delete (fun _ ->
 500         let my_id = Oo.id self in
 501         cicBrowsers := List.filter (fun b -> Oo.id b <> my_id) !cicBrowsers;
 502         if !cicBrowsers = [] &&
 503           Helm_registry.get "matita.mode" = "cicbrowser"
 504         then
 505           GMain.quit ();
 506         false));
 507       ignore(win#whelpResultTreeview#connect#row_activated
 508         ~callback:(fun _ _ ->
 509           handle_error (fun () -> self#loadInput (self#_getSelectedUri ()))));
 510       mathView#set_href_callback (Some (fun uri ->
 511         handle_error (fun () ->
 512           self#load (`Uri (UriManager.uri_of_string uri)))));
 513       self#_load (`About `Blank);
 514       toplevel#show ()
 515
 516     val mutable current_entry = `About `Blank
 517     val mutable current_infos = None
 518     val mutable current_mathml = None
 519
 520     val model =
 521       new MatitaGtkMisc.taggedStringListModel tags win#whelpResultTreeview
 522
 523     val mutable lastDir = ""  (* last loaded "directory" *)
 524
 525     method private _getSelectedUri () =
 526       match model#easy_selection () with
 527       | [sel] when is_uri sel -> sel  (* absolute URI selected *)
 528 (*       | [sel] -> win#browserUri#entry#text ^ sel  |+ relative URI selected +| *)
 529       | [sel] -> lastDir ^ sel
 530       | _ -> assert false
 531
 532     (** history RATIONALE
 533      *
 534      * All operations about history are done using _historyFoo.
 535      * Only toplevel functions (ATM load and loadInput) call _historyAdd.
 536      *)
 537
 538     method private _historyAdd item =
 539       history#add item;
 540       win#browserBackButton#misc#set_sensitive true;
 541       win#browserForwardButton#misc#set_sensitive false
 542
 543     method private _historyPrev () =
 544       let item = history#previous in
 545       if history#is_begin then win#browserBackButton#misc#set_sensitive false;
 546       win#browserForwardButton#misc#set_sensitive true;
 547       item
 548
 549     method private _historyNext () =
 550       let item = history#next in
 551       if history#is_end then win#browserForwardButton#misc#set_sensitive false;
 552       win#browserBackButton#misc#set_sensitive true;
 553       item
 554
 555     (** notebook RATIONALE
 556      *
 557      * Use only these functions to switch between the tabs
 558      *)
 559     method private _showList = win#mathOrListNotebook#goto_page 1
 560     method private _showMath = win#mathOrListNotebook#goto_page 0
 561
 562     method private back () =
 563       try
 564         self#_load (self#_historyPrev ())
 565       with MatitaMisc.History_failure -> ()
 566
 567     method private forward () =
 568       try
 569         self#_load (self#_historyNext ())
 570       with MatitaMisc.History_failure -> ()
 571
 572       (* loads a uri which can be a cic uri or an about:* uri
 573       * @param uri string *)
 574     method private _load entry =
 575       try
 576         if entry <> current_entry || reloadable entry then begin
 577           (match entry with
 578           | `About `Current_proof -> self#home ()
 579           | `About `Blank -> self#blank ()
 580           | `About `Us -> () (* TODO implement easter egg here :-] *)
 581           | `Check term -> self#_loadCheck term
 582           | `Cic (term, metasenv) -> self#_loadTermCic term metasenv
 583           | `Dir dir -> self#_loadDir dir
 584           | `Uri uri -> self#_loadUriManagerUri uri
 585           | `Whelp (query, results) ->
 586               set_whelp_query query;
 587               self#_loadList (List.map (fun r -> "obj",
 588                 UriManager.string_of_uri r) results));
 589           self#setEntry entry
 590         end
 591       with exn -> fail (MatitaExcPp.to_string exn)
 592
 593     method private blank () =
 594       self#_showMath;
 595       mathView#load_root (MatitaMisc.empty_mathml ())#get_documentElement
 596
 597     method private _loadCheck term =
 598       failwith "not implemented _loadCheck";
 599       self#_showMath
 600
 601     method private home () =
 602       self#_showMath;
 603       match self#script#status.proof_status with
 604       | Proof  (uri, metasenv, bo, ty) ->
 605           let name = UriManager.name_of_uri (MatitaMisc.unopt uri) in
 606           let obj = Cic.CurrentProof (name, metasenv, bo, ty, [], []) in
 607           self#_loadObj obj
 608       | Incomplete_proof ((uri, metasenv, bo, ty), _) ->
 609           let name = UriManager.name_of_uri (MatitaMisc.unopt uri) in
 610           let obj = Cic.CurrentProof (name, metasenv, bo, ty, [], []) in
 611           self#_loadObj obj
 612       | _ -> self#blank ()
 613
 614       (** loads a cic uri from the environment
 615       * @param uri UriManager.uri *)
 616     method private _loadUriManagerUri uri =
 617       let uri = UriManager.strip_xpointer uri in
 618       let (obj, _) = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
 619       self#_loadObj obj
 620
 621     method private _loadDir dir =
 622       let content = Http_getter.ls dir in
 623       let l =
 624         List.fast_sort
 625           Pervasives.compare
 626           (List.map
 627             (function
 628               | Http_getter_types.Ls_section s -> "dir", s
 629               | Http_getter_types.Ls_object o -> "obj", o.Http_getter_types.uri)
 630             content)
 631       in
 632       lastDir <- dir;
 633       self#_loadList l
 634
 635     method private setEntry entry =
 636       win#browserUri#entry#set_text (string_of_entry entry);
 637       current_entry <- entry
 638
 639     method private _loadObj obj =
 640       self#_showMath;
 641       (* this must be _before_ loading the document, since
 642        * if the widget is not mapped (hidden by the notebook)
 643        * the document is not rendered *)
 644       let use_diff = false in (* ZACK TODO use XmlDiff when re-rendering? *)
 645       let (mathml, (_,((ids_to_terms, ids_to_father_ids, ids_to_conjectures,
 646            ids_to_hypotheses, ids_to_inner_sorts, ids_to_inner_types) as info)))
 647       =
 648         ApplyTransformation.mml_of_cic_object obj
 649       in
 650       current_infos <- Some info;
 651       (match current_mathml with
 652       | Some current_mathml when use_diff ->
 653           mathView#freeze;
 654           XmlDiff.update_dom ~from:current_mathml mathml;
 655           mathView#thaw
 656       |  _ ->
 657           let name = "cic_browser.xml" in
 658           prerr_endline ("cic_browser: dumping MathML to ./" ^ name);
 659           ignore (DomMisc.domImpl#saveDocumentToFile ~name ~doc:mathml ());
 660           mathView#load_root ~root:mathml#get_documentElement;
 661           current_mathml <- Some mathml);
 662
 663     method private _loadTermCic term metasenv =
 664       let context = self#script#proofContext in
 665       let dummyno = CicMkImplicit.new_meta metasenv [] in
 666       let sequent = (dummyno, context, term) in
 667       mathView#load_sequent (sequent :: metasenv) dummyno;
 668       self#_showMath
 669
 670     method private _loadList l =
 671       model#list_store#clear ();
 672       List.iter (fun (tag, s) -> model#easy_append ~tag s) l;
 673       self#_showList
 674
 675     (** { public methods, all must call _load!! } *)
 676
 677     method load entry =
 678       handle_error (fun () -> self#_load entry; self#_historyAdd entry)
 679
 680     (**  this is what the browser does when you enter a string an hit enter *)
 681     method loadInput txt =
 682       let txt = strip_blanks txt in
 683       let fix_uri txt =
 684         UriManager.string_of_uri
 685           (UriManager.strip_xpointer (UriManager.uri_of_string txt))
 686       in
 687       if is_whelp txt then begin
 688         set_whelp_query txt;
 689         (MatitaScript.instance ())#advance ~statement:(txt ^ ".") ()
 690       end else begin
 691         let entry =
 692           match txt with
 693           | txt when is_uri txt -> `Uri (UriManager.uri_of_string (fix_uri txt))
 694           | txt when is_dir txt -> `Dir (add_trailing_slash txt)
 695           | txt ->
 696               (try
 697                 entry_of_string txt
 698               with Invalid_argument _ ->
 699                 command_error (sprintf "unsupported uri: %s" txt))
 700         in
 701         self#_load entry;
 702         self#_historyAdd entry
 703       end
 704
 705       (** {2 methods accessing underlying GtkMathView} *)
 706
 707     method updateFontSize = mathView#set_font_size !current_font_size
 708
 709       (** {2 methods used by constructor only} *)
 710
 711     method win = win
 712     method history = history
 713     method currentEntry = current_entry
 714     method refresh () =
 715       if reloadable current_entry then self#_load current_entry
 716
 717   end
 718
 719 let sequentsViewer ~(notebook:GPack.notebook)
 720   ~(sequentViewer:sequentViewer) ()
 721 =
 722   new sequentsViewer ~notebook ~sequentViewer ()
 723
 724 let cicBrowser () =
 725   let size = BuildTimeConf.browser_history_size in
 726   let rec aux history =
 727     let browser = new cicBrowser_impl ~history () in
 728     let win = browser#win in
 729     ignore (win#browserNewButton#connect#clicked (fun () ->
 730       let history =
 731         new MatitaMisc.browser_history ~memento:history#save size
 732           (`About `Blank)
 733       in
 734       let newBrowser = aux history in
 735       newBrowser#load browser#currentEntry));
 736 (*
 737       (* attempt (failed) to close windows on CTRL-W ... *)
 738     MatitaGtkMisc.connect_key win#browserWinEventBox#event ~modifiers:[`CONTROL]
 739       GdkKeysyms._W (fun () -> win#toplevel#destroy ());
 740 *)
 741     cicBrowsers := browser :: !cicBrowsers;
 742     (browser :> cicBrowser)
 743   in
 744   let history = new MatitaMisc.browser_history size (`About `Blank) in
 745   aux history
 746
 747 let default_sequentViewer () = sequentViewer ~show:true ()
 748 let sequentViewer_instance = MatitaMisc.singleton default_sequentViewer
 749
 750 let default_sequentsViewer () =
 751   let gui = MatitaGui.instance () in
 752   let sequentViewer = sequentViewer_instance () in
 753   sequentsViewer ~notebook:gui#main#sequentsNotebook ~sequentViewer ()
 754 let sequentsViewer_instance = MatitaMisc.singleton default_sequentsViewer
 755
 756 let mathViewer () =
 757   object(self)
 758     method private get_browser reuse =
 759       if reuse then
 760         (match !cicBrowsers with
 761         | [] -> cicBrowser ()
 762         | b :: _ -> (b :> cicBrowser))
 763       else
 764         (cicBrowser ())
 765
 766     method show_entry ?(reuse=false) t = (self#get_browser reuse)#load t
 767
 768     method show_uri_list ?(reuse=false) ~entry l =
 769       (self#get_browser reuse)#load entry
 770   end
 771
 772 let refresh_all_browsers () = List.iter (fun b -> b#refresh ()) !cicBrowsers
 773
 774 let update_font_sizes () =
 775   List.iter (fun b -> b#updateFontSize) !cicBrowsers;
 776   (sequentViewer_instance ())#update_font_size
 777