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