Import of official AFP entry for Isabelle 2019.
This commit is contained in:
parent
ae19cacb08
commit
ee9811a317
|
|
@ -3,7 +3,7 @@ pipeline {
|
|||
stages {
|
||||
stage('Build') {
|
||||
steps {
|
||||
sh 'docker run -v $PWD/Core_DOM:/Core_DOM logicalhacking:isabelle2018 isabelle build -D /Core_DOM'
|
||||
sh 'docker run -v $PWD/Core_DOM:/Core_DOM logicalhacking:isabelle2019 isabelle build -D /Core_DOM'
|
||||
}
|
||||
}
|
||||
}
|
||||
|
|
|
|||
|
|
@ -1,7 +1,7 @@
|
|||
chapter AFP
|
||||
|
||||
session "Core_DOM-devel" (AFP) = "HOL-Library" +
|
||||
options [timeout = 600]
|
||||
options [timeout = 1200]
|
||||
theories
|
||||
Core_DOM
|
||||
Core_DOM_Tests
|
||||
|
|
|
|||
|
|
@ -57,9 +57,10 @@ lemma character_data_ptr_kinds_M_eq:
|
|||
lemma character_data_ptr_kinds_M_reads:
|
||||
"reads (\<Union>node_ptr. {preserved (get_M\<^sub>O\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t node_ptr RObject.nothing)}) character_data_ptr_kinds_M h h'"
|
||||
using node_ptr_kinds_M_reads
|
||||
apply(simp add: reads_def node_ptr_kinds_M_defs character_data_ptr_kinds_M_defs
|
||||
character_data_ptr_kinds_def preserved_def)
|
||||
by (metis (mono_tags, hide_lams) node_ptr_kinds_small old.unit.exhaust preserved_def)
|
||||
apply (simp add: reads_def node_ptr_kinds_M_defs character_data_ptr_kinds_M_defs
|
||||
character_data_ptr_kinds_def preserved_def cong del: image_cong_simp)
|
||||
apply (metis (mono_tags, hide_lams) node_ptr_kinds_small old.unit.exhaust preserved_def)
|
||||
done
|
||||
|
||||
global_interpretation l_dummy defines get_M\<^sub>C\<^sub>h\<^sub>a\<^sub>r\<^sub>a\<^sub>c\<^sub>t\<^sub>e\<^sub>r\<^sub>D\<^sub>a\<^sub>t\<^sub>a = "l_get_M.a_get_M get\<^sub>C\<^sub>h\<^sub>a\<^sub>r\<^sub>a\<^sub>c\<^sub>t\<^sub>e\<^sub>r\<^sub>D\<^sub>a\<^sub>t\<^sub>a" .
|
||||
lemma get_M_is_l_get_M: "l_get_M get\<^sub>C\<^sub>h\<^sub>a\<^sub>r\<^sub>a\<^sub>c\<^sub>t\<^sub>e\<^sub>r\<^sub>D\<^sub>a\<^sub>t\<^sub>a type_wf character_data_ptr_kinds"
|
||||
|
|
|
|||
|
|
@ -55,10 +55,10 @@ lemma document_ptr_kinds_M_eq:
|
|||
lemma document_ptr_kinds_M_reads:
|
||||
"reads (\<Union>object_ptr. {preserved (get_M\<^sub>O\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t object_ptr RObject.nothing)}) document_ptr_kinds_M h h'"
|
||||
using object_ptr_kinds_M_reads
|
||||
|
||||
apply(simp add: reads_def object_ptr_kinds_M_defs document_ptr_kinds_M_defs
|
||||
document_ptr_kinds_def preserved_def)
|
||||
by (metis (mono_tags, hide_lams) object_ptr_kinds_preserved_small old.unit.exhaust preserved_def)
|
||||
apply (simp add: reads_def object_ptr_kinds_M_defs document_ptr_kinds_M_defs
|
||||
document_ptr_kinds_def preserved_def cong del: image_cong_simp)
|
||||
apply (metis (mono_tags, hide_lams) object_ptr_kinds_preserved_small old.unit.exhaust preserved_def)
|
||||
done
|
||||
|
||||
global_interpretation l_dummy defines get_M\<^sub>D\<^sub>o\<^sub>c\<^sub>u\<^sub>m\<^sub>e\<^sub>n\<^sub>t = "l_get_M.a_get_M get\<^sub>D\<^sub>o\<^sub>c\<^sub>u\<^sub>m\<^sub>e\<^sub>n\<^sub>t" .
|
||||
lemma get_M_is_l_get_M: "l_get_M get\<^sub>D\<^sub>o\<^sub>c\<^sub>u\<^sub>m\<^sub>e\<^sub>n\<^sub>t type_wf document_ptr_kinds"
|
||||
|
|
|
|||
|
|
@ -54,9 +54,10 @@ lemma element_ptr_kinds_M_eq:
|
|||
|
||||
lemma element_ptr_kinds_M_reads:
|
||||
"reads (\<Union>element_ptr. {preserved (get_M\<^sub>O\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t element_ptr RObject.nothing)}) element_ptr_kinds_M h h'"
|
||||
apply(simp add: reads_def node_ptr_kinds_M_defs element_ptr_kinds_M_defs element_ptr_kinds_def
|
||||
node_ptr_kinds_M_reads preserved_def)
|
||||
by (metis (mono_tags, hide_lams) node_ptr_kinds_small old.unit.exhaust preserved_def)
|
||||
apply (simp add: reads_def node_ptr_kinds_M_defs element_ptr_kinds_M_defs element_ptr_kinds_def
|
||||
node_ptr_kinds_M_reads preserved_def cong del: image_cong_simp)
|
||||
apply (metis (mono_tags, hide_lams) node_ptr_kinds_small old.unit.exhaust preserved_def)
|
||||
done
|
||||
|
||||
global_interpretation l_dummy defines get_M\<^sub>E\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t = "l_get_M.a_get_M get\<^sub>E\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t" .
|
||||
lemma get_M_is_l_get_M: "l_get_M get\<^sub>E\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t type_wf element_ptr_kinds"
|
||||
|
|
|
|||
|
|
@ -75,9 +75,10 @@ global_interpretation l_get_M\<^sub>N\<^sub>o\<^sub>d\<^sub>e_lemmas type_wf by
|
|||
lemma node_ptr_kinds_M_reads:
|
||||
"reads (\<Union>object_ptr. {preserved (get_M\<^sub>O\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t object_ptr RObject.nothing)}) node_ptr_kinds_M h h'"
|
||||
using object_ptr_kinds_M_reads
|
||||
apply(simp add: reads_def node_ptr_kinds_M_defs node_ptr_kinds_def
|
||||
object_ptr_kinds_M_reads preserved_def)
|
||||
by (metis (mono_tags, hide_lams) object_ptr_kinds_preserved_small old.unit.exhaust preserved_def)
|
||||
apply (simp add: reads_def node_ptr_kinds_M_defs node_ptr_kinds_def
|
||||
object_ptr_kinds_M_reads preserved_def cong del: image_cong_simp)
|
||||
apply (metis (mono_tags, hide_lams) object_ptr_kinds_preserved_small old.unit.exhaust preserved_def)
|
||||
done
|
||||
|
||||
global_interpretation l_put_M type_wf node_ptr_kinds get\<^sub>N\<^sub>o\<^sub>d\<^sub>e put\<^sub>N\<^sub>o\<^sub>d\<^sub>e
|
||||
rewrites "a_get_M = get_M\<^sub>N\<^sub>o\<^sub>d\<^sub>e"
|
||||
|
|
|
|||
|
|
@ -1,50 +0,0 @@
|
|||
<!doctype html>
|
||||
<meta charset=utf-8>
|
||||
<title>Document.adoptNode</title>
|
||||
<link rel=help href="https://dom.spec.whatwg.org/#dom-document-adoptnode">
|
||||
<script src="/resources/testharness.js"></script>
|
||||
<script src="/resources/testharnessreport.js"></script>
|
||||
<div id="log"></div>
|
||||
<!--creates an element with local name "x<": --><x<>x</x<>
|
||||
<script>
|
||||
test(function() {
|
||||
var y = document.getElementsByTagName("x<")[0]
|
||||
var child = y.firstChild
|
||||
assert_equals(y.parentNode, document.body)
|
||||
assert_equals(y.ownerDocument, document)
|
||||
assert_equals(document.adoptNode(y), y)
|
||||
assert_equals(y.parentNode, null)
|
||||
assert_equals(y.firstChild, child)
|
||||
assert_equals(y.ownerDocument, document)
|
||||
assert_equals(child.ownerDocument, document)
|
||||
var doc = document.implementation.createDocument(null, null, null)
|
||||
assert_equals(doc.adoptNode(y), y)
|
||||
assert_equals(y.parentNode, null)
|
||||
assert_equals(y.firstChild, child)
|
||||
assert_equals(y.ownerDocument, doc)
|
||||
assert_equals(child.ownerDocument, doc)
|
||||
}, "Adopting an Element called 'x<' should work.")
|
||||
|
||||
test(function() {
|
||||
var x = document.createElement(":good:times:")
|
||||
assert_equals(document.adoptNode(x), x);
|
||||
var doc = document.implementation.createDocument(null, null, null)
|
||||
assert_equals(doc.adoptNode(x), x)
|
||||
assert_equals(x.parentNode, null)
|
||||
assert_equals(x.ownerDocument, doc)
|
||||
}, "Adopting an Element called ':good:times:' should work.")
|
||||
|
||||
test(function() {
|
||||
var doctype = document.doctype;
|
||||
assert_equals(doctype.parentNode, document)
|
||||
assert_equals(doctype.ownerDocument, document)
|
||||
assert_equals(document.adoptNode(doctype), doctype)
|
||||
assert_equals(doctype.parentNode, null)
|
||||
assert_equals(doctype.ownerDocument, document)
|
||||
}, "Explicitly adopting a DocumentType should work.")
|
||||
|
||||
test(function() {
|
||||
var doc = document.implementation.createDocument(null, null, null)
|
||||
assert_throws("NOT_SUPPORTED_ERR", function() { document.adoptNode(doc) })
|
||||
}, "Adopting a Document should throw.")
|
||||
</script>
|
||||
|
|
@ -1,350 +0,0 @@
|
|||
<!DOCTYPE html>
|
||||
<meta charset=utf-8>
|
||||
<title>Document.getElementById</title>
|
||||
<link rel="author" title="Tetsuharu OHZEKI" href="mailto:saneyuki.snyk@gmail.com">
|
||||
<link rel=help href="https://dom.spec.whatwg.org/#dom-document-getelementbyid">
|
||||
<script src="/resources/testharness.js"></script>
|
||||
<script src="/resources/testharnessreport.js"></script>
|
||||
<body>
|
||||
<div id="log"></div>
|
||||
|
||||
<!-- test 0 -->
|
||||
<div id=""></div>
|
||||
|
||||
<!-- test 1 -->
|
||||
<div id="test1"></div>
|
||||
|
||||
<!-- test 5 -->
|
||||
<div id="test5" data-name="1st">
|
||||
<p id="test5" data-name="2nd">P</p>
|
||||
<input id="test5" type="submit" value="Submit" data-name="3rd">
|
||||
</div>
|
||||
|
||||
<!-- test 15 -->
|
||||
<div id="outer">
|
||||
<div id="middle">
|
||||
<div id="inner"></div>
|
||||
</div>
|
||||
</div>
|
||||
|
||||
<script>
|
||||
var gBody = document.getElementsByTagName("body")[0];
|
||||
|
||||
test(function() {
|
||||
assert_equals(document.getElementById(""), null);
|
||||
}, "Calling document.getElementById with an empty string argument.");
|
||||
|
||||
test(function() {
|
||||
var element = document.createElement("div");
|
||||
element.setAttribute("id", "null");
|
||||
document.body.appendChild(element);
|
||||
this.add_cleanup(function() { document.body.removeChild(element) });
|
||||
assert_equals(document.getElementById(null), element);
|
||||
}, "Calling document.getElementById with a null argument.");
|
||||
|
||||
test(function() {
|
||||
var element = document.createElement("div");
|
||||
element.setAttribute("id", "undefined");
|
||||
document.body.appendChild(element);
|
||||
this.add_cleanup(function() { document.body.removeChild(element) });
|
||||
assert_equals(document.getElementById(undefined), element);
|
||||
}, "Calling document.getElementById with an undefined argument.");
|
||||
|
||||
|
||||
test(function() {
|
||||
var bar = document.getElementById("test1");
|
||||
assert_not_equals(bar, null, "should not be null");
|
||||
assert_equals(bar.tagName, "DIV", "should have expected tag name.");
|
||||
assert_true(bar instanceof HTMLDivElement, "should be a valid Element instance");
|
||||
}, "on static page");
|
||||
|
||||
|
||||
test(function() {
|
||||
var TEST_ID = "test2";
|
||||
|
||||
var test = document.createElement("div");
|
||||
test.setAttribute("id", TEST_ID);
|
||||
gBody.appendChild(test);
|
||||
|
||||
// test: appended element
|
||||
var result = document.getElementById(TEST_ID);
|
||||
assert_not_equals(result, null, "should not be null.");
|
||||
assert_equals(result.tagName, "DIV", "should have appended element's tag name");
|
||||
assert_true(result instanceof HTMLDivElement, "should be a valid Element instance");
|
||||
|
||||
// test: removed element
|
||||
gBody.removeChild(test);
|
||||
var removed = document.getElementById(TEST_ID);
|
||||
// `document.getElementById()` returns `null` if there is none.
|
||||
// https://dom.spec.whatwg.org/#dom-nonelementparentnode-getelementbyid
|
||||
assert_equals(removed, null, "should not get removed element.");
|
||||
}, "Document.getElementById with a script-inserted element");
|
||||
|
||||
|
||||
test(function() {
|
||||
// setup fixtures.
|
||||
var TEST_ID = "test3";
|
||||
var test = document.createElement("div");
|
||||
test.setAttribute("id", TEST_ID);
|
||||
gBody.appendChild(test);
|
||||
|
||||
// update id
|
||||
var UPDATED_ID = "test3-updated";
|
||||
test.setAttribute("id", UPDATED_ID);
|
||||
var e = document.getElementById(UPDATED_ID);
|
||||
assert_equals(e, test, "should get the element with id.");
|
||||
|
||||
var old = document.getElementById(TEST_ID);
|
||||
assert_equals(old, null, "shouldn't get the element by the old id.");
|
||||
|
||||
// remove id.
|
||||
test.removeAttribute("id");
|
||||
var e2 = document.getElementById(UPDATED_ID);
|
||||
assert_equals(e2, null, "should return null when the passed id is none in document.");
|
||||
}, "update `id` attribute via setAttribute/removeAttribute");
|
||||
|
||||
|
||||
test(function() {
|
||||
var TEST_ID = "test4-should-not-exist";
|
||||
|
||||
var e = document.createElement('div');
|
||||
e.setAttribute("id", TEST_ID);
|
||||
|
||||
assert_equals(document.getElementById(TEST_ID), null, "should be null");
|
||||
document.body.appendChild(e);
|
||||
assert_equals(document.getElementById(TEST_ID), e, "should be the appended element");
|
||||
}, "Ensure that the id attribute only affects elements present in a document");
|
||||
|
||||
|
||||
test(function() {
|
||||
// the method should return the 1st element.
|
||||
var TEST_ID = "test5";
|
||||
var target = document.getElementById(TEST_ID);
|
||||
assert_not_equals(target, null, "should not be null");
|
||||
assert_equals(target.getAttribute("data-name"), "1st", "should return the 1st");
|
||||
|
||||
// even if after the new element was appended.
|
||||
var element4 = document.createElement("div");
|
||||
element4.setAttribute("id", TEST_ID);
|
||||
element4.setAttribute("data-name", "4th");
|
||||
gBody.appendChild(element4);
|
||||
var target2 = document.getElementById(TEST_ID);
|
||||
assert_not_equals(target2, null, "should not be null");
|
||||
assert_equals(target2.getAttribute("data-name"), "1st", "should be the 1st");
|
||||
|
||||
// should return the next element after removed the subtree including the 1st element.
|
||||
target2.parentNode.removeChild(target2);
|
||||
var target3 = document.getElementById(TEST_ID);
|
||||
assert_not_equals(target3, null, "should not be null");
|
||||
assert_equals(target3.getAttribute("data-name"), "4th", "should be the 4th");
|
||||
}, "in tree order, within the context object's tree");
|
||||
|
||||
|
||||
test(function() {
|
||||
var TEST_ID = "test6";
|
||||
var s = document.createElement("div");
|
||||
s.setAttribute("id", TEST_ID);
|
||||
// append to Element, not Document.
|
||||
document.createElement("div").appendChild(s);
|
||||
|
||||
assert_equals(document.getElementById(TEST_ID), null, "should be null");
|
||||
}, "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`.");
|
||||
|
||||
|
||||
test(function() {
|
||||
var TEST_ID = "test7"
|
||||
var element = document.createElement("div");
|
||||
element.setAttribute("id", TEST_ID);
|
||||
gBody.appendChild(element);
|
||||
|
||||
var target = document.getElementById(TEST_ID);
|
||||
assert_equals(target, element, "should return the element before changing the value");
|
||||
|
||||
element.attributes[0].value = TEST_ID + "-updated";
|
||||
var target2 = document.getElementById(TEST_ID);
|
||||
assert_equals(target2, null, "should return null after updated id via Attr.value");
|
||||
var target3 = document.getElementById(TEST_ID + "-updated");
|
||||
assert_equals(target3, element, "should be equal to the updated element.");
|
||||
}, "changing attribute's value via `Attr` gotten from `Element.attribute`.");
|
||||
|
||||
|
||||
test(function() {
|
||||
var TEST_ID = "test8";
|
||||
|
||||
// setup fixture
|
||||
var element = document.createElement("div");
|
||||
element.setAttribute("id", TEST_ID + "-fixture");
|
||||
gBody.appendChild(element);
|
||||
|
||||
// add id-ed element with using innerHTML
|
||||
element.innerHTML = "<div id='"+ TEST_ID +"'></div>";
|
||||
var test = document.getElementById(TEST_ID);
|
||||
assert_equals(test, element.firstChild, "should not be null");
|
||||
assert_equals(test.tagName, "DIV", "should have expected tag name.");
|
||||
assert_true(test instanceof HTMLDivElement, "should be a valid Element instance");
|
||||
}, "add id attribute via innerHTML");
|
||||
|
||||
|
||||
test(function() {
|
||||
var TEST_ID = "test9";
|
||||
|
||||
// add fixture
|
||||
var fixture = document.createElement("div");
|
||||
fixture.setAttribute("id", TEST_ID + "-fixture");
|
||||
gBody.appendChild(fixture);
|
||||
|
||||
var element = document.createElement("div");
|
||||
element.setAttribute("id", TEST_ID);
|
||||
fixture.appendChild(element);
|
||||
|
||||
// check 'getElementById' should get the 'element'
|
||||
assert_equals(document.getElementById(TEST_ID), element, "should not be null");
|
||||
|
||||
// remove id-ed element with using innerHTML (clear 'element')
|
||||
fixture.innerHTML = "";
|
||||
var test = document.getElementById(TEST_ID);
|
||||
assert_equals(test, null, "should be null.");
|
||||
}, "remove id attribute via innerHTML");
|
||||
|
||||
|
||||
test(function() {
|
||||
var TEST_ID = "test10";
|
||||
|
||||
// setup fixture
|
||||
var element = document.createElement("div");
|
||||
element.setAttribute("id", TEST_ID + "-fixture");
|
||||
gBody.appendChild(element);
|
||||
|
||||
// add id-ed element with using outerHTML
|
||||
element.outerHTML = "<div id='"+ TEST_ID +"'></div>";
|
||||
var test = document.getElementById(TEST_ID);
|
||||
assert_not_equals(test, null, "should not be null");
|
||||
assert_equals(test.tagName, "DIV", "should have expected tag name.");
|
||||
assert_true(test instanceof HTMLDivElement,"should be a valid Element instance");
|
||||
}, "add id attribute via outerHTML");
|
||||
|
||||
|
||||
test(function() {
|
||||
var TEST_ID = "test11";
|
||||
|
||||
var element = document.createElement("div");
|
||||
element.setAttribute("id", TEST_ID);
|
||||
gBody.appendChild(element);
|
||||
|
||||
var test = document.getElementById(TEST_ID);
|
||||
assert_equals(test, element, "should be equal to the appended element.");
|
||||
|
||||
// remove id-ed element with using outerHTML
|
||||
element.outerHTML = "<div></div>";
|
||||
var test = document.getElementById(TEST_ID);
|
||||
assert_equals(test, null, "should be null.");
|
||||
}, "remove id attribute via outerHTML");
|
||||
|
||||
|
||||
test(function() {
|
||||
// setup fixtures.
|
||||
var TEST_ID = "test12";
|
||||
var test = document.createElement("div");
|
||||
test.id = TEST_ID;
|
||||
gBody.appendChild(test);
|
||||
|
||||
// update id
|
||||
var UPDATED_ID = TEST_ID + "-updated";
|
||||
test.id = UPDATED_ID;
|
||||
var e = document.getElementById(UPDATED_ID);
|
||||
assert_equals(e, test, "should get the element with id.");
|
||||
|
||||
var old = document.getElementById(TEST_ID);
|
||||
assert_equals(old, null, "shouldn't get the element by the old id.");
|
||||
|
||||
// remove id.
|
||||
test.id = "";
|
||||
var e2 = document.getElementById(UPDATED_ID);
|
||||
assert_equals(e2, null, "should return null when the passed id is none in document.");
|
||||
}, "update `id` attribute via element.id");
|
||||
|
||||
|
||||
test(function() {
|
||||
var TEST_ID = "test13";
|
||||
|
||||
var create_same_id_element = function (order) {
|
||||
var element = document.createElement("div");
|
||||
element.setAttribute("id", TEST_ID);
|
||||
element.setAttribute("data-order", order);// for debug
|
||||
return element;
|
||||
};
|
||||
|
||||
// create fixture
|
||||
var container = document.createElement("div");
|
||||
container.setAttribute("id", TEST_ID + "-fixture");
|
||||
gBody.appendChild(container);
|
||||
|
||||
var element1 = create_same_id_element("1");
|
||||
var element2 = create_same_id_element("2");
|
||||
var element3 = create_same_id_element("3");
|
||||
var element4 = create_same_id_element("4");
|
||||
|
||||
// append element: 2 -> 4 -> 3 -> 1
|
||||
container.appendChild(element2);
|
||||
container.appendChild(element4);
|
||||
container.insertBefore(element3, element4);
|
||||
container.insertBefore(element1, element2);
|
||||
|
||||
|
||||
var test = document.getElementById(TEST_ID);
|
||||
assert_equals(test, element1, "should return 1st element");
|
||||
container.removeChild(element1);
|
||||
|
||||
test = document.getElementById(TEST_ID);
|
||||
assert_equals(test, element2, "should return 2nd element");
|
||||
container.removeChild(element2);
|
||||
|
||||
test = document.getElementById(TEST_ID);
|
||||
assert_equals(test, element3, "should return 3rd element");
|
||||
container.removeChild(element3);
|
||||
|
||||
test = document.getElementById(TEST_ID);
|
||||
assert_equals(test, element4, "should return 4th element");
|
||||
container.removeChild(element4);
|
||||
|
||||
|
||||
}, "where insertion order and tree order don't match");
|
||||
|
||||
test(function() {
|
||||
var TEST_ID = "test14";
|
||||
var a = document.createElement("a");
|
||||
var b = document.createElement("b");
|
||||
a.appendChild(b);
|
||||
b.id = TEST_ID;
|
||||
assert_equals(document.getElementById(TEST_ID), null);
|
||||
|
||||
gBody.appendChild(a);
|
||||
assert_equals(document.getElementById(TEST_ID), b);
|
||||
}, "Inserting an id by inserting its parent node");
|
||||
|
||||
test(function () {
|
||||
var TEST_ID = "test15"
|
||||
var outer = document.getElementById("outer");
|
||||
var middle = document.getElementById("middle");
|
||||
var inner = document.getElementById("inner");
|
||||
outer.removeChild(middle);
|
||||
|
||||
var new_el = document.createElement("h1");
|
||||
new_el.id = "heading";
|
||||
inner.appendChild(new_el);
|
||||
// the new element is not part of the document since
|
||||
// "middle" element was removed previously
|
||||
assert_equals(document.getElementById("heading"), null);
|
||||
}, "Document.getElementById must not return nodes not present in document");
|
||||
|
||||
// TODO:
|
||||
// id attribute in a namespace
|
||||
|
||||
|
||||
// TODO:
|
||||
// SVG + MathML elements with id attributes
|
||||
|
||||
</script>
|
||||
</body>
|
||||
</html>
|
||||
|
|
@ -1,306 +0,0 @@
|
|||
<!DOCTYPE html>
|
||||
<title>Node.insertBefore</title>
|
||||
<script src="/resources/testharness.js"></script>
|
||||
<script src="/resources/testharnessreport.js"></script>
|
||||
<div id="log"></div>
|
||||
<script>
|
||||
function testLeafNode(nodeName, createNodeFunction) {
|
||||
test(function() {
|
||||
var node = createNodeFunction();
|
||||
assert_throws(new TypeError(), function() { node.insertBefore(null, null) })
|
||||
}, "Calling insertBefore with a non-Node first argument on a leaf node " + nodeName + " must throw TypeError.")
|
||||
test(function() {
|
||||
var node = createNodeFunction();
|
||||
assert_throws("HIERARCHY_REQUEST_ERR", function() { node.insertBefore(document.createTextNode("fail"), null) })
|
||||
// Would be step 2.
|
||||
assert_throws("HIERARCHY_REQUEST_ERR", function() { node.insertBefore(node, null) })
|
||||
// Would be step 3.
|
||||
assert_throws("HIERARCHY_REQUEST_ERR", function() { node.insertBefore(node, document.createTextNode("child")) })
|
||||
}, "Calling insertBefore an a leaf node " + nodeName + " must throw HIERARCHY_REQUEST_ERR.")
|
||||
}
|
||||
|
||||
test(function() {
|
||||
// WebIDL.
|
||||
assert_throws(new TypeError(), function() { document.body.insertBefore(null, null) })
|
||||
assert_throws(new TypeError(), function() { document.body.insertBefore(null, document.body.firstChild) })
|
||||
assert_throws(new TypeError(), function() { document.body.insertBefore({'a':'b'}, document.body.firstChild) })
|
||||
}, "Calling insertBefore with a non-Node first argument must throw TypeError.")
|
||||
|
||||
testLeafNode("DocumentType", function () { return document.doctype; } )
|
||||
testLeafNode("Text", function () { return document.createTextNode("Foo") })
|
||||
testLeafNode("Comment", function () { return document.createComment("Foo") })
|
||||
testLeafNode("ProcessingInstruction", function () { return document.createProcessingInstruction("foo", "bar") })
|
||||
|
||||
test(function() {
|
||||
// Step 2.
|
||||
assert_throws("HIERARCHY_REQUEST_ERR", function() { document.body.insertBefore(document.body, document.getElementById("log")) })
|
||||
assert_throws("HIERARCHY_REQUEST_ERR", function() { document.body.insertBefore(document.documentElement, document.getElementById("log")) })
|
||||
}, "Calling insertBefore with an inclusive ancestor of the context object must throw HIERARCHY_REQUEST_ERR.")
|
||||
|
||||
// Step 3.
|
||||
test(function() {
|
||||
var a = document.createElement("div");
|
||||
var b = document.createElement("div");
|
||||
var c = document.createElement("div");
|
||||
assert_throws("NotFoundError", function() {
|
||||
a.insertBefore(b, c);
|
||||
});
|
||||
}, "Calling insertBefore with a reference child whose parent is not the context node must throw a NotFoundError.")
|
||||
|
||||
// Step 4.1.
|
||||
test(function() {
|
||||
var doc = document.implementation.createHTMLDocument("title");
|
||||
var doc2 = document.implementation.createHTMLDocument("title2");
|
||||
assert_throws("HierarchyRequestError", function() {
|
||||
doc.insertBefore(doc2, doc.documentElement);
|
||||
});
|
||||
|
||||
assert_throws("HierarchyRequestError", function() {
|
||||
doc.insertBefore(doc.createTextNode("text"), doc.documentElement);
|
||||
});
|
||||
}, "If the context node is a document, inserting a document or text node should throw a HierarchyRequestError.")
|
||||
|
||||
// Step 4.2.1.
|
||||
test(function() {
|
||||
var doc = document.implementation.createHTMLDocument("title");
|
||||
doc.removeChild(doc.documentElement);
|
||||
|
||||
var df = doc.createDocumentFragment();
|
||||
df.appendChild(doc.createElement("a"));
|
||||
df.appendChild(doc.createElement("b"));
|
||||
assert_throws("HierarchyRequestError", function() {
|
||||
doc.insertBefore(df, null);
|
||||
});
|
||||
|
||||
df = doc.createDocumentFragment();
|
||||
df.appendChild(doc.createTextNode("text"));
|
||||
assert_throws("HierarchyRequestError", function() {
|
||||
doc.insertBefore(df, null);
|
||||
});
|
||||
|
||||
df = doc.createDocumentFragment();
|
||||
df.appendChild(doc.createComment("comment"));
|
||||
df.appendChild(doc.createTextNode("text"));
|
||||
assert_throws("HierarchyRequestError", function() {
|
||||
doc.insertBefore(df, null);
|
||||
});
|
||||
}, "If the context node is a document, appending a DocumentFragment that contains a text node or too many elements should throw a HierarchyRequestError.")
|
||||
test(function() {
|
||||
var doc = document.implementation.createHTMLDocument("title");
|
||||
doc.removeChild(doc.documentElement);
|
||||
|
||||
var df = doc.createDocumentFragment();
|
||||
df.appendChild(doc.createElement("a"));
|
||||
df.appendChild(doc.createElement("b"));
|
||||
assert_throws("HierarchyRequestError", function() {
|
||||
doc.insertBefore(df, doc.firstChild);
|
||||
});
|
||||
|
||||
df = doc.createDocumentFragment();
|
||||
df.appendChild(doc.createTextNode("text"));
|
||||
assert_throws("HierarchyRequestError", function() {
|
||||
doc.insertBefore(df, doc.firstChild);
|
||||
});
|
||||
|
||||
df = doc.createDocumentFragment();
|
||||
df.appendChild(doc.createComment("comment"));
|
||||
df.appendChild(doc.createTextNode("text"));
|
||||
assert_throws("HierarchyRequestError", function() {
|
||||
doc.insertBefore(df, doc.firstChild);
|
||||
});
|
||||
}, "If the context node is a document, inserting a DocumentFragment that contains a text node or too many elements should throw a HierarchyRequestError.")
|
||||
|
||||
// Step 4.2.2.
|
||||
test(function() {
|
||||
// The context node has an element child.
|
||||
var doc = document.implementation.createHTMLDocument("title");
|
||||
var comment = doc.appendChild(doc.createComment("foo"));
|
||||
assert_array_equals(doc.childNodes, [doc.doctype, doc.documentElement, comment]);
|
||||
|
||||
var df = doc.createDocumentFragment();
|
||||
df.appendChild(doc.createElement("a"));
|
||||
assert_throws("HierarchyRequestError", function() {
|
||||
doc.insertBefore(df, doc.doctype);
|
||||
});
|
||||
assert_throws("HierarchyRequestError", function() {
|
||||
doc.insertBefore(df, doc.documentElement);
|
||||
});
|
||||
assert_throws("HierarchyRequestError", function() {
|
||||
doc.insertBefore(df, comment);
|
||||
});
|
||||
assert_throws("HierarchyRequestError", function() {
|
||||
doc.insertBefore(df, null);
|
||||
});
|
||||
}, "If the context node is a document, inserting a DocumentFragment with an element if there already is an element child should throw a HierarchyRequestError.")
|
||||
test(function() {
|
||||
// /child/ is a doctype.
|
||||
var doc = document.implementation.createHTMLDocument("title");
|
||||
var comment = doc.insertBefore(doc.createComment("foo"), doc.firstChild);
|
||||
doc.removeChild(doc.documentElement);
|
||||
assert_array_equals(doc.childNodes, [comment, doc.doctype]);
|
||||
|
||||
var df = doc.createDocumentFragment();
|
||||
df.appendChild(doc.createElement("a"));
|
||||
assert_throws("HierarchyRequestError", function() {
|
||||
doc.insertBefore(df, doc.doctype);
|
||||
});
|
||||
}, "If the context node is a document and a doctype is following the reference child, inserting a DocumentFragment with an element should throw a HierarchyRequestError.")
|
||||
test(function() {
|
||||
// /child/ is not null and a doctype is following /child/.
|
||||
var doc = document.implementation.createHTMLDocument("title");
|
||||
var comment = doc.insertBefore(doc.createComment("foo"), doc.firstChild);
|
||||
doc.removeChild(doc.documentElement);
|
||||
assert_array_equals(doc.childNodes, [comment, doc.doctype]);
|
||||
|
||||
var df = doc.createDocumentFragment();
|
||||
df.appendChild(doc.createElement("a"));
|
||||
assert_throws("HierarchyRequestError", function() {
|
||||
doc.insertBefore(df, comment);
|
||||
});
|
||||
}, "If the context node is a document, inserting a DocumentFragment with an element before the doctype should throw a HierarchyRequestError.")
|
||||
|
||||
// Step 4.3.
|
||||
test(function() {
|
||||
// The context node has an element child.
|
||||
var doc = document.implementation.createHTMLDocument("title");
|
||||
var comment = doc.appendChild(doc.createComment("foo"));
|
||||
assert_array_equals(doc.childNodes, [doc.doctype, doc.documentElement, comment]);
|
||||
|
||||
var a = doc.createElement("a");
|
||||
assert_throws("HierarchyRequestError", function() {
|
||||
doc.insertBefore(a, doc.doctype);
|
||||
});
|
||||
assert_throws("HierarchyRequestError", function() {
|
||||
doc.insertBefore(a, doc.documentElement);
|
||||
});
|
||||
assert_throws("HierarchyRequestError", function() {
|
||||
doc.insertBefore(a, comment);
|
||||
});
|
||||
assert_throws("HierarchyRequestError", function() {
|
||||
doc.insertBefore(a, null);
|
||||
});
|
||||
}, "If the context node is a document, inserting an element if there already is an element child should throw a HierarchyRequestError.")
|
||||
test(function() {
|
||||
// /child/ is a doctype.
|
||||
var doc = document.implementation.createHTMLDocument("title");
|
||||
var comment = doc.insertBefore(doc.createComment("foo"), doc.firstChild);
|
||||
doc.removeChild(doc.documentElement);
|
||||
assert_array_equals(doc.childNodes, [comment, doc.doctype]);
|
||||
|
||||
var a = doc.createElement("a");
|
||||
assert_throws("HierarchyRequestError", function() {
|
||||
doc.insertBefore(a, doc.doctype);
|
||||
});
|
||||
}, "If the context node is a document, inserting an element before the doctype should throw a HierarchyRequestError.")
|
||||
test(function() {
|
||||
// /child/ is not null and a doctype is following /child/.
|
||||
var doc = document.implementation.createHTMLDocument("title");
|
||||
var comment = doc.insertBefore(doc.createComment("foo"), doc.firstChild);
|
||||
doc.removeChild(doc.documentElement);
|
||||
assert_array_equals(doc.childNodes, [comment, doc.doctype]);
|
||||
|
||||
var a = doc.createElement("a");
|
||||
assert_throws("HierarchyRequestError", function() {
|
||||
doc.insertBefore(a, comment);
|
||||
});
|
||||
}, "If the context node is a document and a doctype is following the reference child, inserting an element should throw a HierarchyRequestError.")
|
||||
|
||||
// Step 4.4.
|
||||
test(function() {
|
||||
var doc = document.implementation.createHTMLDocument("title");
|
||||
var comment = doc.insertBefore(doc.createComment("foo"), doc.firstChild);
|
||||
assert_array_equals(doc.childNodes, [comment, doc.doctype, doc.documentElement]);
|
||||
|
||||
var doctype = document.implementation.createDocumentType("html", "", "");
|
||||
assert_throws("HierarchyRequestError", function() {
|
||||
doc.insertBefore(doctype, comment);
|
||||
});
|
||||
assert_throws("HierarchyRequestError", function() {
|
||||
doc.insertBefore(doctype, doc.doctype);
|
||||
});
|
||||
assert_throws("HierarchyRequestError", function() {
|
||||
doc.insertBefore(doctype, doc.documentElement);
|
||||
});
|
||||
assert_throws("HierarchyRequestError", function() {
|
||||
doc.insertBefore(doctype, null);
|
||||
});
|
||||
}, "If the context node is a document, inserting a doctype if there already is a doctype child should throw a HierarchyRequestError.")
|
||||
test(function() {
|
||||
var doc = document.implementation.createHTMLDocument("title");
|
||||
var comment = doc.appendChild(doc.createComment("foo"));
|
||||
doc.removeChild(doc.doctype);
|
||||
assert_array_equals(doc.childNodes, [doc.documentElement, comment]);
|
||||
|
||||
var doctype = document.implementation.createDocumentType("html", "", "");
|
||||
assert_throws("HierarchyRequestError", function() {
|
||||
doc.insertBefore(doctype, comment);
|
||||
});
|
||||
}, "If the context node is a document, inserting a doctype after the document element should throw a HierarchyRequestError.")
|
||||
test(function() {
|
||||
var doc = document.implementation.createHTMLDocument("title");
|
||||
var comment = doc.appendChild(doc.createComment("foo"));
|
||||
doc.removeChild(doc.doctype);
|
||||
assert_array_equals(doc.childNodes, [doc.documentElement, comment]);
|
||||
|
||||
var doctype = document.implementation.createDocumentType("html", "", "");
|
||||
assert_throws("HierarchyRequestError", function() {
|
||||
doc.insertBefore(doctype, null);
|
||||
});
|
||||
}, "If the context node is a document with and element child, appending a doctype should throw a HierarchyRequestError.")
|
||||
|
||||
// Step 5.
|
||||
test(function() {
|
||||
var df = document.createDocumentFragment();
|
||||
var a = df.appendChild(document.createElement("a"));
|
||||
|
||||
var doc = document.implementation.createHTMLDocument("title");
|
||||
assert_throws("HierarchyRequestError", function() {
|
||||
df.insertBefore(doc, a);
|
||||
});
|
||||
assert_throws("HierarchyRequestError", function() {
|
||||
df.insertBefore(doc, null);
|
||||
});
|
||||
|
||||
var doctype = document.implementation.createDocumentType("html", "", "");
|
||||
assert_throws("HierarchyRequestError", function() {
|
||||
df.insertBefore(doctype, a);
|
||||
});
|
||||
assert_throws("HierarchyRequestError", function() {
|
||||
df.insertBefore(doctype, null);
|
||||
});
|
||||
}, "If the context node is a DocumentFragment, inserting a document or a doctype should throw a HierarchyRequestError.")
|
||||
test(function() {
|
||||
var el = document.createElement("div");
|
||||
var a = el.appendChild(document.createElement("a"));
|
||||
|
||||
var doc = document.implementation.createHTMLDocument("title");
|
||||
assert_throws("HierarchyRequestError", function() {
|
||||
el.insertBefore(doc, a);
|
||||
});
|
||||
assert_throws("HierarchyRequestError", function() {
|
||||
el.insertBefore(doc, null);
|
||||
});
|
||||
|
||||
var doctype = document.implementation.createDocumentType("html", "", "");
|
||||
assert_throws("HierarchyRequestError", function() {
|
||||
el.insertBefore(doctype, a);
|
||||
});
|
||||
assert_throws("HierarchyRequestError", function() {
|
||||
el.insertBefore(doctype, null);
|
||||
});
|
||||
}, "If the context node is an element, inserting a document or a doctype should throw a HierarchyRequestError.")
|
||||
|
||||
// Step 7.
|
||||
test(function() {
|
||||
var a = document.createElement("div");
|
||||
var b = document.createElement("div");
|
||||
var c = document.createElement("div");
|
||||
a.appendChild(b);
|
||||
a.appendChild(c);
|
||||
assert_array_equals(a.childNodes, [b, c]);
|
||||
assert_equals(a.insertBefore(b, b), b);
|
||||
assert_array_equals(a.childNodes, [b, c]);
|
||||
assert_equals(a.insertBefore(c, c), c);
|
||||
assert_array_equals(a.childNodes, [b, c]);
|
||||
}, "Inserting a node before itself should not move the node");
|
||||
</script>
|
||||
|
|
@ -1,54 +0,0 @@
|
|||
<!DOCTYPE html>
|
||||
<title>Node.removeChild</title>
|
||||
<script src="/resources/testharness.js"></script>
|
||||
<script src="/resources/testharnessreport.js"></script>
|
||||
<script src="creators.js"></script>
|
||||
<div id="log"></div>
|
||||
<iframe src=about:blank></iframe>
|
||||
<script>
|
||||
var documents = [
|
||||
[function() { return document }, "the main document"],
|
||||
[function() { return frames[0].document }, "a frame document"],
|
||||
[function() { return document.implementation.createHTMLDocument() },
|
||||
"a synthetic document"],
|
||||
];
|
||||
|
||||
documents.forEach(function(d) {
|
||||
var get = d[0], description = d[1]
|
||||
for (var p in creators) {
|
||||
var creator = creators[p];
|
||||
test(function() {
|
||||
var doc = get();
|
||||
var s = doc[creator]("a")
|
||||
assert_equals(s.ownerDocument, doc)
|
||||
assert_throws("NOT_FOUND_ERR", function() { document.body.removeChild(s) })
|
||||
assert_equals(s.ownerDocument, doc)
|
||||
}, "Passing a detached " + p + " from " + description +
|
||||
" to removeChild should not affect it.")
|
||||
|
||||
test(function() {
|
||||
var doc = get();
|
||||
var s = doc[creator]("b")
|
||||
doc.documentElement.appendChild(s)
|
||||
assert_equals(s.ownerDocument, doc)
|
||||
assert_throws("NOT_FOUND_ERR", function() { document.body.removeChild(s) })
|
||||
assert_equals(s.ownerDocument, doc)
|
||||
}, "Passing a non-detached " + p + " from " + description +
|
||||
" to removeChild should not affect it.")
|
||||
|
||||
test(function() {
|
||||
var doc = get();
|
||||
var s = doc[creator]("test")
|
||||
doc.body.appendChild(s)
|
||||
assert_equals(s.ownerDocument, doc)
|
||||
assert_throws("NOT_FOUND_ERR", function() { s.removeChild(doc) })
|
||||
}, "Calling removeChild on a " + p + " from " + description +
|
||||
" with no children should throw NOT_FOUND_ERR.")
|
||||
}
|
||||
});
|
||||
|
||||
test(function() {
|
||||
assert_throws(new TypeError(), function() { document.body.removeChild(null) })
|
||||
assert_throws(new TypeError(), function() { document.body.removeChild({'a':'b'}) })
|
||||
}, "Passing a value that is not a Node reference to removeChild should throw TypeError.")
|
||||
</script>
|
||||
Loading…
Reference in New Issue