state_viewer_images

add_image(RI,CI,II, AVL, NewAVL, Res, NewRes) :-
    (avl_fetch((RI,CI),AVL,ExistingValue)
    -> add_error(state_viewer_images,
    'Animation function defines two images for (Row,Col):[img1,img2] = ',((RI,CI):[ExistingValue,II])),
    NewAVL = AVL, Res=NewRes
    ; avl_store((RI,CI),AVL,II,NewAVL), Res=[((RI,CI),II)|NewRes]
).

animation_function_possibly_active(xtl) :- !.

animation_function_possibly_active(_) :- b_get_machine_animation_function(_,_),!.

can_react_to_item_drag(Mode,FromX,FromY,ToX,ToY,ImageNr) :-
    current_state_id(CurID),
    get_item_drag_template_and_image(Mode,FromX,FromY,ToX,ToY,TransitionTemplateList,ImageNr),
    get_template(TransitionTemplateList,TransitionTemplate),
    transition(CurID,TransitionTemplate,_ActId,_DestID).

can_react_to_item_right_click(CurID,Mode,X,Y,TransitionTemplateList,Str,TransitionID) :-
    get_right_click_template(Mode,CurID,X,Y,TransitionTemplateList),
    get_template(TransitionTemplateList,Template), % deals with list templates
    transition(CurID,TransitionTerm,TransitionID,DestID),
    match_template(Template,TransitionTerm),
    translate_event_with_src_and_target_id(TransitionTerm,CurID,DestID,Str).

check_anim_function([]) :- !.

check_anim_function([H|_]) :- !,
    (H = (RowCol,_Img), get_pair(RowCol,Row,Col) ->
    (get_int(Row,_),get_int(Col,_) -> true
    ; add_error(state_viewer_images,'Elements of ANIMATION_FUNCTION should be convertible to (INT*INT)*INT: ',H)
    )
    ; H = (Row,ColImg), get_pair(ColImg,Col,_Img) ->
    (get_int(Row,_),get_int(Col,_) -> true
    ; add_error(state_viewer_images,'Elements of ANIMATION_FUNCTION should be convertible to INT*(INT*INT): ',H)
    )
    ; add_error(state_viewer_images,
    'Elements of the ANIMATION_FUNCTION should be of type (INT*INT)*INT: ',H)
).

check_anim_function((A,B)) :- !,
    add_error(state_viewer_images,'ANIMATION_FUNCTION should be a set of pairs, not a pair: ',(A,B)).

check_anim_function(X) :- !,
    add_error(state_viewer_images,'ANIMATION_FUNCTION should be of type (INT*INT) +-> INT (or similar): ',X).

clear_animation_images :- retractall(images(_,_,_)).

compute_prefix(OldPath,NewPath,FilePrefix) :-
    %print(old(OldPath)),nl, print(new(NewPath)),nl,
    split_atom(OldPath,['/'],O1),
    split_atom(NewPath,['/'],N1),
    max_prefix(O1,N1,_CommonPrefix,O2,N2), %print(common(CommonPrefix)),nl,
    maplist(gendotdot,N2,N3),
    append(N3,O2,UpdatePath),
    (UpdatePath=[] -> FilePrefix = ''
    ; append(UpdatePath,[''],U1),
    ajoin_with_sep(U1,'/',FilePrefix)),
    debug_println(9,update_prefix_for_images(FilePrefix)).

convert_2nr_into_tk_label(Nr1,Nr2,Prefix,Label) :-
    number_codes(Nr1,Codes1), number_codes(Nr2,Codes2),
    append([Prefix,Codes1,"_",Codes2],C),
    atom_codes(Label,C).

convert_animation_function(Mode,ImageNumbers,((Row,Col),Res),
    entry(Row,Col,TranslatedRes)) :-
    convert_aux(Mode,ImageNumbers,Res,TranslatedRes).

convert_aux(_Mode,ImageNumbers,Img,image(ImgNr)) :- get_int(Img,ImgNr),ord_member(ImgNr,ImageNumbers),!.

convert_aux(_Mode,_,Str,text(StringLbl)) :- get_int(Str,StrNr),get_animation_string(StrNr,StringLbl),!.

convert_aux(b,_,Value,text(PPValue)) :- translate_value_for_tk_text(Value,PPValue),!.

convert_aux(_,_,Value,text(AtomValue)) :- compound(Value),
    !,
    write_to_codes(Value,VC), atom_codes(AtomValue,VC).

convert_aux(_,_,Value,text(Value)).

convert_nr_into_tk_label(Nr,Prefix,Label) :- number_codes(Nr,Codes),
    append(Prefix,Codes,C),
    atom_codes(Label,C).

convert_tk_path_to_coordinates(TkPath,XCoord,YCoord) :-
    split_last(TkPath,'.',_,NameOfItemClicked),
    atom_codes(NameOfItemClicked,Codes),
    get_suffix(Codes,Rest),
    !,
    split_chars(Rest,"_",[YCC,XCC]), % note: coordinates reversed in label
    number_codes(XCoord,XCC),
    number_codes(YCoord,YCC).

convert_tk_path_to_coordinates(TkPath,_,_) :- format('*** Cannot convert TkPath ~w~n',[TkPath]),fail.

display_animation_function_result(FunctionRes,MinRow,MaxRow,FramesAndItems) :-
    get_min_max_row(FunctionRes,MinRow,MaxRow),
    debug_println(9,visualization_matrix_min_max(MinRow,MaxRow)),
    setup_frames(MinRow,MaxRow,Frames), %debug_println(9,frames(Frames)),
    sort(FunctionRes,SortedFR),
    get_frame_items(SortedFR,Items),
    % print(items(Items)),nl,
    pad_text_frame_items(Items,PItems),
    append(Frames,PItems,FramesAndItems).

end_tag(Stream,T) :- format(Stream,'</~w>~n',[T]).

eval_definition_fun(AnimFunction,BState, FunctionRes) :-
    on_enumeration_warning(
    b_interpreter:b_compute_expression_nowf(AnimFunction,[],BState,FunctionResCl),
    fail),
    %% nl, print('FunctionResult'(FunctionResCl)),nl,
    is_set_value(FunctionResCl,eval_definition_fun),
    try_expand_custom_set_with_catch(FunctionResCl, ExpCl, eval_definition_fun),
    (translate_to_ints(ExpCl, FunctionRes)
    -> true /* already translate to ints so that override will work properly */
    ; check_anim_function(ExpCl),fail
) % ,print('fres'(FunctionRes)),nl
.

eval_definition_funs([],_,[]).

eval_definition_funs([anim_fun(_Nr,AnimFunction1)|T],BState,Result) :-
    eval_definition_fun(AnimFunction1, BState, FunctionRes1),
    eval_definition_funs(T,BState,FunctionRes0),
    override_anim_fun(FunctionRes1,FunctionRes0,Result).

eval_parameter(LocalVars,_State,Parameter,Result) :-
    get_texpr_id(Parameter,PID),
    member(LV,LocalVars), get_texpr_id(LV,PID),
    !,
    Result = _.

eval_parameter(_LocalVars,State,Parameter,Result) :-
    b_compute_expression_nowf(Parameter,[],State,Result).

evaluate_animation_function(xtl,State,FunctionRes) :- !,
    xtl_animation_function_result(State,FunctionRes).

evaluate_animation_function(_,State,FunctionRes) :- % Mode will be 'b'
    state_corresponds_to_fully_setup_b_machine(State,BState),
    findall(anim_fun(Nr,AF),b_get_machine_animation_function(AF,Nr),AnimFuns),
    AnimFuns \= [],
    sort(AnimFuns,SAnimFuns),
    %print(animation_images(ImageList)),
    % print('Animation Function: '),
    % translate:print_bexpr(SAnimFuns),
    eval_definition_funs(SAnimFuns, BState, FunctionRes).

execute_rest([],Res) :- !, Res=[].

execute_rest([H|T],[TransitionID|TT]) :- !,
    current_state_id(CurID), %print(try_auto_play(CurID,H)),nl,
    tcltk_interface:compute_all_transitions_if_necessary,
    current_state_id(CurID),
    tcltk_interface:tcltk_perform_action(CurID,H,TransitionID,_NewID), %print(perf(H,_NewID)),nl,
    execute_rest(T,TT).

execute_rest(T,[]) :- format('~n*** Cannot execute rest of transition template ~w~n',[T]).

flatten_img_list([],[]).

flatten_img_list([img(Nr,ImgFilename,Lbl)|T],[Lbl,ImgFilename|FT]) :-
    assert(images(Nr,ImgFilename,Lbl)), flatten_img_list(T,FT).

gen_spaces(Nr,R) :- Nr<1,R=[]. % 34 -> '

gen_spaces(Nr,[32|T]) :- N1 is Nr-1, gen_spaces(N1,T).

gendotdot(_,'..').

get_HEAD_revision_info(ReferenceFile,GitOutputText) :-
    get_parent_directory(ReferenceFile,CurWorkingDir),
    run_git_command(['rev-parse','HEAD'],CurWorkingDir,GitOutputText).

get_animation_expression_label_and_value(StateID,S1,S2) :- b_or_z_mode,
    b_get_machine_animation_expression(AExpr),
    visited_expression(StateID,State),
    state_corresponds_to_fully_setup_b_machine(State,BState),
    b_interpreter:b_compute_expression_nowf(AExpr,[],BState,AValue),
    translate_bexpression(AExpr,S1),
    translate_bvalue(AValue,S2).

get_animation_image_and_label(Mode,Nr,ImgFilename,Lbl) :-
    get_animation_image_in_mode(Mode,Nr,ImgFilename),
    convert_nr_into_tk_label(Nr,"IMG",Lbl).

get_animation_image_grid(ID,Matrix,MinRow,MaxRow,MinCol,MaxCol) :-
    animation_mode(Mode),
    animation_function_possibly_active(Mode), % avoid expanding state; can be expensive
    visited_expression(ID,State),
    evaluate_animation_function(Mode,State,FunctionRes),
    get_min_max_row(FunctionRes,MinRow,MaxRow),
    get_min_max_col(FunctionRes,MinCol,MaxCol),
    get_animation_image_numbers(ImageNumbers),
    maplist(convert_animation_function(Mode,ImageNumbers),FunctionRes,Matrix).

get_animation_image_in_mode(xtl,Nr,S) :- !, xtl_animation_image(Nr,S).

get_animation_image_in_mode(b,Nr,S) :- !, get_animation_image(Nr,S).

get_animation_image_in_mode(csp_and_b,Nr,S) :- get_animation_image(Nr,S).

get_animation_image_numbers(SList) :-
    animation_mode(Mode),
    findall( Nr, get_animation_image_in_mode(Mode,Nr,_File), List), % TO DO: also get animation strings
    sort(List,SList).

get_animation_images(SList) :-
    animation_mode(Mode),
    findall( image_file(Nr,File), get_animation_image_in_mode(Mode,Nr,File), List),
    sort(List,SList).

get_animation_images(Mode,Res) :- clear_animation_images,
    findall( img(Nr,ImgFilename,Lbl), get_animation_image_and_label(Mode,Nr,ImgFilename,Lbl), List),
    flatten_img_list(List,Res).

get_animation_string(Nr,S) :- b_or_z_mode,
    number_codes(Nr,TailCodes),
    /* ANIMATION_STR */
    atom_codes(Def_Name,[65,78,73,77,65,84,73,79,78,95,83,84,82|TailCodes]),
    b_get_definition_string_from_machine(Def_Name,S).

get_b_template(b(E,subst,_),LocalVars,State,Template) :- get_b_template_aux(E,LocalVars,State,Template).

get_b_template_aux(any(Paras,_Pred,Body),LocalVars,State,Template) :- !,
    append(Paras,LocalVars,LV2),
    get_b_template(Body,LV2,State,Template).

get_b_template_aux(let(Paras,_Pred,Body),LocalVars,State,Template) :- !,
    append(Paras,LocalVars,LV2),
    get_b_template(Body,LV2,State,Template).

get_b_template_aux(var(Paras,Body),LocalVars,State,Template) :- !,
    append(Paras,LocalVars,LV2),
    get_b_template(Body,LV2,State,Template).

get_b_template_aux(choice(Options),LocalVars,State,Template) :- !,
    member(A,Options),
    get_b_template(A,LocalVars,State,Template).

get_b_template_aux(if(Options),LocalVars,State,Template) :- !,
    get_b_template_for_if(Options,LocalVars,State,Template).

get_b_template_aux(operation_call(TOpID,_Result,Parameters),LocalVars,State,Template) :- !,
    def_get_texpr_id(TOpID,op(OpID)),
    % TO DO: deal with Result
    maplist(eval_parameter(LocalVars,State),Parameters,TemplateArgs),
    Template =.. [OpID|TemplateArgs].

get_b_template_aux(Subst,_LocalVars,_State,_) :-
    add_error('ANIMATION_RIGHT_CLICK','Uncovered substitution: ',Subst),fail.

get_b_template_for(CurID,Subst,LV,Template) :-
    visited_expression(CurID,State),
    state_corresponds_to_set_up_constants(State,BState),
    % expand_const_and_vars_to_full_store
    get_b_template(Subst,LV,BState,Template).

get_b_template_for_if([b(if_elsif(Test,Body),_,_)|_], LocalVars,State,Template) :-
    b_test_boolean_expression_wf(Test,[],State),!,
    get_b_template(Body,LocalVars,State,Template).

get_b_template_for_if([_|T],LV,State,Template) :- get_b_template_for_if(T,LV,State,Template).

get_file_revision_info(File,GitOutputText) :-
    get_parent_directory(File,CurWorkingDir),
    run_git_command(['ls-files','-s',File],CurWorkingDir,GitOutputText).

get_frame_items([],[]).

get_frame_items([((Row,Col),Img)|T],[ItemLbl,FrameLbl,ImageLbl|TR]) :-
    convert_nr_into_tk_label(Row,"frame",FrameLbl),
    (get_int(Img,ImgNr),images(ImgNr,_,ImageLbl)
    -> convert_2nr_into_tk_label(Row,Col,"item",ItemLbl)
    ; convert_2nr_into_tk_label(Row,Col,"text",ItemLbl),
    (get_int(Img,ImgNr),get_animation_string(ImgNr,ImageLbl) -> true
    ; translate_value_for_tk_text(Img,ImageLbl)
    )
    ),
    get_frame_items(T,TR).

get_int(Nr,R) :- number(Nr),!,R=Nr.

get_int(int(R),R).

get_int(fd(R,_Name),R).

get_int(pred_true /* bool_true */,1).

get_int(pred_false /* bool_false */,0).

get_item_drag_template_and_image(xtl,ColFromX,RowFromY,ToX,ToY,TransitionTemplate,ImageNr) :- !,
    xtl_animation_image_click_transition(RowFromY,ColFromX,ToY,ToX,TransitionTemplate,ImageNr).

get_item_drag_template_and_image(b,FromX,FromY,ToX,ToY,Template,1000) :-
    % TO DO: provide a way to return image number
    Def_Name = 'ANIMATION_CLICK',
    b_get_definition(Def_Name,substitution,ARGS,RawSubst,_Deps),
    arg(1,RawSubst,Pos),
    (ARGS = [_,_,_,_] -> true % we need four arguments
    ; add_warning(state_viewer_images,'DEFINITION needs four arguments: ','ANIMATION_CLICK',Pos),fail
    ),
    temporary_set_preference(allow_local_operation_calls,true,CHNG),
    Scope = [prob_ids(visible),operation_bodies], % do not include variables; otherwise clash warnings; variables already included in operation_bodies
    type_with_errors(definition(Pos,'ANIMATION_CLICK',
    [integer(Pos,FromX),integer(Pos,FromY),integer(Pos,ToX),integer(Pos,ToY)]),Scope,subst,Typed),
    reset_temporary_preference(allow_local_operation_calls,CHNG),
    State = [], % TO DO: get full state like for right click
    get_b_template(Typed,[],State,Template).

get_min_max_col([((_Row,Col),_Img)|T],Min,Max) :- !,
    number(Col), % this is already in a format for Tcl/Tk; not int(.)
    get_min_max_col2(T,Col,Col,Min,Max).

get_min_max_col2([],Min,Max,Min,Max).

get_min_max_col2([((_Row,Col),_Img)|T],Min,Max,MinR,MaxR) :-
    (Col<Min -> Min1=Col ; Min1=Min),
    (Col>Max -> Max1=Col ; Max1=Max),
    get_min_max_col2(T,Min1,Max1,MinR,MaxR).

get_min_max_row([((Row,_Col),_Img)|T],Min,Max) :- !,
    number(Row), % this is already in a format for Tcl/Tk; not int(.)
    get_min_max_row2(T,Row,Row,Min,Max).

get_min_max_row([],_,_) :- !,
    print('**** Empty ANIMATION_FUNCTION result'),nl, fail.

get_min_max_row(Res,_,_) :-
    add_error(state_viewer_images,
    'Unknown Format for ANIMATION_FUNCTION result, must be of type INT or (INT*INT)+->INT',Res),
    fail.

get_min_max_row2([],Min,Max,Min,Max).

get_min_max_row2([((Row,_Col),_Img)|T],Min,Max,MinR,MaxR) :-
    (Row<Min -> Min1=Row ; Min1=Min),
    (Row>Max -> Max1=Row ; Max1=Max),
    get_min_max_row2(T,Min1,Max1,MinR,MaxR).

get_pair((A,B),A,B).

get_pair(avl_set(node((int(1),A),true,1,empty,node((int(2),B),true,0,empty,empty))),A,B). % in TLA: <> sometimes translated as sequence

get_react_to_item_right_click_options(CurID,XCoord,YCoord,Names) :-
    animation_mode(M),
    findall(Name,can_react_to_item_right_click(CurID,M,XCoord,YCoord,_,Name,_),Names).

get_right_click_template(xtl,_,ColX,RowY,Template) :-
    xtl_animation_image_right_click_transition(RowY,ColX,Template).

get_right_click_template(b,CurID,X,Y,Template) :-
    Def_Name = 'ANIMATION_RIGHT_CLICK',
    b_get_definition(Def_Name,substitution,[_,_],RawSubst,_Deps),
    arg(1,RawSubst,Pos),
    temporary_set_preference(allow_local_operation_calls,true,CHNG),
    Scope = [prob_ids(visible),operation_bodies], % do not include variables; otherwise clash warnings
    % type definition call:
    type_with_errors(definition(Pos,'ANIMATION_RIGHT_CLICK',[integer(Pos,X),integer(Pos,Y)]),Scope,subst,Typed),
    reset_temporary_preference(allow_local_operation_calls,CHNG),
    get_b_template_for(CurID,Typed,[],Template).

get_suffix(Codes,Rest) :- append("item",Rest,Codes),!.

get_suffix(Codes,Rest) :- append("text",Rest,Codes),!.

get_suffix(Codes,Rest) :- append("frame",Rest,Codes),!.

get_template([H|_],Template) :- !, % in XTL mode we allow lists of actions
    Template=H.

get_template(Template,Template). % in B,TLA,Z,... mode we only execute a single event

get_template_rest([_|T],T).

html_footer(Stream) :-
    format(Stream,'</body>~n</html>~n',[]).

html_header(Stream,Border) :-
    format(Stream,'<html>~n<head>~n<style>~ntable, th, td {~n',[]),
    (Border=true -> format(Stream,' border: 1px solid black;~n',[]) ; true),
    format(Stream,' border-collapse: collapse;~n}~nth, td {~n padding: 0px;~n}~n</style>~n</head>~n<body>',[]).

html_image(image(ImgNr),Stream,Mode,FilePrefix) :- get_animation_image_in_mode(Mode,ImgNr,File),!,
    ((FilePrefix='' ; is_absolute_path(File))
    -> format(Stream,' <th><img src="~w"></th>~n',[File])
    ; format(Stream,' <th><img src="~w~w"></th>~n',[FilePrefix,File])
).

html_image(text(T),Stream,_,_) :- !,
    format(Stream,' <th><tt>~w</tt></th>~n',[T]).

html_image(T,Stream,_,_) :-
    format(Stream,' <th>ERROR: ~w</th>~n',[T]).

html_info(Stream,A,SpecFile) :-
    format(Stream,'<h2>Information</h2>~n<ul>~n',[]),
    datime(datime(Year,Month,Day,Hour,Min,_Sec)),
    format(Stream,' <li>Trace generated on ~w.~w.~w at ~w:~w</li>~n',[Day,Month,Year,Hour,Min]),
    length(A,Len),
    format(Stream,' <li>Trace length: ~w</li>~n',[Len]),
    animation_mode(Mode),
    format(Stream,' <li>Specification file (~w): ~w</li>~n',[Mode,SpecFile]),
    ((SpecFile \= unknown,get_file_revision_info(SpecFile,GitRev))
    -> format(Stream,' <li>Git revision of file: ~s</li>~n',[GitRev]) ; true),
    ((SpecFile \= unknown,get_HEAD_revision_info(SpecFile,GitHeadRev))
    -> format(Stream,' <li>Git revision of repository HEAD: ~s</li>~n',[GitHeadRev]) ; true),
    version_str(V), revision(R), lastchangeddate(LD),
    format(Stream,' <li>ProB version: ~w</li>~n',[V]),
    format(Stream,' <li>ProB revision: ~w (~w)</li>~n',[R, LD]),
    format(Stream,'</ul>~n',[]).

html_print([],Stream,_,_,_FilePrefix) :- end_tag(Stream,tr).

html_print([entry(Row,_Col,Img)|T],Stream,LastRow,Mode,FilePrefix) :-
    (Row>LastRow -> end_tag(Stream,tr),start_tag(Stream,tr) ; true),
    % TO DO: insert empty cells when we jump over Columns
    html_image(Img,Stream,Mode,FilePrefix),
    html_print(T,Stream,Row,Mode,FilePrefix).

html_print_action(Stream,Action,PreviousID,_ID,MaxLevel) :-
    MaxLevel > 0, PreviousID \= none,
    get_operation_name(Action,OpName),
    !,
    % print operation guards up to MaxLevel nesting, TODO: use parameter values for this action
    (html_debug_operation_for_stateid(Stream,OpName,PreviousID,MaxLevel) % fails for INITIALISATION, SETUP_CONSTANTS
    -> true
    ; true). %add_internal_error('Failed: ',html_debug_operation_for_stateid(OpName,ID,MaxLevel))).

html_print_action(_,_,_,_,_).

html_print_animation_expression(Stream,StateID) :-
    get_animation_expression_label_and_value(StateID,S1,S2),
    format(Stream,'~w=~w~n',[S1,S2]).

html_print_animation_expression(_,_).

html_print_animation_image_grid(Stream,ID,FilePrefix) :-
    get_animation_image_grid(ID,Matrix,MinRow,_MaxRow,_MinCol,_MaxCol),
    sort(Matrix,SortedMatrix),
    start_tag(Stream,table),
    start_tag(Stream,tr),animation_mode(Mode),
    html_print(SortedMatrix,Stream,MinRow,Mode,FilePrefix),
    end_tag(Stream,table).

html_print_history(File) :- html_print_history(File,3).

html_print_history(File,MaxOpDebugLevel) :-
    get_state_id_trace([root|StateIds]),
    get_action_term_trace(RAT), reverse(RAT,Actions),
    % TO DO: adapt path of images so that they work in File
    (currently_opened_file(SpecFile), atom(SpecFile)
    -> get_parent_directory(SpecFile,SParent),
    absolute_file_name(SParent, SAbsParent), %, [relative_to(Directory)]),
    get_parent_directory(File,TParent),
    absolute_file_name(TParent, TAbsParent), %, [relative_to(Directory)]),
    compute_prefix(SAbsParent,TAbsParent,FilePrefix)
    ; SpecFile=unknown, FilePrefix='.'),
    open(File,write,Stream,[encoding(utf8)]),
    html_header(Stream,true),
    html_info(Stream,Actions,SpecFile),
    html_print_history2(Stream,1,Actions,StateIds,none,FilePrefix,MaxOpDebugLevel),
    html_footer(Stream),
    close(Stream).

html_print_history2(_,_,[],[],_,_,_).

html_print_history2(Stream,_,[],[ID|_],_,FilePrefix,_) :-
    html_print_state(Stream,ID,FilePrefix).

html_print_history2(Stream,StepNr,[Action|AT],[ID|T],PreviousID,FilePrefix,MaxOpDebugLevel) :-
    translate_event(Action,AS),
    format(Stream,'~n~n<h2>~w. ~w</h2>~n',[StepNr,AS]), flush_output(Stream),
    html_print_action(Stream,Action,PreviousID,ID,MaxOpDebugLevel),
    html_print_state(Stream,ID,FilePrefix),
    S1 is StepNr+1,
    html_print_history2(Stream,S1,AT,T,ID,FilePrefix,MaxOpDebugLevel).

html_print_state(Stream,ID,FilePrefix) :-
    (html_print_animation_image_grid(Stream,ID,FilePrefix)
    -> true ; format(Stream,'No visualisation available for state id ~w~n',[ID])),
    html_print_animation_expression(Stream,ID).

is_text_type(ItemLabel) :- atom_codes(ItemLabel,Codes), append("text",_,Codes).

l_translate([],AVL,AVL,Res,Res).

l_translate([H|T],AVL,NewAVL,Res,NewRes) :- translate_element(H,AVL,NewAVL1,Res,NewRes1),
    l_translate(T,NewAVL1,NewAVL,NewRes1,NewRes).

longest_text([],R,R).

longest_text([ItemLabel,_Frame,Text|TR],Acc,R) :-
    is_text_type(ItemLabel),!,
    atom_length(Text,Len),
    (Len>Acc -> NAcc = Len ; NAcc=Acc),
    longest_text(TR,NAcc,R).

longest_text([_,_,_|TR],Acc,R) :- longest_text(TR,Acc,R).

match_template(T,T) :- !.

match_template(T,'-->'(ActionWoResults,_Results)) :- !, match_template(T,ActionWoResults).

match_template(Template,Action) :-
    atom(Template), % with get_preference(show_eventb_any_arguments,true) we have extra arguments
    get_operation_name(Action,Template).

max_prefix([H|T],[H|T2],[H|PT],Suffix1,Suffix2) :- !,
    max_prefix(T,T2,PT,Suffix1,Suffix2).

max_prefix(S1,S2,[],S1,S2).

override_anim_fun([],Fun2,Res) :- !, Res=Fun2.

override_anim_fun(int(_),Fun2,Res) :- !, Res=Fun2.

override_anim_fun([((RowT,Col),Img)|T],Fun2,Res) :- !,
    (member(((RowT,Col),_),Fun2)
    -> Res = ResT % we use version from Fun2
    ; Res = [((RowT,Col),Img)|ResT]
    ), override_anim_fun(T,Fun2,ResT).

override_anim_fun(X,F,R) :-
    add_error(state_viewer_images,'Unknown Format for ANIMATION_FUNCTION_DEFAULT', X),
    R=F.

pad_text_frame_items(FrameItems,NewFrameItems) :- b_or_z_mode,
    (b_get_true_expression_definition('ANIMATION_STR_JUSTIFY_LEFT') ;
    b_get_true_expression_definition('ANIMATION_STR_JUSTIFY_RIGHT') ),
    longest_text(FrameItems,0,Len),
    Len>0,
    !,
    %print(longest(Len)),nl,
    pad_text_frame_items_to(FrameItems,Len,NewFrameItems).

pad_text_frame_items(F,F).

pad_text_frame_items_to([],_,[]).

pad_text_frame_items_to([ItemLabel,Frame,Text|TR],Len,[ItemLabel,Frame,NewText|NTR]) :-
    (is_text_type(ItemLabel)
    -> atom_codes(Text,Codes),
    length(Codes,TLen),
    AdditionalSpaces is Len-TLen, gen_spaces(AdditionalSpaces,AS),
    (b_get_true_expression_definition('ANIMATION_STR_JUSTIFY_RIGHT')
    -> append(AS,Codes,NewCodes)
    ; append(Codes,AS,NewCodes) % 34 -> ' 39 ->
    ),
    atom_codes(NewText,NewCodes)
    ; NewText=Text),
    pad_text_frame_items_to(TR,Len,NTR).