]> matita.cs.unibo.it Git - helm.git/blob - helm/matita/matitaMathView.ml
Added a new section on the logical library.
[helm.git] / 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
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         TermAcicContent.ast_of_acic ids_to_inner_sorts annterm
332       in
333       let pped_ast = TermContentPres.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           HLog.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     HLog.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         HLog.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 CicNotationPt.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 (snd (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 (MatitaTypes.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                MatitaTypes.entry_of_string txt
897               with Invalid_argument _ ->
898                raise
899                 (GrafiteTypes.Command_error(sprintf "unsupported uri: %s" txt)))
900         in
901         self#_load entry;
902         self#_historyAdd entry
903       end
904
905       (** {2 methods accessing underlying GtkMathView} *)
906
907     method updateFontSize = mathView#set_font_size !current_font_size
908
909       (** {2 methods used by constructor only} *)
910
911     method win = win
912     method history = history
913     method currentEntry = current_entry
914     method refresh ~force () = self#_load ~force current_entry
915
916   end
917   
918 let sequentsViewer ~(notebook:GPack.notebook) ~(cicMathView:cicMathView) ():
919   MatitaGuiTypes.sequentsViewer
920 =
921   new sequentsViewer ~notebook ~cicMathView ()
922
923 let cicBrowser () =
924   let size = BuildTimeConf.browser_history_size in
925   let rec aux history =
926     let browser = new cicBrowser_impl ~history () in
927     let win = browser#win in
928     ignore (win#browserNewButton#connect#clicked (fun () ->
929       let history =
930         new MatitaMisc.browser_history ~memento:history#save size
931           (`About `Blank)
932       in
933       let newBrowser = aux history in
934       newBrowser#load browser#currentEntry));
935 (*
936       (* attempt (failed) to close windows on CTRL-W ... *)
937     MatitaGtkMisc.connect_key win#browserWinEventBox#event ~modifiers:[`CONTROL]
938       GdkKeysyms._W (fun () -> win#toplevel#destroy ());
939 *)
940     cicBrowsers := browser :: !cicBrowsers;
941     (browser :> MatitaGuiTypes.cicBrowser)
942   in
943   let history = new MatitaMisc.browser_history size (`About `Blank) in
944   aux history
945
946 let default_cicMathView () = cicMathView ~show:true ()
947 let cicMathView_instance = MatitaMisc.singleton default_cicMathView
948
949 let default_sequentsViewer () =
950   let gui = get_gui () in
951   let cicMathView = cicMathView_instance () in
952   sequentsViewer ~notebook:gui#main#sequentsNotebook ~cicMathView ()
953 let sequentsViewer_instance = MatitaMisc.singleton default_sequentsViewer
954
955 let mathViewer () = 
956   object(self)
957     method private get_browser reuse = 
958       if reuse then
959         (match !cicBrowsers with
960         | [] -> cicBrowser ()
961         | b :: _ -> (b :> MatitaGuiTypes.cicBrowser))
962       else
963         (cicBrowser ())
964           
965     method show_entry ?(reuse=false) t = (self#get_browser reuse)#load t
966       
967     method show_uri_list ?(reuse=false) ~entry l =
968       (self#get_browser reuse)#load entry
969   end
970
971 let refresh_all_browsers () =
972  List.iter (fun b -> b#refresh ~force:false ()) !cicBrowsers
973
974 let update_font_sizes () =
975   List.iter (fun b -> b#updateFontSize) !cicBrowsers;
976   (cicMathView_instance ())#update_font_size
977
978 let get_math_views () =
979   ((cicMathView_instance ()) :> MatitaGuiTypes.clickableMathView)
980   :: (List.map (fun b -> b#mathView) !cicBrowsers)
981
982 let get_selections () =
983   if (MatitaScript.current ())#onGoingProof () then
984     let rec aux =
985       function
986       | [] -> None
987       | mv :: tl ->
988           (match mv#string_of_selections with
989           | [] -> aux tl
990           | sels -> Some sels)
991     in
992     aux (get_math_views ())
993   else
994     None
995
996 let reset_selections () =
997   List.iter (fun mv -> mv#remove_selections) (get_math_views ())
998