init.m

%% init
%   initialize the gui
% inputs:
%   obj:GUI - GUI object
% outputs:
%   none
% Author: Colin Eles elesc@mcmaster.ca
% Organization: McMaster Centre for Software Certification
function [] = init(object)

% create the handles for the gui objects
if object.mode == 1
    name = get_param(object.block_handle,'Name');
elseif object.mode == 0
    name = 'Table Tool';
end
% main figure
object.fig = figure('units','pixels',...
    'position',[0 0 object.fig_width object.fig_height],...
    'menubar','none',...
    'name','Table Tool',...
    'numbertitle','off',...
    'resize','on',...
    'Name',name,...
    'CloseRequestFcn',@(src,event)close_fig(object,src,event),...
    'ResizeFcn',@(src,event)resize_fig(object,src,event));


% edit button
object.edit_tog = uicontrol('style','toggle',...
    'units','pix',...
    'string','Edit',...
    'HorizontalAlign','left',...
    'Parent',object.fig,...
    'Value',object.edit,...
    'callback',@(src,event)edit_tog_call(object,src,event));

% Save button
object.save_pb = uicontrol('style','push',...
    'units','pix',...
    'string','Save',...
    'HorizontalAlign','left',...
    'Parent',object.fig,...
    'callback',@(src,event)save_call(object,src,event));

% Close button
object.close_pb = uicontrol('style','push',...
    'units','pix',...
    'string','Close',...
    'HorizontalAlign','left',...
    'Parent',object.fig,...
    'callback',@(src,event)close_fig(object,src,event));

% Save external button
object.save_ext_pb = uicontrol('style','push',...
    'units','pix',...
    'string','Save Ext',...
    'HorizontalAlign','left',...
    'Parent',object.fig,...
    'callback',@(src,event)save_ext_call(object,src,event));


% Check button
object.check_pb = uicontrol('style','push',...
    'units','pix',...
    'string','Syntax',...
    'HorizontalAlign','left',...
    'Parent',object.fig,...
    'Max',2.0,...
    'callback',@(src,event)check_call(object,src,event));



% PVS button
object.pvs_pb = uicontrol('style','push',...
    'units','pix',...
    'string','Typecheck',...
    'HorizontalAlign','left',...
    'Parent',object.fig,...
    'callback',@(src,event)typecheck_call(object,src,event));

% Input/Output button
object.input_pb = uicontrol('style','push',...
    'units','pix',...
    'string','Ports',...
    'HorizontalAlign','left',...
    'Parent',object.fig,...
    'callback',@(src,event)input_call(object,src,event));

% Settings button
object.settings_pb = uicontrol('style','push',...
    'units','pix',...
    'string','Settings',...
    'HorizontalAlign','left',...
    'Parent',object.fig,...
    'callback',@(src,event)settings_call(object,src,event));

% Expression Name Label
object.name_label = uicontrol('style','text',...
    'string','Expression Name',...
    'HorizontalAlign','right',...
    'BackgroundColor',get(object.fig,'Color'));

% Expression Name Edit box
object.function_name_control = uicontrol('style','edit',...
    'units','pix',...
    'Parent',object.fig,...
    'HorizontalAlign','center',...
    'FontWeight','bold',...
    'FontSize',12,...
    'Max',2.0,...
    'KeyPressFcn',@(src,event)textbox_callback(object,src,event),...
    'BackgroundColor',[1 1 1]);

% input list label
object.input_label = uicontrol('style','text',...
    'string','Inputs',...
    'HorizontalAlign','right',...
    'BackgroundColor',get(object.fig,'Color'));

% input list edit box
object.function_inputs_control = uicontrol('style','edit',...
    'units','pix',...
    'Parent',object.fig,...
    'HorizontalAlign','center',...
    'FontWeight','bold',...
    'Max',2.0,...
    'FontSize',12,...
    'KeyPressFcn',@(src,event)textbox_callback(object,src,event),...
    'BackgroundColor',[1 1 1]);



% load the function name and inputs
if (~isempty(object.function_name_text))
    set(object.function_name_control,'String',object.function_name_text);
end
if (~isempty(object.function_inputs_text))
    set(object.function_inputs_control,'String',object.function_inputs_text);
end


% Set up Menu
filemenu = uimenu('Label','File');
editmenu = uimenu('Label','Edit');
checkmenu = uimenu('Label','Typecheck');
helpmenu = uimenu('Label','Help');
uimenu(filemenu,'Label','New','Accelerator','n','Callback',@(src,event)new_call(object,src,event));
uimenu(filemenu,'Label','Open...','Callback',@(src,event)open_call(object,src,event));
uimenu(filemenu,'Label','Save to Block','Separator','on','Accelerator','s','Callback',@(src,event)save_call(object,src,event));
uimenu(filemenu,'Label','Save to M-File','Callback',@(src,event)save_ext_call(object,src,event));
uimenu(filemenu,'Label','Close','Accelerator','w','Separator','on','Callback',@(src,event)close_fig(object,src,event));
object.undo_opt = uimenu(editmenu,'Label','Undo','Accelerator','z','Callback',@(src,event)undo_call(object,src,event));
object.redo_opt = uimenu(editmenu,'Label','Redo','Accelerator','r','Callback',@(src,event)redo_call(object,src,event));
uimenu(editmenu,'Label','Show edit controls','Checked','on','Separator','on');
uimenu(editmenu,'Label','Ports and Data Manager','Accelerator','p','Callback',@(src,event)input_call(object,src,event));
multi_mode_menu = uimenu(editmenu,'Label','Output Mode');
object.multi_opt_reg = uimenu(multi_mode_menu,'Label','One Output','Callback',@(src,event)multi_select_call(object,src,event));
object.multi_opt_out = uimenu(multi_mode_menu,'Label','Multiple Outputs','Callback',@(src,event)multi_select_call(object,src,event));
uimenu(checkmenu,'Label','Typecheck','Accelerator','t','Callback',@(src,event)typecheck_call(object,src,event));
prover_menu = uimenu(checkmenu,'Label','Default Prover');
object.prover_opt_cvc = uimenu(prover_menu,'Label','CVC3','Callback',@(src,event)prover_select_call(object,src,event));
object.prover_opt_pvs = uimenu(prover_menu,'Label','PVS','Callback',@(src,event)prover_select_call(object,src,event));
object.prover_opt_smtlib = uimenu(prover_menu,'Label','Z3','Callback',@(src,event)prover_select_call(object,src,event));
uimenu(checkmenu,'Label', 'Syntax Check','Callback',@(src,event)check_call(object,src,event));


uimenu(checkmenu,'Label','CVC Typecheck','Separator','on','Callback',@(src,event)cvc_ext_call(object,src,event));
uimenu(checkmenu,'Label','CVC Generate File');

uimenu(checkmenu,'Label','PVS Typecheck','Separator','on','Callback',@(src,event)pvs_ext_call(object,src,event));
uimenu(checkmenu,'Label','PVS Settings','Callback',@(src,event)settings_call(object,src,event));
uimenu(checkmenu,'Label','PVS Check Status','Callback',@(src,event)prf_file_call(object,src,event));
uimenu(checkmenu,'Label','PVS Generate file','Callback',@(src,event)pvs_file_call(object,src,event));
uimenu(checkmenu,'Label','PVS Typecheck SimTypes','Callback',@(src,event)pvs_ext_call_sim(object,src,event));

uimenu(checkmenu,'Label','Z3 Typecheck','Separator','on','Callback',@(src,event)smtlib_ext_call(object,src,event));

uimenu(helpmenu,'Label','Product Help','Callback',@(src,event)help_call(object,src,event));
uimenu(helpmenu,'Label','About Tabular Expression Toolbox','Callback',@(src,event)about_call(object,src,event));

object.set_command_pos;
object.reset_wh();
object.draw_allgrids(2);
object.saved = 1;
object.setPBenable;

object.default_prover = object.CVC_const;


object.settings = TTSettings();
if isfield(object.Data.settings,'set')
    object.settings.setvalues(object.Data.settings);
else
    object.settings.init();
    
end

object.undo_man = UndoManager();



object.update_Statusbar;
object.update_multi_check_status;
object.update_prover_check_status;
object.update_undoredo;

object.PVS = PVS_checker(object.Data);
object.EMLGen = EMLGenerator(object.Data);


object.CVC = CVC_checker(object.Data);


object.initialized = 1;
object.Data.open = 1;
object.Data.fig = object.fig;




end