# HG changeset patch # User Walther Neuper # Date 1482401538 -3600 # Node ID a474900d5bd270a581603cbf11df0dafcf4abe9d # Parent ea0691a897ad3b9182a54c823127f850c1a5ab49 note on policy for "open" structures see two previous changesets. diff -r ea0691a897ad -r a474900d5bd2 src/Tools/isac/Interpret/ctree.sml --- a/src/Tools/isac/Interpret/ctree.sml Thu Dec 22 10:39:45 2016 +0100 +++ b/src/Tools/isac/Interpret/ctree.sml Thu Dec 22 11:12:18 2016 +0100 @@ -2509,3 +2509,17 @@ (*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* ) open Ctree ( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*) + +(* policy for "open" structures: +-------------------------------- +The above "open Ctree" creates an unclear situation with structures, in particular in test/. +This is work in progress, but urges to make policy explicit: + +(1) All structures are closed with a signature; this for prepares re-arrangement of structures. +(2) Some structures are pervasive (e.g. Ctree) such, that an "open" ensures readability locally. +(3) test/ is preceeded by "open" for all structures, in order to ease copy&paste from scr/ to test/ + +ad (1) Presently this point is under construction. +ad (2) Such local "open" are kept to a minimum (with the goal to reach Isabelle's state). +ad (3) See https://intra.ist.tugraz.at/hg/isa/file/2ba35efb07b7/test/Tools/isac/Test_Isac.thy#l70 +*)