1 (* Copyright (C) 2004-2005, HELM Team.
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.
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.
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.
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,
22 * For details, see the HELM World-Wide-Web page,
23 * http://cs.unibo.it/helm/.
33 module Stack = Continuationals.Stack
35 let cicBrowsers = ref []
37 let tab_label meta_markup =
40 | `Closed m -> sprintf "<s>%s</s>" (aux m)
41 | `Current m -> sprintf "<b>%s</b>" (aux m)
42 | `Shift (pos, m) -> sprintf "|<sub>%d</sub>: %s" pos (aux m)
43 | `Meta n -> sprintf "?%d" n
45 let markup = aux meta_markup in
46 (GMisc.label ~markup ~show:true ())#coerce
48 let goal_of_switch = function Stack.Open g | Stack.Closed g -> g
50 class sequentsViewer ~(notebook:GPack.notebook) ~(cicMathView:cicMathView) () =
52 method cicMathView = cicMathView (** clickableMathView accessor *)
55 val mutable switch_page_callback = None
56 val mutable page2goal = [] (* associative list: page no -> goal no *)
57 val mutable goal2page = [] (* the other way round *)
58 val mutable goal2win = [] (* associative list: goal no -> scrolled win *)
59 val mutable _metasenv = [],[]
60 val mutable scrolledWin: GBin.scrolled_window option = None
61 (* scrolled window to which the sequentViewer is currently attached *)
62 val logo = (GMisc.image
63 ~file:(MatitaMisc.image_path "matita_medium.png") ()
66 val logo_with_qed = (GMisc.image
67 ~file:(MatitaMisc.image_path "matita_small.png") ()
71 notebook#set_show_tabs false;
72 ignore(notebook#append_page logo)
74 method load_logo_with_qed =
75 notebook#set_show_tabs false;
76 ignore(notebook#append_page logo_with_qed)
79 cicMathView#remove_selections;
80 (match scrolledWin with
82 (* removing page from the notebook will destroy all contained widget,
83 * we do not want the cicMathView to be destroyed as well *)
84 w#remove cicMathView#coerce;
87 (match switch_page_callback with
89 GtkSignal.disconnect notebook#as_widget id;
90 switch_page_callback <- None
92 for _i = 0 to pages do notebook#remove_page 0 done;
93 notebook#set_show_tabs true;
100 method nload_sequents : 'status. #GrafiteTypes.status as 'status -> unit
101 = fun (status : #GrafiteTypes.status) ->
102 let _,_,metasenv,subst,_ = status#obj in
103 _metasenv <- metasenv,subst;
105 let win goal_switch =
107 GBin.scrolled_window ~hpolicy:`AUTOMATIC ~vpolicy:`ALWAYS
108 ~shadow_type:`IN ~show:true () in
110 scrolledWin <- Some w;
111 (match cicMathView#misc#parent with
114 let parent = GContainer.cast_container p in
115 parent#remove cicMathView#coerce);
116 w#add cicMathView#coerce
118 goal2win <- (goal_switch, reparent) :: goal2win;
122 let stack_goals = Stack.open_goals status#stack in
123 let proof_goals = List.map fst metasenv in
125 HExtlib.list_uniq (List.sort compare stack_goals)
126 <> List.sort compare proof_goals
128 prerr_endline ("STACK GOALS = " ^ String.concat " " (List.map string_of_int stack_goals));
129 prerr_endline ("PROOF GOALS = " ^ String.concat " " (List.map string_of_int proof_goals));
135 function Stack.Open i ->`Meta i | Stack.Closed i ->`Closed (`Meta i)
138 let added_goals = ref [] in
139 (* goals can be duplicated on the tack due to focus, but we should avoid
140 * multiple labels in the user interface *)
141 let add_tab markup goal_switch =
142 let goal = Stack.goal_of_switch goal_switch in
143 if not (List.mem goal !added_goals) then begin
144 ignore(notebook#append_page
145 ~tab_label:(tab_label markup) (win goal_switch));
146 page2goal <- (!page, goal_switch) :: page2goal;
147 goal2page <- (goal_switch, !page) :: goal2page;
150 added_goals := goal :: !added_goals
153 let add_switch _ _ (_, sw) = add_tab (render_switch sw) sw in
154 Stack.iter (** populate notebook with tabs *)
155 ~env:(fun depth _tag (pos, sw) ->
157 match depth, pos with
158 | 0, 0 -> `Current (render_switch sw)
159 | 0, _ -> `Shift (pos, `Current (render_switch sw))
160 | 1, pos when Stack.head_tag status#stack = `BranchTag ->
161 `Shift (pos, render_switch sw)
162 | _ -> render_switch sw
165 ~cont:add_switch ~todo:add_switch
167 switch_page_callback <-
168 Some (notebook#connect#switch_page ~callback:(fun page ->
170 try List.assoc page page2goal with Not_found -> assert false
172 self#render_page status ~page ~goal_switch))
174 method private render_page:
175 'status. #ApplyTransformation.status as 'status -> page:int ->
176 goal_switch:Stack.switch -> unit
177 = fun status ~page:_ ~goal_switch ->
178 (match goal_switch with
180 let menv,subst = _metasenv in
181 cicMathView#nload_sequent status menv subst goal
182 | Stack.Closed _goal ->
183 let root = Lazy.force closed_goal_mathml in
184 cicMathView#load_root ~root);
186 cicMathView#set_selection None;
187 List.assoc goal_switch goal2win ();
188 (match cicMathView#misc#parent with
191 (* The text widget dinamycally inserts the text in a separate
192 thread. We need to wait for it to terminate before we can
193 move the scrollbar to the end *)
194 while Glib.Main.pending()do ignore(Glib.Main.iteration false); done;
196 new GBin.scrolled_window
197 (Gobject.try_cast p#as_widget "GtkScrolledWindow") in
198 (* The double change upper/lower is to trigger the emission of
200 w#hadjustment#set_value w#hadjustment#upper;
201 w#hadjustment#set_value w#hadjustment#lower;
202 w#vadjustment#set_value w#vadjustment#lower;
203 w#vadjustment#set_value
204 (w#vadjustment#upper -. w#vadjustment#page_size));
205 with Not_found -> assert false)
207 method goto_sequent: 'status. #ApplyTransformation.status as 'status -> int -> unit
209 let goal_switch, page =
212 (function Stack.Open g, _ | Stack.Closed g, _ -> g = goal)
214 with Not_found -> assert false
216 notebook#goto_page page;
217 self#render_page status ~page ~goal_switch
220 let blank_uri = BuildTimeConf.blank_uri
221 let current_proof_uri = BuildTimeConf.current_proof_uri
224 [ `Ast of NotationPt.term
225 | `NCic of NCic.term * NCic.context * NCic.metasenv * NCic.substitution
229 class cicBrowser_impl ~(history:MatitaTypes.mathViewer_entry MatitaMisc.history)
234 "^cic:/([^/]+/)*[^/]+\\.(con|ind|var)(#xpointer\\(\\d+(/\\d+)+\\))?$"
236 let dir_RE = Pcre.regexp "^cic:((/([^/]+/)*[^/]+(/)?)|/|)$" in
237 let is_uri txt = Pcre.pmatch ~rex:uri_RE txt in
238 let is_dir txt = Pcre.pmatch ~rex:dir_RE txt in
239 let _gui = MatitaMisc.get_gui () in
240 let win = new MatitaGeneratedGui.browserWin () in
241 let _ = win#browserUri#misc#grab_focus () in
242 let gviz = LablGraphviz.graphviz ~packing:win#graphScrolledWin#add () in
244 GSourceView3.source_view ~auto_indent:false ~editable:false ()
247 win#scrolledwinContent#add (searchText :> GObj.widget);
249 let text = win#entrySearch#text in
250 let highlight start end_ =
251 searchText#source_buffer#move_mark `INSERT ~where:start;
252 searchText#source_buffer#move_mark `SEL_BOUND ~where:end_;
253 searchText#scroll_mark_onscreen `INSERT
255 let iter = searchText#source_buffer#get_iter `SEL_BOUND in
256 match iter#forward_search text with
258 (match searchText#source_buffer#start_iter#forward_search text with
260 | Some (start,end_) -> highlight start end_)
261 | Some (start,end_) -> highlight start end_
263 ignore(win#entrySearch#connect#activate ~callback);
264 ignore(win#buttonSearch#connect#clicked ~callback);
266 let toplevel = win#toplevel in
267 let mathView = cicMathView ~packing:win#scrolledBrowser#add () in
269 MatitaGtkMisc.report_error ~title:"Cic browser" ~message
273 [ "dir", GdkPixbuf.from_file (MatitaMisc.image_path "matita-folder.png");
274 "obj", GdkPixbuf.from_file (MatitaMisc.image_path "matita-object.png") ]
276 let b = (not (Helm_registry.get_bool "matita.debug")) in
282 fail (snd (MatitaExcPp.to_string exn))
285 let handle_error' f = (fun () -> handle_error (fun () -> f ())) in
286 let load_easter_egg = lazy (
287 win#browserImage#set_file (MatitaMisc.image_path "meegg.png"))
290 let module Pp = GraphvizPp.Dot in
291 let filename, oc = Filename.open_temp_file "matita" ".dot" in
292 let fmt = Format.formatter_of_out_channel oc in
293 let status = (get_matita_script_current ())#status in
297 ~graph_attrs:["overlap", "false"]
298 ~node_attrs:["fontsize", "9"; "width", ".4";
299 "height", ".4"; "shape", "box"]
300 ~edge_attrs:["fontsize", "10"; "len", "2"] fmt;
301 NCicUnifHint.generate_dot_file status fmt;
305 gviz#load_graph_from_file ~gviz_cmd:"neato -Tpng" filename;
306 (*HExtlib.safe_remove filename*)
308 let load_coerchgraph tred () =
309 let module Pp = GraphvizPp.Dot in
310 let filename, oc = Filename.open_temp_file "matita" ".dot" in
311 let fmt = Format.formatter_of_out_channel oc in
314 ~node_attrs:["fontsize", "9"; "width", ".4"; "height", ".4"]
315 ~edge_attrs:["fontsize", "10"] fmt;
316 let status = (get_matita_script_current ())#status in
317 NCicCoercion.generate_dot_file status fmt;
322 gviz#load_graph_from_file
323 (* gvpack can no longer read the output of -Txdot :-( *)
324 (*~gviz_cmd:"dot -Txdot | tred |gvpack -gv | dot" filename*)
325 ~gviz_cmd:"dot -Txdot | tred | dot" filename
327 gviz#load_graph_from_file
328 (* gvpack can no longer read the output of -Txdot :-( *)
329 (*~gviz_cmd:"dot -Txdot | gvpack -gv | dot" filename;*)
330 ~gviz_cmd:"dot -Txdot | dot" filename;
331 HExtlib.safe_remove filename
334 val mutable gviz_uri =
335 let uri = NUri.uri_of_string "cic:/dummy/dec.con" in
336 NReference.reference_of_spec uri NReference.Decl;
338 val dep_contextual_menu = GMenu.menu ()
341 win#mathOrListNotebook#set_show_tabs false;
342 win#browserForwardButton#misc#set_sensitive false;
343 win#browserBackButton#misc#set_sensitive false;
344 ignore (win#browserUri#connect#activate (handle_error' (fun () ->
345 self#loadInput win#browserUri#text)));
346 ignore (win#browserHomeButton#connect#clicked (handle_error' (fun () ->
347 self#load (`About `Current_proof))));
348 ignore (win#browserRefreshButton#connect#clicked
349 (handle_error' (self#refresh ~force:true)));
350 ignore (win#browserBackButton#connect#clicked (handle_error' self#back));
351 ignore (win#browserForwardButton#connect#clicked
352 (handle_error' self#forward));
353 ignore (win#toplevel#event#connect#delete (fun _ ->
354 let my_id = Oo.id self in
355 cicBrowsers := List.filter (fun b -> Oo.id b <> my_id) !cicBrowsers;
357 ignore(win#whelpResultTreeview#connect#row_activated
358 ~callback:(fun _ _ ->
359 handle_error (fun () -> self#loadInput (self#_getSelectedUri ()))));
360 mathView#set_href_callback (Some (fun uri ->
361 handle_error (fun () ->
362 let uri = `NRef (NReference.reference_of_string uri) in
364 gviz#connect_href (fun button_ev attrs ->
365 let time = GdkEvent.Button.time button_ev in
366 let uri = List.assoc "href" attrs in
367 gviz_uri <- NReference.reference_of_string uri;
368 match GdkEvent.Button.button button_ev with
369 | button when button = MatitaMisc.left_button -> self#load (`NRef gviz_uri)
370 | button when button = MatitaMisc.right_button ->
371 dep_contextual_menu#popup ~button ~time
373 connect_menu_item win#browserCloseMenuItem (fun () ->
374 let my_id = Oo.id self in
375 cicBrowsers := List.filter (fun b -> Oo.id b <> my_id) !cicBrowsers;
376 win#toplevel#misc#hide(); win#toplevel#destroy ());
377 connect_menu_item win#browserUrlMenuItem (fun () ->
378 win#browserUri#misc#grab_focus ());
380 self#_load (`About `Blank);
383 val mutable current_entry = `About `Blank
385 (** @return None if no object uri can be built from the current entry *)
386 method private currentCicUri =
387 match current_entry with
388 | `NRef uri -> Some uri
392 new MatitaGtkMisc.taggedStringListModel tags win#whelpResultTreeview
394 val mutable lastDir = "" (* last loaded "directory" *)
396 method mathView = mathView
398 method private _getSelectedUri () =
399 match model#easy_selection () with
400 | [sel] when is_uri sel -> sel (* absolute URI selected *)
401 (* | [sel] -> win#browserUri#entry#text ^ sel |+ relative URI selected +| *)
402 | [sel] -> lastDir ^ sel
405 (** history RATIONALE
407 * All operations about history are done using _historyFoo.
408 * Only toplevel functions (ATM load and loadInput) call _historyAdd.
411 method private _historyAdd item =
413 win#browserBackButton#misc#set_sensitive true;
414 win#browserForwardButton#misc#set_sensitive false
416 method private _historyPrev () =
417 let item = history#previous in
418 if history#is_begin then win#browserBackButton#misc#set_sensitive false;
419 win#browserForwardButton#misc#set_sensitive true;
422 method private _historyNext () =
423 let item = history#next in
424 if history#is_end then win#browserForwardButton#misc#set_sensitive false;
425 win#browserBackButton#misc#set_sensitive true;
428 (** notebook RATIONALE
430 * Use only these functions to switch between the tabs
432 method private _showMath = win#mathOrListNotebook#goto_page 0
433 method private _showList = win#mathOrListNotebook#goto_page 1
434 method private _showEgg = win#mathOrListNotebook#goto_page 2
435 method private _showGviz = win#mathOrListNotebook#goto_page 3
436 method private _showSearch = win#mathOrListNotebook#goto_page 4
438 method private back () =
440 self#_load (self#_historyPrev ())
441 with MatitaMisc.History_failure -> ()
443 method private forward () =
445 self#_load (self#_historyNext ())
446 with MatitaMisc.History_failure -> ()
448 (* loads a uri which can be a cic uri or an about:* uri
449 * @param uri string *)
450 method private _load ?(force=false) entry =
451 handle_error (fun () ->
452 if entry <> current_entry || entry = `About `Current_proof || entry =
453 `About `Coercions || entry = `About `CoercionsFull || force then
456 | `About `Current_proof -> self#home ()
457 | `About `Blank -> self#blank ()
458 | `About `Us -> self#egg ()
459 | `About `CoercionsFull -> self#coerchgraph false ()
460 | `About `Coercions -> self#coerchgraph true ()
461 | `About `Hints -> self#hints ()
462 | `About `TeX -> self#tex ()
463 | `About `Grammar -> self#grammar ()
464 | `Check term -> self#_loadCheck term
465 | `NCic (term, ctx, metasenv, subst) ->
466 self#_loadTermNCic term metasenv subst ctx
467 | `Dir dir -> self#_loadDir dir
468 | `NRef nref -> self#_loadNReference nref);
472 method private blank () =
474 mathView#load_root (Lazy.force empty_mathml)
476 method private _loadCheck _term =
477 failwith "not implemented _loadCheck";
480 method private egg () =
482 Lazy.force load_easter_egg
484 method private redraw_gviz ?center_on () =
485 if Sys.command "which dot" = 0 then
486 let tmpfile, oc = Filename.open_temp_file "matita" ".dot" in
487 (* MATITA 1.0 let fmt = Format.formatter_of_out_channel oc in
488 MetadataDeps.DepGraph.render fmt gviz_graph;*)
490 gviz#load_graph_from_file ~gviz_cmd:"tred | dot" tmpfile;
491 (match center_on with
493 | Some uri -> gviz#center_on_href (NReference.string_of_reference uri));
494 HExtlib.safe_remove tmpfile
496 MatitaGtkMisc.report_error ~title:"graphviz error"
497 ~message:("Graphviz is not installed but is necessary to render "^
498 "the graph of dependencies amoung objects. Please install it.")
499 ~parent:win#toplevel ()
501 method private dependencies _direction _uri () =
502 assert false (* MATITA 1.0
503 let dbd = LibraryDb.instance () in
506 | `Fwd -> MetadataDeps.DepGraph.direct_deps ~dbd uri
507 | `Back -> MetadataDeps.DepGraph.inverse_deps ~dbd uri in
508 gviz_graph <- graph; (** XXX check this for memory consuption *)
509 self#redraw_gviz ~center_on:uri ();
512 method private coerchgraph tred () =
513 load_coerchgraph tred ();
516 method private hints () =
520 method private tex () =
521 let b = Buffer.create 1000 in
522 Printf.bprintf b "UTF-8 equivalence classes (rotate with ALT-L):\n\n";
525 List.iter (fun sym ->
526 Printf.bprintf b " %s" (Glib.Utf8.from_unichar sym)
528 Printf.bprintf b "\n";
531 (fun l1 l2 -> compare (List.hd l1) (List.hd l2))
532 (Virtuals.get_all_eqclass ()));
533 Printf.bprintf b "\n\nVirtual keys (trigger with ALT-L):\n\n";
536 Printf.bprintf b " %s:\n" tag;
538 (fun names, symbol ->
539 Printf.bprintf b " \t%s\t%s\n"
540 (Glib.Utf8.from_unichar symbol)
541 (String.concat ", " names))
543 (fun (_,a) (_,b) -> compare a b)
545 Printf.bprintf b "\n")
547 (fun (a,_) (b,_) -> compare a b)
548 (Virtuals.get_all_virtuals ()));
549 self#_loadText (Buffer.contents b)
551 method private _loadText text =
552 searchText#source_buffer#set_text text;
553 win#entrySearch#misc#grab_focus ();
556 method private grammar () =
558 (Print_grammar.ebnf_of_term (get_matita_script_current ())#status);
560 method private home () =
562 let status = (get_matita_script_current ())#status in
563 match status#ng_mode with
564 `ProofMode -> self#_loadNObj status status#obj
567 method private _loadNReference (NReference.Ref (uri,_)) =
568 let status = (get_matita_script_current ())#status in
569 let obj = NCicEnvironment.get_checked_obj status uri in
570 self#_loadNObj status obj
572 method private _loadDir dir =
573 let content = Http_getter.ls ~local:false dir in
579 | Http_getter_types.Ls_section s -> "dir", s
580 | Http_getter_types.Ls_object o -> "obj", o.Http_getter_types.uri)
586 method private setEntry entry =
587 win#browserUri#set_text (MatitaTypes.string_of_entry entry);
588 current_entry <- entry
590 method private _loadNObj status obj =
591 (* showMath must be done _before_ loading the document, since if the
592 * widget is not mapped (hidden by the notebook) the document is not
595 mathView#load_nobject status obj
597 method private _loadTermNCic term m s c =
599 let m = (0,([],c,term))::m in
600 let status = (get_matita_script_current ())#status in
601 mathView#nload_sequent status m s d;
604 method private _loadList l =
605 model#list_store#clear ();
606 List.iter (fun (tag, s) -> model#easy_append ~tag s) l;
609 (** { public methods, all must call _load!! } *)
612 handle_error (fun () -> self#_load entry; self#_historyAdd entry)
614 (** this is what the browser does when you enter a string an hit enter *)
615 method loadInput txt =
616 let txt = HExtlib.trim_blanks txt in
617 (* (* ZACK: what the heck? *)
619 UriManager.string_of_uri
620 (UriManager.strip_xpointer (UriManager.uri_of_string txt))
625 | txt when is_uri txt ->
626 `NRef (NReference.reference_of_string ((*fix_uri*) txt))
627 | txt when is_dir txt -> `Dir (MatitaMisc.normalize_dir txt)
630 MatitaTypes.entry_of_string txt
631 with Invalid_argument _ ->
633 (GrafiteTypes.Command_error(sprintf "unsupported uri: %s" txt)))
636 self#_historyAdd entry
638 (** {2 methods used by constructor only} *)
641 method history = history
642 method currentEntry = current_entry
643 method refresh ~force () = self#_load ~force current_entry
647 let sequentsViewer ~(notebook:GPack.notebook) ~(cicMathView:cicMathView) ():
648 MatitaGuiTypes.sequentsViewer
650 (new sequentsViewer ~notebook ~cicMathView ():> MatitaGuiTypes.sequentsViewer)
652 let new_cicBrowser () =
653 let size = BuildTimeConf.browser_history_size in
654 let rec aux history =
655 let browser = new cicBrowser_impl ~history () in
656 let win = browser#win in
657 ignore (win#browserNewButton#connect#clicked (fun () ->
659 new MatitaMisc.browser_history ~memento:history#save size
662 let newBrowser = aux history in
663 newBrowser#load browser#currentEntry));
665 (* attempt (failed) to close windows on CTRL-W ... *)
666 MatitaGtkMisc.connect_key win#browserWinEventBox#event ~modifiers:[`CONTROL]
667 GdkKeysyms._W (fun () -> win#toplevel#destroy ());
669 cicBrowsers := browser :: !cicBrowsers;
672 let history = new MatitaMisc.browser_history size (`About `Blank) in
675 (** @param reuse if set reused last opened cic browser otherwise
676 * opens a new one. default is false *)
677 let cicBrowser ?(reuse=false) t =
680 (match !cicBrowsers with [] -> new_cicBrowser () | b :: _ -> b)
686 | Some t -> browser#load t
689 let default_cicMathView () =
690 let res = cicMathView ~show:true () in
691 res#set_href_callback
693 let uri = `NRef (NReference.reference_of_string uri) in
694 cicBrowser (Some uri)));
697 let cicMathView_instance =
698 MatitaMisc.singleton default_cicMathView
700 let default_sequentsViewer notebook =
701 let cicMathView = cicMathView_instance () in
702 sequentsViewer ~notebook ~cicMathView ()
704 let sequentsViewer_instance =
705 let already_used = ref false in
707 if !already_used then assert false
709 (already_used := true;
710 default_sequentsViewer notebook)
712 let refresh_all_browsers () =
713 List.iter (fun b -> b#refresh ~force:false ()) !cicBrowsers
715 let get_math_views () =
716 (cicMathView_instance ()) :: (List.map (fun b -> b#mathView) !cicBrowsers)
718 let find_selection_owner () =
721 | [] -> raise Not_found
723 (match mv#get_selections with
727 aux (get_math_views ())
729 let has_selection () =
730 try ignore (find_selection_owner ()); true
731 with Not_found -> false
733 let math_view_clipboard = ref None (* associative list target -> string *)
734 let has_clipboard () = !math_view_clipboard <> None
735 let empty_clipboard () = math_view_clipboard := None
737 let copy_selection () =
739 math_view_clipboard :=
740 Some ((find_selection_owner ())#strings_of_selection)
741 with Not_found -> failwith "no selection"
743 let paste_clipboard paste_kind =
744 match !math_view_clipboard with
745 | None -> failwith "empty clipboard"
747 (try List.assoc paste_kind cb with Not_found -> assert false)