Index of values

act_assoc_valid ar b returns the activation record associated with ar in b.

act_new l act b adds act, paired with l, to the activation record store of b and returns its fresh key.

act_update ar l act b associates ar with the new domain l and the new activation record act in b.

act_valid ar b returns true if ar is in the variable store of b.

add_domains doclist domains adds a list of domains of the remote script urls from the list of docs doclist into the list of domains domains.

build_new_domains body in case body is an Html_file, builds a list of domains of the remote scripts in the body using function add_domains.

build_node_tree doc allocates all of the node references needed to represent doc and returns the association list of these nodes with their appropriate node data.

build_win wn u doc b builds a new window structure with the window name wn.

button_handlers_in_pos wr pos b returns the button handlers associated with the button in position pos in the window referenced by wr in b, along with the corresponding node_ref.

close_doc_request_connections wr b removes any network connection that is waiting for a document to load into the window referenced by wr.

Advance the browser state one step.

continue_w r advance the wrapper state with one step from the running state r.

create_var x r ar b creates (or overwrites) the binding of x with the rslt r in the activation record referenced by ar in b.

del_site_cookie d p k b removes the mapping for of cookie key k for the domain d and path p in b.

del_site_cookies d p ks b removes the mapping of all of the cookies with keys in ks from the cookie store for the domain d and path p in b.

direct_win wr u b directs the window referenced by wr to the URL u.

domain_of_net_connection nc returns a domain of a Net_connection nc.

domain_of_url u defines a domain of url u

fetch_url u wr b performs whatever action is required by the URL u.

filter_one_output oe run_lev levs returns a list containing oe if the level of oe is run_lev or if it's higher than run_lev and is not in the list of currently running levels levs.

filter_outputs os lev new_add_levs filters list of outputs os leaving only those that are at level lev and higher.

filter_outputs_acc os lev new_add_levs acc is an auxiliary function for filter_output.

filter_outputs_one_level oes run_lev levs filters outputs oes leaving only those that are at level run_lev.

An auxiliary function for a function filter_outputs_one_level oes run_lev levs.

find_new_levels all_ls ls new_ls finds levels in the list of levels ls that are not in the list all_ls and put them in a list new_ls.

Finds the position of a key in a mapping.

Generates a fresh act_ref.

Generates a fresh node_ref.

Generates a fresh page_ref.

Generates a fresh win_ref.

get_output p ie produces output of the copy at level label_input ie on input ie.

Return the known expressions at the head of the script queue for the page in the window referenced by wr as browser tasks, and remove them from the page's script queue.

get_site_cookies d p b builds the mapping of cookie keys and values that is specific for the domain d and the path p in b.

get_var x ar b gets the result associated with x in b in the scope defined by ar, if x exists in that scope.

Handling a User_click_button_event.

Handling a User_close_win_event.

Handling an User_input_text_event.

Handling a User_load_in_new_win_event.

Handling a User_load_in_win_event.

Handling a Network_response_event.

http_send d uri body dst b updates the appropriate browser structures and creates the necessary output events for sending a new HTTP request whose response will be received by dst.

insert_levels all_ls ls inserts list of levels ls into a list all_ls assuming that all_ls does not contain any level from list ls.

insert_new_level lev ls inserts a new level lev into a list of levels ls using insert_new_level_acc

insert_new_level_acc lev ls acc is an auxiliary function to insert a new level lev into a list of levels ls, acc is an accumulative list assuming that lev is not in the list ls.

label_input input assigns a security level to an input event input

label_output output assigns a security level to output event output

leq l1 l2 defines whether security level l1 is less or equal than the security level l2

level_of_url u defines a level of url as M(domain)

levels_from_domains domains builds a list of levels from domains domains using levels_from_domains_acc

levels_from_domains_acc domains levels is an auxiliary function that builds a list of levels levels from domains domains

make_new_copies ls lev p makes copies of a state p lev and for every level l in a list ls defines p l := p lev.

net_connection_domain_nth d n b returns the nth req_uri and dst associated with d (based on the order in which they were opened) among the open network connections of b, if one exists.

net_connection_domain_remove_nth d n b removes the nth req_uri and dst associated with d (based on the order in which they were opened) among the open network connections of b, if one exists.

node_assoc_valid dr b returns the node associated with dr in the node store of b.

insert_node parent child pos b inserts child into the children of parent at position pos.

node_new dn b adds dn to the node store of b and returns its fresh key.

Finds the page displaying a node if there is one.

Finds the parent of a node.

Removes a node from its location in its node tree or page.

node_update dr dn b associates dr with the node dn in b.

node_valid dr b returns true if dr is in the node store of b.

open_win wn u b creates a new window in the browser with the window name wn, directed to the URL u.

page_assoc pr b returns the page associated with pr in the page store of b, if one exists.

page_assoc_valid pr b returns the page associated with pr in the page store of b.

page_new p b adds p to the page store of b and returns its fresh key.

page_remove pr b removes pr and its page from from b.

page_update pr p b associates pr with the new page p in b.

page_update_event pr b returns a UI_page_updated_event for the page reference pr.

page_valid pr b returns true if pr is in the page store of b.

page_win pr b returns the win_ref that refers to the unique window that contains the page referenced by pr.

pi label input projection function of input event input to a level label

The implementation of some primitive unary operations.

The implementation of some primitive binary operations.

print_levels ls recursively prints a list of levels ls

print_outputs oes recursively prints a list of outputs oes

process_node_scripts pr dr b prepares for execution all of the scripts that are found among the descendents of dr and have not yet been executed.

proj dom body builds a projection of the body of the receive event body to the domain dom

project_doclist dom doclist doclist' builds a projection of the doc list doclist on the domain dom.

Respond to an incoming event.

receive_w ie w respond to an incoming event ie while being in a waiting state w.

render_page pr b returns the rendered representation of the document in pr.

ro input defines a of additional levels for input input

set_site_cookie d p (k, v) b adds the mapping of the cookie key k to the rslt v for the domain d and path p in b.

set_site_cookies d p pairs b adds all of the key-rslt mappings in pairs to the cookie store for the domain d and path p in b.

set_var x r ar b updates the nearest enclosing binding of x (with the rslt r) under the scope defined by ar in b.

split_queued_exprs qes returns the prefix of qes that are known scripts, as an inner expr list, along with the remainder of qes.

The initial configuration of a browser.

An initial state of the wrapper.

Carries out a single step of executing a script expression.

string_of_domain d transforms a domain d into a string

string_of_level l transforms a security level l to a string

string_of_output output transforms an output output to a string

string_of_string_list ls acc transforms a string list ls to a string acc in a reversed order, e.g.

string_of_url url transforms a url url into a string, if url is empty, transforms to "blank".

textbox_handlers_in_pos wr pos b returns the textbox handlers associated with the textbox in position pos in the window referenced by wr in b, along with the corresponding node_ref.

The obvious coercion from source expressions to internal expresions.

Adds or updates a binding in a mapping.

upd_cookies d uri resp b executes all of the cookie updates requested by resp, which was received in response to a request to d for resource req_uri.

update_pointer lev p ie if p lev is a waiting state, then updates the pointer p with the new state upon consuming the input ie.

update_pointers levs p ie at all the levels in levs moves the pointer p to the producer state corresponding to comsuming input ie.

upper levs ie defines a list of upper security levels for input event ie from the list of all levels levs.

win_assoc wr b returns the win associated with wr in the window store of b, if one exists.

win_assoc_valid wr b returns the win associated with wr in the window store of b.

win_from_user_window uw b returns a reference to the open window in b that corresponds to the domain and number given by uw.

win_from_win_name str b returns the window reference corresponding to the window name str in b.

win_new w b adds w to the window store of b and returns its fresh key.

win_remove wr b removes wr and its window from from b.

win_to_user_window wr b returns the user window description corresponding to the valid window reference wr.

win_update wr w b associates wr with the new window w in b.

win_valid wr b returns true if wr is in the window store of b.