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