src/Tools/isac/MathEngBasic/ctree.sml
changeset 59674 3da177a07c3e
parent 59662 e3713aaf2735
child 59680 2796db5c718c
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/Tools/isac/MathEngBasic/ctree.sml	Sat Oct 26 13:03:16 2019 +0200
     1.3 @@ -0,0 +1,34 @@
     1.4 +(* Title: the calctree
     1.5 +   Author: Walther Neuper 161228
     1.6 +   (c) due to copyright terms
     1.7 +*)
     1.8 +
     1.9 +signature CTREE =
    1.10 +sig
    1.11 +  include BASIC_CALC_TREE
    1.12 +  include CALC_TREE_NAVIGATION
    1.13 +  include CALC_TREE_ACCESS
    1.14 +end
    1.15 +structure Ctree : CTREE =
    1.16 +struct
    1.17 +  open CTbasic
    1.18 +  open CTnavi
    1.19 +  open CTaccess
    1.20 +end;
    1.21 +(*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
    1.22 +  open Ctree;
    1.23 +( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
    1.24 +
    1.25 +(* policy for "open" structures:
    1.26 +--------------------------------
    1.27 +The above "open Ctree" creates an unclear situation with structures, in particular in test/.
    1.28 +This is work in progress, but urges to make policy explicit:
    1.29 +
    1.30 +(1) All structures are closed with a signature; this prepares for re-arrangement of structures.
    1.31 +(2) Some structures are pervasive (e.g. Ctree) such, that an "open" ensures readability locally.
    1.32 +(3) test/ is preceeded by "open" for all structures, in order to ease copy&paste from scr/ to test/
    1.33 +
    1.34 +ad (1) Presently this point is under construction.
    1.35 +ad (2) Such local "open" are kept to a minimum (with the goal to reach Isabelle's state).
    1.36 +ad (3) See https://intra.ist.tugraz.at/hg/isa/file/2ba35efb07b7/test/Tools/isac/Test_Isac.thy#l70
    1.37 +*)