(* Title: the calctree

    Author: Walther Neuper 161228

    (c) due to copyright terms

 *)

 signature CTREE =

 sig

   include BASIC_CALC_TREE

   include CALC_TREE_NAVIGATION

   include CALC_TREE_ACCESS

   val get_pblID : state -> Spec.pblID option

 end

 structure Ctree : CTREE =

 struct

   open CTbasic

   open CTnavi

   open CTaccess

 fun get_pblID (pt, (p, _)) =

   let val p' = par_pblobj pt p

   	val (_, pI, _) = get_obj g_spec pt p'

   	val (_, (_, oI, _), _) = get_obj g_origin pt p'

   in

     if pI <> Spec.e_pblID

     then SOME pI

     else

       if oI <> Spec.e_pblID then SOME oI else NONE end;

 end;

 (*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )

   open Ctree;

   open Pos

 ( *\--- ! 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 prepares for 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

 *)