MatitaMisc.decrease_font_size;
connect_menu_item main#normalFontSizeMenuItem
MatitaMisc.reset_font_size;
+ ignore (main#scriptNotebook#connect#switch_page
+ (fun page -> (MatitaScript.at_page page)#activate));
method private externalEditor () =
let script = MatitaScript.current () in
method newScript () =
let scrolledWindow = GBin.scrolled_window () in
let tab_label = GMisc.label ~text:"foo" () in
- ignore (main#scriptNotebook#prepend_page ~tab_label:tab_label#coerce scrolledWindow#coerce);
let script =
MatitaScript.script
~urichooser:(fun source_view uris ->
~parent:(MatitaMisc.get_gui ())#main#toplevel ())
~parent:scrolledWindow ~tab_label ()
in
+ ignore (main#scriptNotebook#prepend_page ~tab_label:tab_label#coerce scrolledWindow#coerce);
main#scriptNotebook#goto_page 0;
sequents_viewer#reset;
sequents_viewer#load_logo;
`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
+ Continuationals.Stack.find_goal grafite_status#stack
in
sequents_viewer#goto_sequent grafite_status goal
- with Failure _ -> script#setGoal None);
+ with Failure _ -> ());
| `CommandMode -> sequents_viewer#load_logo
in
script#addObserver sequents_observer;