/[eiffelstudio]/branches/eth/eve/Src/Eiffel/interface/graphical/tools/autoproof/es_autoproof_tool_panel.e
ViewVC logotype

Contents of /branches/eth/eve/Src/Eiffel/interface/graphical/tools/autoproof/es_autoproof_tool_panel.e

Parent Directory Parent Directory | Revision Log Revision Log


Revision 93597 - (show annotations)
Tue Dec 3 00:48:44 2013 UTC (5 years, 10 months ago) by julian
File size: 26668 byte(s)
AutoProof: special translation for lemma and functional
1 note
2 description:
3 "Graphical panel for Proof tool"
4 date: "$Date$"
5 revision: "$Revision$"
6
7 class
8 ES_AUTOPROOF_TOOL_PANEL
9
10 inherit
11 ES_CLICKABLE_EVENT_LIST_TOOL_PANEL_BASE
12 rename
13 messages as es_messages
14 redefine
15 build_tool_interface,
16 on_before_initialize,
17 on_after_initialized,
18 internal_recycle,
19 create_right_tool_bar_items,
20 is_event_list_synchronized_on_initialized,
21 is_event_list_scrolled_automatically,
22 is_appliable_event,
23 on_event_item_added,
24 on_event_item_removed,
25 find_event_row
26 end
27
28 SESSION_EVENT_OBSERVER
29 export {NONE} all end
30
31 SHARED_ERROR_TRACER
32 export {NONE} all end
33
34 EBB_SHARED_BLACKBOARD
35
36 E2B_SHARED_CONTEXT
37
38 create {ES_AUTOPROOF_TOOL}
39 make
40
41 feature {NONE} -- Initialization
42
43 on_before_initialize
44 -- <Precursor>
45 local
46 l_shared_writer: EB_SHARED_WRITER
47 do
48 Precursor
49
50 -- create l_shared_writer
51 -- l_shared_writer.label_font_table.item (0).set_height (16)
52 -- l_shared_writer.label_font_table.item (1).set_height (16)
53 -- l_shared_writer.label_font_table.item (2).set_height (16)
54
55 -- We want the tool to synchronize with the event list, when first initialized.
56 is_event_list_synchronized_on_initialized := True
57 end
58
59 on_after_initialized
60 -- <Precursor>
61 do
62 -- Bind redirecting pick and drop actions
63 stone_director.bind (grid_events, Current)
64
65 -- Hook up events for session data
66 if session_manager.is_service_available then
67 session_data.session_connection.connect_events (Current)
68 end
69
70 is_event_list_scrolled_automatically := False
71
72 Precursor
73 end
74
75 create_tool_bar_items: ARRAYED_LIST [SD_TOOL_BAR_ITEM]
76 -- <Precursor>
77 do
78 -- "toggle successful" button
79 create successful_button.make
80 successful_button.set_pixmap (stock_pixmaps.general_check_document_icon)
81 successful_button.set_pixel_buffer (stock_pixmaps.general_check_document_icon_buffer)
82 successful_button.enable_select
83 successful_button.select_actions.extend (agent on_update_visiblity)
84
85 -- "toggle failed" button
86 create failed_button.make
87 failed_button.set_pixmap (stock_pixmaps.debug_exception_handling_icon)
88 failed_button.set_pixel_buffer (stock_pixmaps.debug_exception_handling_icon_buffer)
89 failed_button.enable_select
90 failed_button.select_actions.extend (agent on_update_visiblity)
91
92 -- "toggle skipped" button
93 create skipped_button.make
94 skipped_button.set_pixmap (stock_pixmaps.general_warning_icon)
95 skipped_button.set_pixel_buffer (stock_pixmaps.general_warning_icon_buffer)
96 skipped_button.enable_select
97 skipped_button.select_actions.extend (agent on_update_visiblity)
98
99 update_button_titles
100
101 create Result.make (5)
102 proof_button := (create {ES_AUTOPROOF_COMMAND}.make).new_sd_toolbar_item (True)
103 Result.extend (proof_button)
104 Result.extend (create {SD_TOOL_BAR_SEPARATOR}.make)
105 Result.extend (successful_button)
106 Result.extend (failed_button)
107 -- Result.extend (skipped_button)
108 end
109
110 create_right_tool_bar_items: ARRAYED_LIST [SD_TOOL_BAR_ITEM]
111 -- <Precursor>
112 local
113 l_box: EV_HORIZONTAL_BOX
114 l_button: SD_TOOL_BAR_BUTTON
115 l_popup_button: SD_TOOL_BAR_POPUP_BUTTON
116 do
117 -- live text filter
118 create l_box
119 l_box.extend (create {EV_LABEL}.make_with_text (ep_names.tool_text_filter + ": "))
120 l_box.disable_item_expand (l_box.last)
121 create text_filter
122 text_filter.key_release_actions.force_extend (agent on_update_visiblity)
123 text_filter.set_minimum_width_in_characters (10)
124 l_box.extend (text_filter)
125 l_box.disable_item_expand (text_filter)
126
127 -- clear button
128 create l_button.make
129 l_button.set_pixmap (stock_mini_pixmaps.general_delete_icon)
130 l_button.pointer_button_press_actions.force_extend (
131 agent
132 do
133 text_filter.set_text ("")
134 on_update_visiblity
135 end
136 )
137
138 -- options button
139 create l_popup_button.make
140 l_popup_button.set_pixmap (stock_pixmaps.metric_filter_icon)
141 l_popup_button.set_pixel_buffer (stock_pixmaps.metric_filter_icon_buffer)
142 l_popup_button.set_tooltip ("AutoProof options")
143 l_popup_button.set_menu_function (agent build_options_menu)
144
145 create Result.make (4)
146 Result.extend (create {SD_TOOL_BAR_RESIZABLE_ITEM}.make (l_box))
147 Result.extend (l_button)
148 Result.extend (create {SD_TOOL_BAR_SEPARATOR}.make)
149 Result.extend (l_popup_button)
150 end
151
152 build_options_menu: EV_MENU
153 -- Build options menu.
154 local
155 l_item: EV_CHECK_MENU_ITEM
156 do
157 create Result
158
159 create l_item.make_with_text_and_action ("Two-step verification",
160 agent do
161 options.set_two_step_verification_enabled (not options.is_two_step_verification_enabled)
162 end)
163 if options.is_two_step_verification_enabled then
164 l_item.toggle
165 end
166 Result.extend (l_item)
167
168 create l_item.make_with_text_and_action ("Automatic inlining of routines without postcondition",
169 agent do
170 options.set_automatic_inlining_enabled (not options.is_automatic_inlining_enabled)
171 end)
172 if options.is_automatic_inlining_enabled then
173 l_item.toggle
174 end
175 Result.extend (l_item)
176
177 create l_item.make_with_text_and_action ("Automatic unrolling of loops without invariants",
178 agent do
179 options.set_automatic_loop_unrolling_enabled (not options.is_automatic_loop_unrolling_enabled)
180 end)
181 if options.is_automatic_loop_unrolling_enabled then
182 l_item.toggle
183 end
184 Result.extend (l_item)
185
186 create l_item.make_with_text_and_action ("Use sound loop unrolling",
187 agent do
188 options.set_sound_loop_unrolling_enabled (not options.is_sound_loop_unrolling_enabled)
189 end)
190 if options.is_sound_loop_unrolling_enabled then
191 l_item.toggle
192 end
193 Result.extend (l_item)
194
195 create l_item.make_with_text_and_action ("Check integer overflow",
196 agent do
197 options.set_checking_overflow (not options.is_checking_overflow)
198 end)
199 if options.is_checking_overflow then
200 l_item.toggle
201 end
202 Result.extend (l_item)
203
204 Result.extend (create {EV_MENU_SEPARATOR})
205
206 create l_item.make_with_text_and_action ("Check frame condition",
207 agent do
208 options.set_checking_frame (not options.is_checking_frame)
209 end)
210 if options.is_checking_frame then
211 l_item.toggle
212 end
213 Result.extend (l_item)
214
215 create l_item.make_with_text_and_action ("Enable ownership",
216 agent do
217 options.set_ownership_enabled (not options.is_ownership_enabled)
218 end)
219 if options.is_ownership_enabled then
220 l_item.toggle
221 end
222 Result.extend (l_item)
223
224 create l_item.make_with_text_and_action ("- use defaults",
225 agent do
226 options.set_ownership_defaults_enabled (not options.is_ownership_defaults_enabled)
227 end)
228 if options.is_ownership_defaults_enabled then
229 l_item.toggle
230 end
231 Result.extend (l_item)
232
233 create l_item.make_with_text_and_action ("Enable postcondition mutation",
234 agent do
235 options.set_postcondition_mutation_enabled (not options.is_postcondition_mutation_enabled)
236 end)
237 if options.is_postcondition_mutation_enabled then
238 l_item.toggle
239 end
240 Result.extend (l_item)
241
242 create l_item.make_with_text_and_action ("- with coupled mutations",
243 agent do
244 options.set_coupled_mutations_enabled (not options.is_coupled_mutations_enabled)
245 end)
246 if options.is_coupled_mutations_enabled then
247 l_item.toggle
248 end
249 Result.extend (l_item)
250
251 create l_item.make_with_text_and_action ("- with uncoupled mutations",
252 agent do
253 options.set_uncoupled_mutations_enabled (not options.is_uncoupled_mutations_enabled)
254 end)
255 if options.is_uncoupled_mutations_enabled then
256 l_item.toggle
257 end
258 Result.extend (l_item)
259
260 create l_item.make_with_text_and_action ("- with aging",
261 agent do
262 options.set_aging_enabled (not options.is_aging_enabled)
263 end)
264 if options.is_aging_enabled then
265 l_item.toggle
266 end
267 Result.extend (l_item)
268 end
269
270 build_tool_interface (a_widget: ES_GRID)
271 -- Builds the tools user interface elements.
272 -- Note: This function is called prior to showing the tool for the first time.
273 --
274 -- `a_widget': A widget to build the tool interface using.
275 local
276 l_col: EV_GRID_COLUMN
277 do
278 Precursor {ES_CLICKABLE_EVENT_LIST_TOOL_PANEL_BASE} (a_widget)
279 a_widget.set_column_count_to (time_column)
280
281 -- Create columns
282 l_col := a_widget.column (1)
283 l_col.set_width (20)
284 l_col := a_widget.column (icon_column)
285 l_col.set_width (20)
286 l_col := a_widget.column (class_column)
287 l_col.set_title (ep_names.tool_header_class)
288 l_col.set_width (100)
289 l_col := a_widget.column (feature_column)
290 l_col.set_title (ep_names.tool_header_feature)
291 l_col.set_width (120)
292 l_col := a_widget.column (info_column)
293 l_col.set_title (ep_names.tool_header_information)
294 l_col.set_width (300)
295 l_col := a_widget.column (position_column)
296 l_col.set_title (ep_names.tool_header_position)
297 l_col.set_width (40)
298 l_col := a_widget.column (time_column)
299 l_col.set_title (ep_names.tool_header_time)
300 l_col.set_width (50)
301
302 a_widget.enable_tree
303 a_widget.disable_row_height_fixed
304 a_widget.enable_auto_size_best_fit_column (info_column)
305
306 -- Enable sorting
307 enable_sorting_on_columns (
308 <<
309 a_widget.column (icon_column),
310 a_widget.column (class_column),
311 a_widget.column (feature_column),
312 a_widget.column (time_column)
313 >>)
314 end
315
316 feature -- Access
317
318 proof_button: EB_SD_COMMAND_TOOL_BAR_BUTTON
319 -- Button to launch AutoProof.
320
321 successful_count: INTEGER
322 -- Number of successful events
323
324 failed_count: INTEGER
325 -- Number of successful events
326
327 skipped_count: INTEGER
328 -- Number of successful events
329
330 feature -- Status report
331
332 show_successful: BOOLEAN
333 -- Indicates if errors should be shown
334 do
335 Result := not is_initialized or else successful_button.is_selected
336 end
337
338 show_failed: BOOLEAN
339 -- Indicates if errors should be shown
340 do
341 Result := not is_initialized or else failed_button.is_selected
342 end
343
344 show_skipped: BOOLEAN
345 -- Indicates if errors should be shown
346 do
347 Result := not is_initialized or else skipped_button.is_selected
348 end
349
350 is_item_visible (a_item: EV_GRID_ROW): BOOLEAN
351 -- Is `a_item' visible?
352 local
353 l_text: STRING
354 l_item: E2B_VERIFICATION_EVENT
355 do
356 Result := True
357 l_item ?= a_item.data
358 if l_item /= Void then
359 if is_successful_event (l_item) and not show_successful then
360 Result := False
361 elseif is_failed_event (l_item) and not show_failed then
362 Result := False
363 else
364 l_text := text_filter.text.as_lower
365 if not l_text.is_empty then
366 if
367 not l_item.context_class.name.as_lower.has_substring (l_text) and
368 (l_item.context_feature = Void or else
369 not l_item.context_feature.feature_name_32.as_lower.has_substring (l_text)) and
370 not l_item.description.as_lower.has_substring (l_text)
371 then
372 Result := False
373 end
374 end
375 end
376 end
377 end
378
379 frozen is_event_list_synchronized_on_initialized: BOOLEAN
380 -- <Precursor>
381
382 frozen is_event_list_scrolled_automatically: BOOLEAN
383 -- <Precursor>
384
385 feature {NONE} -- User interface items
386
387 successful_button: SD_TOOL_BAR_TOGGLE_BUTTON
388 -- Toogle to show/hide successful proofs
389
390 failed_button: SD_TOOL_BAR_TOGGLE_BUTTON
391 -- Toogle to show/hide failed proofs
392
393 skipped_button: SD_TOOL_BAR_TOGGLE_BUTTON
394 -- Toogle to show/hide skipped proofs
395
396 text_filter: EV_TEXT_FIELD
397 -- Text field to enter filter
398
399 feature {NONE} -- Events
400
401 on_event_item_added (a_service: EVENT_LIST_S; a_event_item: EVENT_LIST_ITEM_I)
402 -- <Precursor>
403 local
404 l_applicable: BOOLEAN
405 do
406 l_applicable := is_appliable_event (a_event_item)
407 if l_applicable and not is_initialized then
408 -- We have to perform initialization to set the icon and counter.
409 -- Synchronization with the event list service is surpress to prevent duplication of event items being added.
410 is_event_list_synchronized_on_initialized := True
411 initialize
412 end
413 if l_applicable then
414 if is_successful_event (a_event_item) then
415 successful_count := successful_count + 1
416 elseif is_failed_event (a_event_item) then
417 failed_count := failed_count + 1
418 else
419 check false end
420 end
421
422 update_button_titles
423
424 Precursor {ES_CLICKABLE_EVENT_LIST_TOOL_PANEL_BASE} (a_service, a_event_item)
425 end
426 ensure then
427 is_initialized: is_appliable_event (a_event_item) implies is_initialized
428 end
429
430 on_event_item_removed (a_service: EVENT_LIST_S; a_event_item: EVENT_LIST_ITEM_I)
431 -- <Precursor>
432 local
433 l_applicable: BOOLEAN
434 do
435 l_applicable := is_appliable_event (a_event_item)
436 if l_applicable and not is_initialized then
437 -- We have to perform initialization to set the icon and counter
438 -- Synchronization with the event list service is surpress to prevent duplication of event items being added.
439 is_event_list_synchronized_on_initialized := True
440 initialize
441 end
442 if l_applicable then
443 if is_successful_event (a_event_item) then
444 successful_count := successful_count - 1
445 elseif is_failed_event (a_event_item) then
446 failed_count := failed_count - 1
447 else
448 check false end
449 end
450
451 update_button_titles
452
453 Precursor {ES_CLICKABLE_EVENT_LIST_TOOL_PANEL_BASE} (a_service, a_event_item)
454 end
455 ensure then
456 is_initialized: is_appliable_event (a_event_item) implies is_initialized
457 end
458
459 on_update_visiblity
460 -- Called when visibility settings change
461 require
462 is_interface_usable: is_interface_usable
463 is_initialized: is_initialized
464 local
465 l_row: EV_GRID_ROW
466 l_count, i: INTEGER
467 do
468 from
469 i := 1
470 l_count := grid_events.row_count
471 until
472 i > l_count
473 loop
474 l_row := grid_events.row (i)
475 if is_item_visible (l_row) then
476 l_row.show
477 else
478 l_row.hide
479 end
480 i := i + 1
481 end
482 end
483
484 feature {NONE} -- Query
485
486 is_appliable_event (a_event_item: EVENT_LIST_ITEM_I): BOOLEAN
487 -- Determines if event `a_event_item' can be shown with the current event list tool
488 do
489 Result := attached {E2B_VERIFICATION_EVENT} a_event_item or attached {E2B_FAILED_EXECUTION_EVENT} a_event_item
490 end
491
492 is_successful_event (a_event_item: EVENT_LIST_ITEM_I): BOOLEAN
493 -- Determines if event `a_event_item' is a successful event
494 do
495 Result :=
496 attached {E2B_VERIFICATION_EVENT} a_event_item as l_event and then
497 attached {E2B_SUCCESSFUL_VERIFICATION} l_event.data
498 end
499
500 is_failed_event (a_event_item: EVENT_LIST_ITEM_I): BOOLEAN
501 -- Determines if event `a_event_item' is a failed event
502 do
503 Result :=
504 attached {E2B_VERIFICATION_EVENT} a_event_item as l_event and then
505 attached {E2B_FAILED_VERIFICATION} l_event.data
506 end
507
508 is_failed_execution_event (a_event_item: EVENT_LIST_ITEM_I): BOOLEAN
509 -- Determines if event `a_event_item' is a skipped event
510 do
511 Result := attached {E2B_FAILED_EXECUTION_EVENT} a_event_item
512 end
513
514 feature {NONE} -- Basic operations
515
516 do_default_action (a_row: EV_GRID_ROW)
517 -- <Precursor>
518 local
519 l_stone: STONE
520 do
521 if attached {E2B_VERIFICATION_EVENT} a_row.parent_row_root.data as l_event_item then
522 if attached {E2B_VERIFICATION_ERROR} a_row.data as l_error and then l_error.eiffel_line_number > 0 then
523 create {COMPILED_LINE_STONE} l_stone.make_with_line (l_event_item.context_class, l_error.eiffel_line_number, False)
524 elseif l_event_item.line_number > 0 then
525 create {COMPILED_LINE_STONE} l_stone.make_with_line (l_event_item.context_class, l_event_item.line_number, False)
526 elseif l_event_item.context_feature /= Void then
527 create {FEATURE_STONE} l_stone.make (l_event_item.context_feature.api_feature (l_event_item.context_class.class_id))
528 else
529 create {CLASSC_STONE} l_stone.make (l_event_item.context_class)
530 end
531 elseif attached {E2B_FAILED_EXECUTION_EVENT} a_row.parent_row_root.data as l_event_item then
532 if l_event_item.data.eiffel_feature /= Void then
533 create {FEATURE_STONE} l_stone.make (l_event_item.data.eiffel_feature.api_feature (l_event_item.data.eiffel_class.class_id))
534 elseif l_event_item.data.eiffel_class /= Void then
535 create {CLASSC_STONE} l_stone.make (l_event_item.data.eiffel_class)
536 end
537 end
538 if l_stone /= Void and then l_stone.is_valid then
539 (create {EB_CONTROL_PICK_HANDLER}).launch_stone (l_stone)
540 end
541 end
542
543 populate_event_grid_row_items (a_event_item: EVENT_LIST_ITEM_I; a_row: EV_GRID_ROW)
544 -- Populates a grid row's item on a given row using the event `a_event_item'.
545 --
546 -- `a_event_item': A event to base the creation of a grid row on.
547 -- `a_row': The row to create items on.
548 local
549 l_editor_item: EB_GRID_EDITOR_TOKEN_ITEM
550 l_gen, l_message_gen, l_text_gen: EB_EDITOR_TOKEN_GENERATOR
551 l_lines: LIST [EIFFEL_EDITOR_LINE]
552 l_tip: EB_EDITOR_TOKEN_TOOLTIP
553 l_label: EV_GRID_LABEL_ITEM
554 l_error_list: LIST [EP_ERROR]
555 l_error: EP_ERROR
556 l_row: EV_GRID_ROW
557 l_format: FORMAT_DOUBLE
558 do
559 a_row.set_data (a_event_item)
560 if attached {E2B_FAILED_EXECUTION_EVENT} a_event_item as l_result then
561
562 if l_result.data.eiffel_class /= Void then
563 -- Class location
564 create l_gen.make
565 l_result.data.eiffel_class.append_name (l_gen)
566 l_editor_item := create_clickable_grid_item (l_gen.last_line, True)
567 a_row.set_item (class_column, l_editor_item)
568 end
569 if l_result.data.eiffel_feature /= Void then
570 create l_gen.make
571 l_gen.add_feature_name (l_result.data.eiffel_feature.feature_name_32, l_result.data.eiffel_class)
572 l_editor_item := create_clickable_grid_item (l_gen.last_line, True)
573 a_row.set_item (feature_column, l_editor_item)
574 end
575
576 -- Icon
577 create l_label
578 l_label.set_pixmap (stock_pixmaps.general_error_icon)
579 l_label.set_data ("failed")
580 l_label.disable_full_select
581 a_row.set_item (icon_column, l_label)
582
583 -- Message
584 create l_label.make_with_text (l_result.data.type + ": " + l_result.data.single_line_message)
585 a_row.set_item (info_column, l_label)
586
587 -- Color
588 a_row.set_background_color (failed_color)
589
590 -- Multi-line message
591 if l_result.data.multi_line_message /= Void and then not l_result.data.multi_line_message.is_empty then
592 insert_subrow_for_suggestion (a_row, l_result.data.multi_line_message)
593 end
594
595
596 elseif attached {E2B_VERIFICATION_EVENT} a_event_item as l_result then
597 -- Class location
598 create l_gen.make
599 l_result.context_class.append_name (l_gen)
600 l_editor_item := create_clickable_grid_item (l_gen.last_line, True)
601 a_row.set_item (class_column, l_editor_item)
602
603 -- Feature location
604 if l_result.context_feature /= Void then
605 create l_gen.make
606 l_gen.add_feature_name (l_result.context_feature.feature_name_32, l_result.context_class)
607 l_editor_item := create_clickable_grid_item (l_gen.last_line, True)
608 a_row.set_item (feature_column, l_editor_item)
609 end
610
611 -- Time information
612 create l_format.make (4, 2)
613 create l_label.make_with_text (l_format.formatted (l_result.milliseconds_used))
614 a_row.set_item (time_column, l_label)
615
616 if is_successful_event (a_event_item) then
617 -- Icon
618 create l_label
619 l_label.set_pixmap (stock_pixmaps.general_tick_icon)
620 l_label.set_data ("successful")
621 l_label.disable_full_select
622 a_row.set_item (icon_column, l_label)
623
624 -- Info
625 create l_message_gen.make
626 l_result.single_line_message (l_message_gen)
627 l_editor_item := create_clickable_grid_item (l_message_gen.last_line, True)
628 a_row.set_height (l_editor_item.required_height_for_text_and_component)
629 a_row.set_item (info_column, l_editor_item)
630
631 -- Display
632 a_row.set_background_color (successful_color)
633
634 if attached {E2B_SUCCESSFUL_VERIFICATION} a_event_item.data as l_success then
635 if attached l_success.suggestion and then not l_success.suggestion.is_empty then
636 insert_subrow_for_suggestion (a_row, l_success.suggestion)
637 end
638 if attached l_success.original_errors then
639 across l_success.original_errors as l_errors loop
640 insert_subrow_for_error (a_row, l_errors.item)
641 end
642 a_row.set_background_color (partial_color)
643 end
644 end
645
646 elseif is_failed_event (a_event_item) then
647 -- Icon
648 create l_label
649 l_label.set_pixmap (stock_pixmaps.general_error_icon)
650 l_label.set_data ("failed")
651 l_label.disable_full_select
652 a_row.set_item (icon_column, l_label)
653
654 -- Info
655 create l_message_gen.make
656 l_result.single_line_message (l_message_gen)
657 l_editor_item := create_clickable_grid_item (l_message_gen.last_line, True)
658 a_row.set_height (l_editor_item.required_height_for_text_and_component)
659 a_row.set_item (info_column, l_editor_item)
660
661 -- Display
662 a_row.set_background_color (failed_color)
663
664 if attached {E2B_FAILED_VERIFICATION} a_event_item.data as l_failure then
665 across
666 l_failure.errors as l_errors
667 loop
668 insert_subrow_for_error (a_row, l_errors.item)
669 end
670 end
671
672 -- Position
673 if l_result.line_number > 0 then
674 a_row.set_item (position_column, create {EV_GRID_LABEL_ITEM}.make_with_text (l_result.line_number.out))
675 end
676 end
677 else
678 check False end
679 end
680
681
682 if not is_item_visible (a_row) then
683 a_row.hide
684 end
685 end
686
687 insert_subrow_for_error (a_parent: EV_GRID_ROW; a_error: E2B_VERIFICATION_ERROR)
688 -- Insert a new subrow into `a_parent' for `a_error'.
689 local
690 l_index: INTEGER
691 l_row: EV_GRID_ROW
692 l_text_gen: EB_EDITOR_TOKEN_GENERATOR
693 l_editor_item: EB_GRID_EDITOR_TOKEN_ITEM
694 do
695 l_index := a_parent.subrow_count + 1
696
697 a_parent.insert_subrow (l_index)
698 l_row := a_parent.subrow (l_index)
699 l_row.set_data (a_error)
700
701 l_row.set_item (icon_column, create {EV_GRID_LABEL_ITEM})
702 l_row.set_item (class_column, create {EV_GRID_LABEL_ITEM})
703 l_row.set_item (feature_column, create {EV_GRID_LABEL_ITEM})
704
705 create l_text_gen.make
706 l_text_gen.enable_multiline
707 a_error.multi_line_message (l_text_gen)
708 l_text_gen.add_new_line
709 l_editor_item := create_multiline_clickable_grid_item (l_text_gen.lines, True, False)
710 l_row.set_height (l_editor_item.required_height_for_text_and_component)
711 l_row.set_item (info_column, l_editor_item)
712
713 if a_error.eiffel_line_number > 0 then
714 l_row.set_item (position_column, create {EV_GRID_LABEL_ITEM}.make_with_text (a_error.eiffel_line_number.out))
715 end
716
717 if l_index \\ 2 = 1 then
718 l_row.set_background_color (odd_failed_sub_color)
719 else
720 l_row.set_background_color (even_failed_sub_color)
721 end
722
723 end
724
725 insert_subrow_for_suggestion (a_parent: EV_GRID_ROW; a_suggestion: STRING)
726 -- Insert a new subrow into `a_parent' for `a_error'.
727 local
728 l_index: INTEGER
729 l_row: EV_GRID_ROW
730 l_text_gen: EB_EDITOR_TOKEN_GENERATOR
731 l_editor_item: EB_GRID_EDITOR_TOKEN_ITEM
732 do
733 l_index := a_parent.subrow_count + 1
734
735 a_parent.insert_subrow (l_index)
736 l_row := a_parent.subrow (l_index)
737 l_row.set_data (a_suggestion)
738
739 l_row.set_item (icon_column, create {EV_GRID_LABEL_ITEM})
740 l_row.set_item (class_column, create {EV_GRID_LABEL_ITEM})
741 l_row.set_item (feature_column, create {EV_GRID_LABEL_ITEM})
742 l_row.set_item (info_column, create {EV_GRID_LABEL_ITEM}.make_with_text (a_suggestion))
743
744 l_row.set_background_color (partial_color)
745
746 end
747
748 update_button_titles
749 -- Update button titles with number of events.
750 do
751 successful_button.set_text (successful_count.out + " " + ep_names.tool_button_successful)
752 failed_button.set_text (failed_count.out + " " + ep_names.tool_button_failed)
753 skipped_button.set_text (skipped_count.out + " " + ep_names.tool_button_skipped)
754 end
755
756 find_event_row (a_event_item: EVENT_LIST_ITEM_I): EV_GRID_ROW
757 -- <Precursor>
758 local
759 l_grid: like grid_events
760 l_row: EV_GRID_ROW
761 i: INTEGER
762 do
763 l_grid := grid_events
764 from
765 -- Count backwards as it is more optimal for use in item insertion/removal.
766 i := l_grid.row_count
767 until
768 i = 0
769 loop
770 l_row := l_grid.row (i)
771 if l_row.data = a_event_item then
772 Result := l_row
773 i := 0
774 else
775 i := i - 1
776 end
777 end
778 end
779
780 feature {NONE} -- Clean up
781
782 internal_recycle
783 -- <Precursor>
784 do
785 if is_initialized then
786 if session_manager.is_service_available then
787 if session_data.session_connection.is_connected (Current) then
788 session_data.session_connection.disconnect_events (Current)
789 end
790 end
791 end
792 Precursor {ES_CLICKABLE_EVENT_LIST_TOOL_PANEL_BASE}
793 end
794
795 feature {NONE} -- Constants
796
797 icon_column: INTEGER = 2
798 class_column: INTEGER = 3
799 feature_column: INTEGER = 4
800 info_column: INTEGER = 5
801 position_column: INTEGER = 6
802 time_column: INTEGER = 7
803
804 successful_color: EV_COLOR
805 -- Background color for successful rows
806 once
807 create Result.make_with_rgb (0.8, 1.0, 0.8)
808 end
809
810 failed_color: EV_COLOR
811 -- Background color for successful rows
812 once
813 create Result.make_with_rgb (1.0, 0.7, 0.7)
814 end
815
816 even_failed_sub_color: EV_COLOR
817 -- Background color for successful rows
818 once
819 create Result.make_with_rgb (1.0, 0.9, 0.9)
820 end
821
822 odd_failed_sub_color: EV_COLOR
823 -- Background color for successful rows
824 once
825 create Result.make_with_rgb (1.0, 0.8, 0.8)
826 end
827
828 partial_color: EV_COLOR
829 -- Background color for partial success
830 once
831 create Result.make_with_rgb (1.0, 0.9, 0.4)
832 end
833
834 ep_names: !EP_NAMES
835 -- Shared access to interface names
836 once
837 create Result
838 end
839
840 note
841 copyright: "Copyright (c) 1984-2013, Eiffel Software"
842 license: "GPL version 2 (see http://www.eiffel.com/licensing/gpl.txt)"
843 licensing_options: "http://www.eiffel.com/licensing"
844 copying: "[
845 This file is part of Eiffel Software's Eiffel Development Environment.
846
847 Eiffel Software's Eiffel Development Environment is free
848 software; you can redistribute it and/or modify it under
849 the terms of the GNU General Public License as published
850 by the Free Software Foundation, version 2 of the License
851 (available at the URL listed under "license" above).
852
853 Eiffel Software's Eiffel Development Environment is
854 distributed in the hope that it will be useful, but
855 WITHOUT ANY WARRANTY; without even the implied warranty
856 of MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.
857 See the GNU General Public License for more details.
858
859 You should have received a copy of the GNU General Public
860 License along with Eiffel Software's Eiffel Development
861 Environment; if not, write to the Free Software Foundation,
862 Inc., 51 Franklin St, Fifth Floor, Boston, MA 02110-1301 USA
863 ]"
864 source: "[
865 Eiffel Software
866 5949 Hollister Ave., Goleta, CA 93117 USA
867 Telephone 805-685-1006, Fax 805-685-6869
868 Website http://www.eiffel.com
869 Customer support http://support.eiffel.com
870 ]"
871 end

Properties

Name Value
svn:eol-style native
svn:keywords Author Date ID Revision

  ViewVC Help
Powered by ViewVC 1.1.23