- (* math viewers *)
-let _ =
- let cic_math_view = MatitaMathView.cicMathView_instance () in
- let sequents_viewer = MatitaMathView.sequentsViewer_instance () in
- sequents_viewer#load_logo;
- cic_math_view#set_href_callback
- (Some (fun uri ->
- let uri =
- try
- `Uri (UriManager.uri_of_string uri)
- with
- UriManager.IllFormedUri _ ->
- `NRef (NReference.reference_of_string uri)
- in
- (MatitaMathView.cicBrowser ())#load uri));
- let browser_observer _ = MatitaMathView.refresh_all_browsers () in
- let sequents_observer grafite_status =
- sequents_viewer#reset;
- match grafite_status#ng_mode with
- `ProofMode ->
- sequents_viewer#nload_sequents grafite_status;
- (try
- script#setGoal
- (Some (Continuationals.Stack.find_goal grafite_status#stack));
- let goal =
- match script#goal with
- None -> assert false
- | Some n -> n
- in
- sequents_viewer#goto_sequent grafite_status goal
- with Failure _ -> script#setGoal None);
- | `CommandMode -> sequents_viewer#load_logo
- in
- script#addObserver sequents_observer;
- script#addObserver browser_observer
-