From 2aa64dcace09aa8691104ee7c7c1f55e890bb17c Mon Sep 17 00:00:00 2001 From: Michael Herzberg Date: Thu, 25 Jul 2019 16:27:35 +0100 Subject: [PATCH] Use prefixed document variable. --- Core_DOM/tests/Document_adoptNode.thy | 24 +++-- Core_DOM/tests/Document_getElementById.thy | 116 ++++++++++----------- Core_DOM/tests/Node_insertBefore.thy | 36 ++++--- Core_DOM/tests/Node_removeChild.thy | 24 +++-- 4 files changed, 103 insertions(+), 97 deletions(-) diff --git a/Core_DOM/tests/Document_adoptNode.thy b/Core_DOM/tests/Document_adoptNode.thy index 3135aa5..2614008 100644 --- a/Core_DOM/tests/Document_adoptNode.thy +++ b/Core_DOM/tests/Document_adoptNode.thy @@ -27,8 +27,10 @@ * SPDX-License-Identifier: BSD-2-Clause ***********************************************************************************) -section\Testing adoptNode\ -text\This theory contains the test cases for adoptNode.\ +(* This file is automatically generated, please do not modify! *) + +section\Testing Core_DOM\ +text\This theory contains the test cases for Core_DOM.\ theory Document_adoptNode imports @@ -52,30 +54,30 @@ definition Document_adoptNode_heap :: heap⇩f⇩i⇩n⇩a⇩l where (cast (element_ptr.Ref 11), cast (create_element_obj ''script'' [cast (character_data_ptr.Ref 3)] fmempty None)), (cast (character_data_ptr.Ref 3), cast (create_character_data_obj ''%3C%3Cscript%3E%3E''))]" -definition document :: "(unit, unit, unit, unit, unit, unit) object_ptr option" where "document = Some (cast (document_ptr.Ref 1))" +definition Document_adoptNode_document :: "(unit, unit, unit, unit, unit, unit) object_ptr option" where "Document_adoptNode_document = Some (cast (document_ptr.Ref 1))" text \"Adopting an Element called 'x<' should work."\ lemma "test (do { - tmp0 \ document . getElementsByTagName(''x<''); + tmp0 \ Document_adoptNode_document . getElementsByTagName(''x<''); y \ return (tmp0 ! 0); child \ y . firstChild; tmp1 \ y . parentNode; - tmp2 \ document . body; + tmp2 \ Document_adoptNode_document . body; assert_equals(tmp1, tmp2); tmp3 \ y . ownerDocument; - assert_equals(tmp3, document); - tmp4 \ document . adoptNode(y); + assert_equals(tmp3, Document_adoptNode_document); + tmp4 \ Document_adoptNode_document . adoptNode(y); assert_equals(tmp4, y); tmp5 \ y . parentNode; assert_equals(tmp5, None); tmp6 \ y . firstChild; assert_equals(tmp6, child); tmp7 \ y . ownerDocument; - assert_equals(tmp7, document); + assert_equals(tmp7, Document_adoptNode_document); tmp8 \ child . ownerDocument; - assert_equals(tmp8, document); + assert_equals(tmp8, Document_adoptNode_document); doc \ createDocument(None, None, None); tmp9 \ doc . adoptNode(y); assert_equals(tmp9, y); @@ -94,8 +96,8 @@ lemma "test (do { text \"Adopting an Element called ':good:times:' should work."\ lemma "test (do { - x \ document . createElement('':good:times:''); - tmp0 \ document . adoptNode(x); + x \ Document_adoptNode_document . createElement('':good:times:''); + tmp0 \ Document_adoptNode_document . adoptNode(x); assert_equals(tmp0, x); doc \ createDocument(None, None, None); tmp1 \ doc . adoptNode(x); diff --git a/Core_DOM/tests/Document_getElementById.thy b/Core_DOM/tests/Document_getElementById.thy index f816d05..939f11e 100644 --- a/Core_DOM/tests/Document_getElementById.thy +++ b/Core_DOM/tests/Document_getElementById.thy @@ -27,8 +27,10 @@ * SPDX-License-Identifier: BSD-2-Clause ***********************************************************************************) -section\Testing getElementById\ -text\This theory contains the test cases for getElementById.\ +(* This file is automatically generated, please do not modify! *) + +section\Testing Core_DOM\ +text\This theory contains the test cases for Core_DOM.\ theory Document_getElementById imports @@ -60,23 +62,23 @@ definition Document_getElementById_heap :: heap⇩f⇩i⇩n⇩a⇩l where (cast (element_ptr.Ref 19), cast (create_element_obj ''script'' [cast (character_data_ptr.Ref 3)] fmempty None)), (cast (character_data_ptr.Ref 3), cast (create_character_data_obj ''%3C%3Cscript%3E%3E''))]" -definition document :: "(unit, unit, unit, unit, unit, unit) object_ptr option" where "document = Some (cast (document_ptr.Ref 1))" +definition Document_getElementById_document :: "(unit, unit, unit, unit, unit, unit) object_ptr option" where "Document_getElementById_document = Some (cast (document_ptr.Ref 1))" text \"Document.getElementById with a script-inserted element"\ lemma "test (do { - gBody \ document . body; + gBody \ Document_getElementById_document . body; TEST_ID \ return ''test2''; - test \ document . createElement(''div''); + test \ Document_getElementById_document . createElement(''div''); test . setAttribute(''id'', TEST_ID); gBody . appendChild(test); - result \ document . getElementById(TEST_ID); + result \ Document_getElementById_document . getElementById(TEST_ID); assert_not_equals(result, None, ''should not be null.''); tmp0 \ result . tagName; assert_equals(tmp0, ''div'', ''should have appended element's tag name''); gBody . removeChild(test); - removed \ document . getElementById(TEST_ID); + removed \ Document_getElementById_document . getElementById(TEST_ID); assert_equals(removed, None, ''should not get removed element.'') }) Document_getElementById_heap" by eval @@ -85,19 +87,19 @@ lemma "test (do { text \"update `id` attribute via setAttribute/removeAttribute"\ lemma "test (do { - gBody \ document . body; + gBody \ Document_getElementById_document . body; TEST_ID \ return ''test3''; - test \ document . createElement(''div''); + test \ Document_getElementById_document . createElement(''div''); test . setAttribute(''id'', TEST_ID); gBody . appendChild(test); UPDATED_ID \ return ''test3-updated''; test . setAttribute(''id'', UPDATED_ID); - e \ document . getElementById(UPDATED_ID); + e \ Document_getElementById_document . getElementById(UPDATED_ID); assert_equals(e, test, ''should get the element with id.''); - old \ document . getElementById(TEST_ID); + old \ Document_getElementById_document . getElementById(TEST_ID); assert_equals(old, None, ''shouldn't get the element by the old id.''); test . removeAttribute(''id''); - e2 \ document . getElementById(UPDATED_ID); + e2 \ Document_getElementById_document . getElementById(UPDATED_ID); assert_equals(e2, None, ''should return null when the passed id is none in document.'') }) Document_getElementById_heap" by eval @@ -107,13 +109,13 @@ text \"Ensure that the id attribute only affects elements present in a doc lemma "test (do { TEST_ID \ return ''test4-should-not-exist''; - e \ document . createElement(''div''); + e \ Document_getElementById_document . createElement(''div''); e . setAttribute(''id'', TEST_ID); - tmp0 \ document . getElementById(TEST_ID); + tmp0 \ Document_getElementById_document . getElementById(TEST_ID); assert_equals(tmp0, None, ''should be null''); - tmp1 \ document . body; + tmp1 \ Document_getElementById_document . body; tmp1 . appendChild(e); - tmp2 \ document . getElementById(TEST_ID); + tmp2 \ Document_getElementById_document . getElementById(TEST_ID); assert_equals(tmp2, e, ''should be the appended element'') }) Document_getElementById_heap" by eval @@ -122,23 +124,23 @@ lemma "test (do { text \"in tree order, within the context object's tree"\ lemma "test (do { - gBody \ document . body; + gBody \ Document_getElementById_document . body; TEST_ID \ return ''test5''; - target \ document . getElementById(TEST_ID); + target \ Document_getElementById_document . getElementById(TEST_ID); assert_not_equals(target, None, ''should not be null''); tmp0 \ target . getAttribute(''data-name''); assert_equals(tmp0, ''1st'', ''should return the 1st''); - element4 \ document . createElement(''div''); + element4 \ Document_getElementById_document . createElement(''div''); element4 . setAttribute(''id'', TEST_ID); element4 . setAttribute(''data-name'', ''4th''); gBody . appendChild(element4); - target2 \ document . getElementById(TEST_ID); + target2 \ Document_getElementById_document . getElementById(TEST_ID); assert_not_equals(target2, None, ''should not be null''); tmp1 \ target2 . getAttribute(''data-name''); assert_equals(tmp1, ''1st'', ''should be the 1st''); tmp2 \ target2 . parentNode; tmp2 . removeChild(target2); - target3 \ document . getElementById(TEST_ID); + target3 \ Document_getElementById_document . getElementById(TEST_ID); assert_not_equals(target3, None, ''should not be null''); tmp3 \ target3 . getAttribute(''data-name''); assert_equals(tmp3, ''4th'', ''should be the 4th'') @@ -146,17 +148,15 @@ lemma "test (do { by eval -text \"Modern browsers optimize this method with using internal id cache. - This test checks that their optimization should effect only append to - `Document`, not append to `Node`."\ +text \"Modern browsers optimize this method with using internal id cache. This test checks that their optimization should effect only append to `Document`, not append to `Node`."\ lemma "test (do { TEST_ID \ return ''test6''; - s \ document . createElement(''div''); + s \ Document_getElementById_document . createElement(''div''); s . setAttribute(''id'', TEST_ID); - tmp0 \ document . createElement(''div''); + tmp0 \ Document_getElementById_document . createElement(''div''); tmp0 . appendChild(s); - tmp1 \ document . getElementById(TEST_ID); + tmp1 \ Document_getElementById_document . getElementById(TEST_ID); assert_equals(tmp1, None, ''should be null'') }) Document_getElementById_heap" by eval @@ -165,17 +165,17 @@ lemma "test (do { text \"changing attribute's value via `Attr` gotten from `Element.attribute`."\ lemma "test (do { - gBody \ document . body; + gBody \ Document_getElementById_document . body; TEST_ID \ return ''test7''; - element \ document . createElement(''div''); + element \ Document_getElementById_document . createElement(''div''); element . setAttribute(''id'', TEST_ID); gBody . appendChild(element); - target \ document . getElementById(TEST_ID); + target \ Document_getElementById_document . getElementById(TEST_ID); assert_equals(target, element, ''should return the element before changing the value''); element . setAttribute(''id'', (TEST_ID @ ''-updated'')); - target2 \ document . getElementById(TEST_ID); + target2 \ Document_getElementById_document . getElementById(TEST_ID); assert_equals(target2, None, ''should return null after updated id via Attr.value''); - target3 \ document . getElementById((TEST_ID @ ''-updated'')); + target3 \ Document_getElementById_document . getElementById((TEST_ID @ ''-updated'')); assert_equals(target3, element, ''should be equal to the updated element.'') }) Document_getElementById_heap" by eval @@ -184,19 +184,19 @@ lemma "test (do { text \"update `id` attribute via element.id"\ lemma "test (do { - gBody \ document . body; + gBody \ Document_getElementById_document . body; TEST_ID \ return ''test12''; - test \ document . createElement(''div''); + test \ Document_getElementById_document . createElement(''div''); test . setAttribute(''id'', TEST_ID); gBody . appendChild(test); UPDATED_ID \ return (TEST_ID @ ''-updated''); test . setAttribute(''id'', UPDATED_ID); - e \ document . getElementById(UPDATED_ID); + e \ Document_getElementById_document . getElementById(UPDATED_ID); assert_equals(e, test, ''should get the element with id.''); - old \ document . getElementById(TEST_ID); + old \ Document_getElementById_document . getElementById(TEST_ID); assert_equals(old, None, ''shouldn't get the element by the old id.''); test . setAttribute(''id'', ''''); - e2 \ document . getElementById(UPDATED_ID); + e2 \ Document_getElementById_document . getElementById(UPDATED_ID); assert_equals(e2, None, ''should return null when the passed id is none in document.'') }) Document_getElementById_heap" by eval @@ -205,33 +205,33 @@ lemma "test (do { text \"where insertion order and tree order don't match"\ lemma "test (do { - gBody \ document . body; + gBody \ Document_getElementById_document . body; TEST_ID \ return ''test13''; - container \ document . createElement(''div''); + container \ Document_getElementById_document . createElement(''div''); container . setAttribute(''id'', (TEST_ID @ ''-fixture'')); gBody . appendChild(container); - element1 \ document . createElement(''div''); + element1 \ Document_getElementById_document . createElement(''div''); element1 . setAttribute(''id'', TEST_ID); - element2 \ document . createElement(''div''); + element2 \ Document_getElementById_document . createElement(''div''); element2 . setAttribute(''id'', TEST_ID); - element3 \ document . createElement(''div''); + element3 \ Document_getElementById_document . createElement(''div''); element3 . setAttribute(''id'', TEST_ID); - element4 \ document . createElement(''div''); + element4 \ Document_getElementById_document . createElement(''div''); element4 . setAttribute(''id'', TEST_ID); container . appendChild(element2); container . appendChild(element4); container . insertBefore(element3, element4); container . insertBefore(element1, element2); - test \ document . getElementById(TEST_ID); + test \ Document_getElementById_document . getElementById(TEST_ID); assert_equals(test, element1, ''should return 1st element''); container . removeChild(element1); - test \ document . getElementById(TEST_ID); + test \ Document_getElementById_document . getElementById(TEST_ID); assert_equals(test, element2, ''should return 2nd element''); container . removeChild(element2); - test \ document . getElementById(TEST_ID); + test \ Document_getElementById_document . getElementById(TEST_ID); assert_equals(test, element3, ''should return 3rd element''); container . removeChild(element3); - test \ document . getElementById(TEST_ID); + test \ Document_getElementById_document . getElementById(TEST_ID); assert_equals(test, element4, ''should return 4th element''); container . removeChild(element4) }) Document_getElementById_heap" @@ -241,16 +241,16 @@ lemma "test (do { text \"Inserting an id by inserting its parent node"\ lemma "test (do { - gBody \ document . body; + gBody \ Document_getElementById_document . body; TEST_ID \ return ''test14''; - a \ document . createElement(''a''); - b \ document . createElement(''b''); + a \ Document_getElementById_document . createElement(''a''); + b \ Document_getElementById_document . createElement(''b''); a . appendChild(b); b . setAttribute(''id'', TEST_ID); - tmp0 \ document . getElementById(TEST_ID); + tmp0 \ Document_getElementById_document . getElementById(TEST_ID); assert_equals(tmp0, None); gBody . appendChild(a); - tmp1 \ document . getElementById(TEST_ID); + tmp1 \ Document_getElementById_document . getElementById(TEST_ID); assert_equals(tmp1, b) }) Document_getElementById_heap" by eval @@ -260,15 +260,15 @@ text \"Document.getElementById must not return nodes not present in docume lemma "test (do { TEST_ID \ return ''test15''; - outer \ document . getElementById(''outer''); - middle \ document . getElementById(''middle''); - inner \ document . getElementById(''inner''); - tmp0 \ document . getElementById(''middle''); + outer \ Document_getElementById_document . getElementById(''outer''); + middle \ Document_getElementById_document . getElementById(''middle''); + inner \ Document_getElementById_document . getElementById(''inner''); + tmp0 \ Document_getElementById_document . getElementById(''middle''); outer . removeChild(tmp0); - new_el \ document . createElement(''h1''); + new_el \ Document_getElementById_document . createElement(''h1''); new_el . setAttribute(''id'', ''heading''); inner . appendChild(new_el); - tmp1 \ document . getElementById(''heading''); + tmp1 \ Document_getElementById_document . getElementById(''heading''); assert_equals(tmp1, None) }) Document_getElementById_heap" by eval diff --git a/Core_DOM/tests/Node_insertBefore.thy b/Core_DOM/tests/Node_insertBefore.thy index 64284cb..0e6b40c 100644 --- a/Core_DOM/tests/Node_insertBefore.thy +++ b/Core_DOM/tests/Node_insertBefore.thy @@ -27,8 +27,10 @@ * SPDX-License-Identifier: BSD-2-Clause ***********************************************************************************) -section\Testing insertBefore\ -text\This theory contains the test cases for insertBefore.\ +(* This file is automatically generated, please do not modify! *) + +section\Testing Core_DOM\ +text\This theory contains the test cases for Core_DOM.\ theory Node_insertBefore imports @@ -48,14 +50,14 @@ definition Node_insertBefore_heap :: heap⇩f⇩i⇩n⇩a⇩l where (cast (element_ptr.Ref 8), cast (create_element_obj ''script'' [cast (character_data_ptr.Ref 2)] fmempty None)), (cast (character_data_ptr.Ref 2), cast (create_character_data_obj ''%3C%3Cscript%3E%3E''))]" -definition document :: "(unit, unit, unit, unit, unit, unit) object_ptr option" where "document = Some (cast (document_ptr.Ref 1))" +definition Node_insertBefore_document :: "(unit, unit, unit, unit, unit, unit) object_ptr option" where "Node_insertBefore_document = Some (cast (document_ptr.Ref 1))" text \"Calling insertBefore an a leaf node Text must throw HIERARCHY\_REQUEST\_ERR."\ lemma "test (do { - node \ document . createTextNode(''Foo''); - tmp0 \ document . createTextNode(''fail''); + node \ Node_insertBefore_document . createTextNode(''Foo''); + tmp0 \ Node_insertBefore_document . createTextNode(''fail''); assert_throws(HierarchyRequestError, node . insertBefore(tmp0, None)) }) Node_insertBefore_heap" by eval @@ -64,13 +66,13 @@ lemma "test (do { text \"Calling insertBefore with an inclusive ancestor of the context object must throw HIERARCHY\_REQUEST\_ERR."\ lemma "test (do { - tmp1 \ document . body; - tmp2 \ document . getElementById(''log''); - tmp0 \ document . body; + tmp1 \ Node_insertBefore_document . body; + tmp2 \ Node_insertBefore_document . getElementById(''log''); + tmp0 \ Node_insertBefore_document . body; assert_throws(HierarchyRequestError, tmp0 . insertBefore(tmp1, tmp2)); - tmp4 \ document . documentElement; - tmp5 \ document . getElementById(''log''); - tmp3 \ document . body; + tmp4 \ Node_insertBefore_document . documentElement; + tmp5 \ Node_insertBefore_document . getElementById(''log''); + tmp3 \ Node_insertBefore_document . body; assert_throws(HierarchyRequestError, tmp3 . insertBefore(tmp4, tmp5)) }) Node_insertBefore_heap" by eval @@ -79,9 +81,9 @@ lemma "test (do { text \"Calling insertBefore with a reference child whose parent is not the context node must throw a NotFoundError."\ lemma "test (do { - a \ document . createElement(''div''); - b \ document . createElement(''div''); - c \ document . createElement(''div''); + a \ Node_insertBefore_document . createElement(''div''); + b \ Node_insertBefore_document . createElement(''div''); + c \ Node_insertBefore_document . createElement(''div''); assert_throws(NotFoundError, a . insertBefore(b, c)) }) Node_insertBefore_heap" by eval @@ -104,9 +106,9 @@ lemma "test (do { text \"Inserting a node before itself should not move the node"\ lemma "test (do { - a \ document . createElement(''div''); - b \ document . createElement(''div''); - c \ document . createElement(''div''); + a \ Node_insertBefore_document . createElement(''div''); + b \ Node_insertBefore_document . createElement(''div''); + c \ Node_insertBefore_document . createElement(''div''); a . appendChild(b); a . appendChild(c); tmp0 \ a . childNodes; diff --git a/Core_DOM/tests/Node_removeChild.thy b/Core_DOM/tests/Node_removeChild.thy index 812db93..423844d 100644 --- a/Core_DOM/tests/Node_removeChild.thy +++ b/Core_DOM/tests/Node_removeChild.thy @@ -27,8 +27,10 @@ * SPDX-License-Identifier: BSD-2-Clause ***********************************************************************************) -section\Testing removeChild\ -text\This theory contains the test cases for removeChild.\ +(* This file is automatically generated, please do not modify! *) + +section\Testing Core_DOM\ +text\This theory contains the test cases for Core_DOM.\ theory Node_removeChild imports @@ -50,17 +52,17 @@ definition Node_removeChild_heap :: heap⇩f⇩i⇩n⇩a⇩l where (cast (element_ptr.Ref 10), cast (create_element_obj ''script'' [cast (character_data_ptr.Ref 2)] fmempty None)), (cast (character_data_ptr.Ref 2), cast (create_character_data_obj ''%3C%3Cscript%3E%3E''))]" -definition document :: "(unit, unit, unit, unit, unit, unit) object_ptr option" where "document = Some (cast (document_ptr.Ref 1))" +definition Node_removeChild_document :: "(unit, unit, unit, unit, unit, unit) object_ptr option" where "Node_removeChild_document = Some (cast (document_ptr.Ref 1))" text \"Passing a detached Element to removeChild should not affect it."\ lemma "test (do { - doc \ return document; + doc \ return Node_removeChild_document; s \ doc . createElement(''div''); tmp0 \ s . ownerDocument; assert_equals(tmp0, doc); - tmp1 \ document . body; + tmp1 \ Node_removeChild_document . body; assert_throws(NotFoundError, tmp1 . removeChild(s)); tmp2 \ s . ownerDocument; assert_equals(tmp2, doc) @@ -71,13 +73,13 @@ lemma "test (do { text \"Passing a non-detached Element to removeChild should not affect it."\ lemma "test (do { - doc \ return document; + doc \ return Node_removeChild_document; s \ doc . createElement(''div''); tmp0 \ doc . documentElement; tmp0 . appendChild(s); tmp1 \ s . ownerDocument; assert_equals(tmp1, doc); - tmp2 \ document . body; + tmp2 \ Node_removeChild_document . body; assert_throws(NotFoundError, tmp2 . removeChild(s)); tmp3 \ s . ownerDocument; assert_equals(tmp3, doc) @@ -88,7 +90,7 @@ lemma "test (do { text \"Calling removeChild on an Element with no children should throw NOT\_FOUND\_ERR."\ lemma "test (do { - doc \ return document; + doc \ return Node_removeChild_document; s \ doc . createElement(''div''); tmp0 \ doc . body; tmp0 . appendChild(s); @@ -106,7 +108,7 @@ lemma "test (do { s \ doc . createElement(''div''); tmp0 \ s . ownerDocument; assert_equals(tmp0, doc); - tmp1 \ document . body; + tmp1 \ Node_removeChild_document . body; assert_throws(NotFoundError, tmp1 . removeChild(s)); tmp2 \ s . ownerDocument; assert_equals(tmp2, doc) @@ -123,7 +125,7 @@ lemma "test (do { tmp0 . appendChild(s); tmp1 \ s . ownerDocument; assert_equals(tmp1, doc); - tmp2 \ document . body; + tmp2 \ Node_removeChild_document . body; assert_throws(NotFoundError, tmp2 . removeChild(s)); tmp3 \ s . ownerDocument; assert_equals(tmp3, doc) @@ -148,7 +150,7 @@ lemma "test (do { text \"Passing a value that is not a Node reference to removeChild should throw TypeError."\ lemma "test (do { - tmp0 \ document . body; + tmp0 \ Node_removeChild_document . body; assert_throws(TypeError, tmp0 . removeChild(None)) }) Node_removeChild_heap" by eval