val mutable scrolledWin: GBin.scrolled_window option = None
(* scrolled window to which the sequentViewer is currently attached *)
val logo = (GMisc.image
- ~file:(BuildTimeConf.runtime_base_dir ^ "/logo/matita_medium.png") ()
+ ~file:(MatitaMisc.image_path "matita_medium.png") ()
:> GObj.widget)
val logo_with_qed = (GMisc.image
- ~file:(BuildTimeConf.runtime_base_dir ^ "/logo/matita_small.png") ()
+ ~file:(MatitaMisc.image_path "matita_small.png") ()
:> GObj.widget)
method load_logo =
w#remove cicMathView#coerce;
scrolledWin <- None
| None -> ());
- for i = 0 to pages do notebook#remove_page 0 done;
+ (match switch_page_callback with
+ | Some id ->
+ GtkSignal.disconnect notebook#as_widget id;
+ switch_page_callback <- None
+ | None -> ());
+ for i = 0 to pages do notebook#remove_page 0 done;
notebook#set_show_tabs true;
pages <- 0;
page2goal <- [];
goal2page <- [];
goal2win <- [];
- _metasenv <- [];
+ _metasenv <- [];
self#script#setGoal ~-1;
- (match switch_page_callback with
- | Some id ->
- GtkSignal.disconnect notebook#as_widget id;
- switch_page_callback <- None
- | None -> ())
method load_sequents (status: ProofEngineTypes.status) =
let ((_, metasenv, _, _), goal) = status in
let handle_error f =
try
f ()
- with exn -> fail (MatitaExcPp.to_string exn)
+ with exn ->
+ if Helm_registry.get_bool "matita.catch_top_level_exn" then
+ fail (MatitaExcPp.to_string exn)
+ else raise exn
in
let handle_error' f = (fun () -> handle_error (fun () -> f ())) in
+ let load_easter_egg = lazy (
+ win#easterEggImage#set_file (MatitaMisc.image_path "meegg.png"))
+ in
object (self)
inherit scriptAccessor
*
* Use only these functions to switch between the tabs
*)
- method private _showList = win#mathOrListNotebook#goto_page 1
method private _showMath = win#mathOrListNotebook#goto_page 0
-
+ method private _showList = win#mathOrListNotebook#goto_page 1
+
method private back () =
try
self#_load (self#_historyPrev ())
(* loads a uri which can be a cic uri or an about:* uri
* @param uri string *)
method private _load ?(force=false) entry =
- try
+ handle_error (fun () ->
if entry <> current_entry || entry = `About `Current_proof || force then
begin
(match entry with
| `About `Current_proof -> self#home ()
| `About `Blank -> self#blank ()
- | `About `Us -> () (* TODO implement easter egg here :-] *)
+ | `About `Us -> self#egg ()
| `Check term -> self#_loadCheck term
| `Cic (term, metasenv) -> self#_loadTermCic term metasenv
| `Dir dir -> self#_loadDir dir
self#_loadList (List.map (fun r -> "obj",
UriManager.string_of_uri r) results));
self#setEntry entry
- end
- with exn -> fail (MatitaExcPp.to_string exn)
+ end)
method private blank () =
self#_showMath;
failwith "not implemented _loadCheck";
self#_showMath
+ method private egg () =
+ win#mathOrListNotebook#goto_page 2;
+ Lazy.force load_easter_egg
+
method private home () =
self#_showMath;
match self#script#status.proof_status with