diff --git a/Core_DOM/Core_DOM.thy b/Core_DOM/common/Core_DOM.thy similarity index 95% rename from Core_DOM/Core_DOM.thy rename to Core_DOM/common/Core_DOM.thy index 70c10d7..de33929 100644 --- a/Core_DOM/Core_DOM.thy +++ b/Core_DOM/common/Core_DOM.thy @@ -32,8 +32,13 @@ text\This theory is the main entry point of our formalization of the core theory Core_DOM imports - "$CORE_DOM/Core_DOM_Heap_WF" + "Core_DOM_Heap_WF" begin +ML + {* + map warning (Posix.ProcEnv.environ()) +*} + end diff --git a/Core_DOM/Core_DOM_Basic_Datatypes.thy b/Core_DOM/common/Core_DOM_Basic_Datatypes.thy similarity index 100% rename from Core_DOM/Core_DOM_Basic_Datatypes.thy rename to Core_DOM/common/Core_DOM_Basic_Datatypes.thy diff --git a/Core_DOM/Core_DOM_Functions.thy b/Core_DOM/common/Core_DOM_Functions.thy similarity index 100% rename from Core_DOM/Core_DOM_Functions.thy rename to Core_DOM/common/Core_DOM_Functions.thy diff --git a/Core_DOM/Core_DOM_Tests.thy b/Core_DOM/common/Core_DOM_Tests.thy similarity index 100% rename from Core_DOM/Core_DOM_Tests.thy rename to Core_DOM/common/Core_DOM_Tests.thy diff --git a/Core_DOM/classes/BaseClass.thy b/Core_DOM/common/classes/BaseClass.thy similarity index 100% rename from Core_DOM/classes/BaseClass.thy rename to Core_DOM/common/classes/BaseClass.thy diff --git a/Core_DOM/classes/CharacterDataClass.thy b/Core_DOM/common/classes/CharacterDataClass.thy similarity index 99% rename from Core_DOM/classes/CharacterDataClass.thy rename to Core_DOM/common/classes/CharacterDataClass.thy index 59c5dc1..cf9786f 100644 --- a/Core_DOM/classes/CharacterDataClass.thy +++ b/Core_DOM/common/classes/CharacterDataClass.thy @@ -31,7 +31,7 @@ section\CharacterData\ text\In this theory, we introduce the types for the CharacterData class.\ theory CharacterDataClass imports - "$CORE_DOM/ElementClass" + ElementClass begin subsubsection\CharacterData\ diff --git a/Core_DOM/classes/DocumentClass.thy b/Core_DOM/common/classes/DocumentClass.thy similarity index 100% rename from Core_DOM/classes/DocumentClass.thy rename to Core_DOM/common/classes/DocumentClass.thy diff --git a/Core_DOM/classes/NodeClass.thy b/Core_DOM/common/classes/NodeClass.thy similarity index 100% rename from Core_DOM/classes/NodeClass.thy rename to Core_DOM/common/classes/NodeClass.thy diff --git a/Core_DOM/classes/ObjectClass.thy b/Core_DOM/common/classes/ObjectClass.thy similarity index 100% rename from Core_DOM/classes/ObjectClass.thy rename to Core_DOM/common/classes/ObjectClass.thy diff --git a/Core_DOM/classes/standard/ElementClass.thy b/Core_DOM/common/classes/standard/ElementClass.thy similarity index 100% rename from Core_DOM/classes/standard/ElementClass.thy rename to Core_DOM/common/classes/standard/ElementClass.thy diff --git a/Core_DOM/document/root.bib b/Core_DOM/common/document/root.bib similarity index 100% rename from Core_DOM/document/root.bib rename to Core_DOM/common/document/root.bib diff --git a/Core_DOM/document/root.tex b/Core_DOM/common/document/root.tex similarity index 100% rename from Core_DOM/document/root.tex rename to Core_DOM/common/document/root.tex diff --git a/Core_DOM/monads/BaseMonad.thy b/Core_DOM/common/monads/BaseMonad.thy similarity index 100% rename from Core_DOM/monads/BaseMonad.thy rename to Core_DOM/common/monads/BaseMonad.thy diff --git a/Core_DOM/monads/CharacterDataMonad.thy b/Core_DOM/common/monads/CharacterDataMonad.thy similarity index 100% rename from Core_DOM/monads/CharacterDataMonad.thy rename to Core_DOM/common/monads/CharacterDataMonad.thy diff --git a/Core_DOM/monads/DocumentMonad.thy b/Core_DOM/common/monads/DocumentMonad.thy similarity index 100% rename from Core_DOM/monads/DocumentMonad.thy rename to Core_DOM/common/monads/DocumentMonad.thy diff --git a/Core_DOM/monads/ElementMonad.thy b/Core_DOM/common/monads/ElementMonad.thy similarity index 99% rename from Core_DOM/monads/ElementMonad.thy rename to Core_DOM/common/monads/ElementMonad.thy index 48ca417..de137cc 100644 --- a/Core_DOM/monads/ElementMonad.thy +++ b/Core_DOM/common/monads/ElementMonad.thy @@ -32,7 +32,7 @@ text\In this theory, we introduce the monadic method setup for the Element theory ElementMonad imports NodeMonad - "../classes/$CORE_DOM/ElementClass" + "ElementClass" begin type_synonym ('object_ptr, 'node_ptr, 'element_ptr, 'character_data_ptr, 'document_ptr, diff --git a/Core_DOM/monads/NodeMonad.thy b/Core_DOM/common/monads/NodeMonad.thy similarity index 100% rename from Core_DOM/monads/NodeMonad.thy rename to Core_DOM/common/monads/NodeMonad.thy diff --git a/Core_DOM/monads/ObjectMonad.thy b/Core_DOM/common/monads/ObjectMonad.thy similarity index 100% rename from Core_DOM/monads/ObjectMonad.thy rename to Core_DOM/common/monads/ObjectMonad.thy diff --git a/Core_DOM/pointers/CharacterDataPointer.thy b/Core_DOM/common/pointers/CharacterDataPointer.thy similarity index 100% rename from Core_DOM/pointers/CharacterDataPointer.thy rename to Core_DOM/common/pointers/CharacterDataPointer.thy diff --git a/Core_DOM/pointers/DocumentPointer.thy b/Core_DOM/common/pointers/DocumentPointer.thy similarity index 100% rename from Core_DOM/pointers/DocumentPointer.thy rename to Core_DOM/common/pointers/DocumentPointer.thy diff --git a/Core_DOM/pointers/ElementPointer.thy b/Core_DOM/common/pointers/ElementPointer.thy similarity index 100% rename from Core_DOM/pointers/ElementPointer.thy rename to Core_DOM/common/pointers/ElementPointer.thy diff --git a/Core_DOM/pointers/NodePointer.thy b/Core_DOM/common/pointers/NodePointer.thy similarity index 100% rename from Core_DOM/pointers/NodePointer.thy rename to Core_DOM/common/pointers/NodePointer.thy diff --git a/Core_DOM/pointers/ObjectPointer.thy b/Core_DOM/common/pointers/ObjectPointer.thy similarity index 100% rename from Core_DOM/pointers/ObjectPointer.thy rename to Core_DOM/common/pointers/ObjectPointer.thy diff --git a/Core_DOM/pointers/Ref.thy b/Core_DOM/common/pointers/Ref.thy similarity index 100% rename from Core_DOM/pointers/Ref.thy rename to Core_DOM/common/pointers/Ref.thy diff --git a/Core_DOM/pointers/standard/ShadowRootPointer.thy b/Core_DOM/common/pointers/standard/ShadowRootPointer.thy similarity index 100% rename from Core_DOM/pointers/standard/ShadowRootPointer.thy rename to Core_DOM/common/pointers/standard/ShadowRootPointer.thy diff --git a/Core_DOM/preliminaries/Heap_Error_Monad.thy b/Core_DOM/common/preliminaries/Heap_Error_Monad.thy similarity index 100% rename from Core_DOM/preliminaries/Heap_Error_Monad.thy rename to Core_DOM/common/preliminaries/Heap_Error_Monad.thy diff --git a/Core_DOM/preliminaries/Hiding_Type_Variables.thy b/Core_DOM/common/preliminaries/Hiding_Type_Variables.thy similarity index 100% rename from Core_DOM/preliminaries/Hiding_Type_Variables.thy rename to Core_DOM/common/preliminaries/Hiding_Type_Variables.thy diff --git a/Core_DOM/preliminaries/Testing_Utils.thy b/Core_DOM/common/preliminaries/Testing_Utils.thy similarity index 100% rename from Core_DOM/preliminaries/Testing_Utils.thy rename to Core_DOM/common/preliminaries/Testing_Utils.thy diff --git a/Core_DOM/tests/Core_DOM_BaseTest.thy b/Core_DOM/common/tests/Core_DOM_BaseTest.thy similarity index 100% rename from Core_DOM/tests/Core_DOM_BaseTest.thy rename to Core_DOM/common/tests/Core_DOM_BaseTest.thy diff --git a/Core_DOM/tests/Document-adoptNode.html b/Core_DOM/common/tests/Document-adoptNode.html similarity index 100% rename from Core_DOM/tests/Document-adoptNode.html rename to Core_DOM/common/tests/Document-adoptNode.html diff --git a/Core_DOM/tests/Document-adoptNode.html.orig b/Core_DOM/common/tests/Document-adoptNode.html.orig similarity index 100% rename from Core_DOM/tests/Document-adoptNode.html.orig rename to Core_DOM/common/tests/Document-adoptNode.html.orig diff --git a/Core_DOM/tests/Document-getElementById.html b/Core_DOM/common/tests/Document-getElementById.html similarity index 100% rename from Core_DOM/tests/Document-getElementById.html rename to Core_DOM/common/tests/Document-getElementById.html diff --git a/Core_DOM/tests/Document-getElementById.html.orig b/Core_DOM/common/tests/Document-getElementById.html.orig similarity index 100% rename from Core_DOM/tests/Document-getElementById.html.orig rename to Core_DOM/common/tests/Document-getElementById.html.orig diff --git a/Core_DOM/tests/Document_adoptNode.thy b/Core_DOM/common/tests/Document_adoptNode.thy similarity index 100% rename from Core_DOM/tests/Document_adoptNode.thy rename to Core_DOM/common/tests/Document_adoptNode.thy diff --git a/Core_DOM/tests/Document_getElementById.thy b/Core_DOM/common/tests/Document_getElementById.thy similarity index 100% rename from Core_DOM/tests/Document_getElementById.thy rename to Core_DOM/common/tests/Document_getElementById.thy diff --git a/Core_DOM/tests/Node-insertBefore.html b/Core_DOM/common/tests/Node-insertBefore.html similarity index 100% rename from Core_DOM/tests/Node-insertBefore.html rename to Core_DOM/common/tests/Node-insertBefore.html diff --git a/Core_DOM/tests/Node-insertBefore.html.orig b/Core_DOM/common/tests/Node-insertBefore.html.orig similarity index 100% rename from Core_DOM/tests/Node-insertBefore.html.orig rename to Core_DOM/common/tests/Node-insertBefore.html.orig diff --git a/Core_DOM/tests/Node-removeChild.html b/Core_DOM/common/tests/Node-removeChild.html similarity index 100% rename from Core_DOM/tests/Node-removeChild.html rename to Core_DOM/common/tests/Node-removeChild.html diff --git a/Core_DOM/tests/Node-removeChild.html.orig b/Core_DOM/common/tests/Node-removeChild.html.orig similarity index 100% rename from Core_DOM/tests/Node-removeChild.html.orig rename to Core_DOM/common/tests/Node-removeChild.html.orig diff --git a/Core_DOM/tests/Node_insertBefore.thy b/Core_DOM/common/tests/Node_insertBefore.thy similarity index 100% rename from Core_DOM/tests/Node_insertBefore.thy rename to Core_DOM/common/tests/Node_insertBefore.thy diff --git a/Core_DOM/tests/Node_removeChild.thy b/Core_DOM/common/tests/Node_removeChild.thy similarity index 100% rename from Core_DOM/tests/Node_removeChild.thy rename to Core_DOM/common/tests/Node_removeChild.thy diff --git a/Core_DOM/sc_components/Core_DOM_Heap_WF.thy b/Core_DOM/sc_components/Core_DOM_Heap_WF.thy index 2258c97..d611b65 100644 --- a/Core_DOM/sc_components/Core_DOM_Heap_WF.thy +++ b/Core_DOM/sc_components/Core_DOM_Heap_WF.thy @@ -34,7 +34,7 @@ DOM to what extend they preserve wellformendess.\ theory Core_DOM_Heap_WF imports - "../Core_DOM_Functions" + "Core_DOM_Functions" begin locale l_heap_is_wellformed\<^sub>C\<^sub>o\<^sub>r\<^sub>e\<^sub>_\<^sub>D\<^sub>O\<^sub>M_defs = diff --git a/Core_DOM/classes/sc_components/ElementClass.thy b/Core_DOM/sc_components/classes/ElementClass.thy similarity index 99% rename from Core_DOM/classes/sc_components/ElementClass.thy rename to Core_DOM/sc_components/classes/ElementClass.thy index a890511..f738c8c 100644 --- a/Core_DOM/classes/sc_components/ElementClass.thy +++ b/Core_DOM/sc_components/classes/ElementClass.thy @@ -31,8 +31,8 @@ section\Element\ text\In this theory, we introduce the types for the Element class.\ theory ElementClass imports - "../NodeClass" - "../../pointers/$CORE_DOM/ShadowRootPointer" + "NodeClass" + "ShadowRootPointer" begin text\The type @{type "DOMString"} is a type synonym for @{type "string"}, define in \autoref{sec:Core_DOM_Basic_Datatypes}.\ diff --git a/Core_DOM/pointers/sc_components/ShadowRootPointer.thy b/Core_DOM/sc_components/pointers/ShadowRootPointer.thy similarity index 99% rename from Core_DOM/pointers/sc_components/ShadowRootPointer.thy rename to Core_DOM/sc_components/pointers/ShadowRootPointer.thy index 71747d8..38660a2 100644 --- a/Core_DOM/pointers/sc_components/ShadowRootPointer.thy +++ b/Core_DOM/sc_components/pointers/ShadowRootPointer.thy @@ -34,7 +34,7 @@ We only include them here, as they are required for future work and they cannot following the object-oriented extensibility of our data model.\ theory ShadowRootPointer imports - "../DocumentPointer" + "DocumentPointer" begin datatype 'shadow_root_ptr shadow_root_ptr = Ref (the_ref: ref) | Ext 'shadow_root_ptr