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