Newer
Older
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
% 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',...
Colin Eles
committed
'string','Syntax',...
'HorizontalAlign','left',...
'Parent',object.fig,...
'callback',@(src,event)check_call(object,src,event));
Colin Eles
committed
% 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,...
'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',...
'FontSize',12,...
'KeyPressFcn',@(src,event)textbox_callback(object,src,event),...
'BackgroundColor',[1 1 1]);
Colin Eles
committed
% 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');
Colin Eles
committed
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));
Colin Eles
committed
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));
Colin Eles
committed
uimenu(checkmenu,'Label', 'Syntax Check','Callback',@(src,event)check_call(object,src,event));
Colin Eles
committed
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.saved = 1;
object.setPBenable;
Colin Eles
committed
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;
Colin Eles
committed
object.update_prover_check_status;
object.update_undoredo;
object.PVS = PVS_checker(object.Data);
object.EMLGen = EMLGenerator(object.Data);
Colin Eles
committed
object.CVC = CVC_checker(object.Data);