(* Title:  BaseDefinitions/theoryC.sml

    Author: Walther Neuper

    (c) due to copyright terms

 Probably this structure can be dropped due to improved reflection in Isabelle.

 *)

 signature THEORY_ISAC =

 sig

   eqtype id

   val cut_id: string -> id

   val last_isabelle_thy: theory

   val session_specify_names: id list

   val session_interpret_names: id list

   val get_theory: id -> theory         (* restricted to Isac_Knowledge *)

   val id_to_ctxt: id -> Proof.context

   val to_ctxt: theory -> Proof.context (* inverse of Proof_Context.theory_of *)

   val id_empty: id

   val Isac: 'a -> theory

   val parent_of: theory -> theory -> theory

   val sub_common : theory * theory -> theory

 (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)

   (*NONE*)

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

   val get_thy: id -> theory            (* restricted to session Isac *)

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

 end

 (**)

 structure ThyC(**): THEORY_ISAC(**) =

 struct

 (**)

 type id = string;

 fun cut_id dn = hd (space_explode "." dn);

 val last_isabelle_thy = @{theory Complex_Main}

 val session_specify_names = ["Specify", "MathEngBasic", "Input_Descript",

   "ProgLang", "Auto_Prog", "Prog_Expr", "Tactical", "Prog_Tac", "Program", "ListC", "Calculate",

   "BaseDefinitions", "Know_Store"]

 val session_interpret_names = ["Interpret"]

 fun get_thy thyID =

   if member op = session_specify_names thyID

   then Thy_Info.get_theory ("Specify." ^ thyID)

   else if member op = session_interpret_names thyID

   then Thy_Info.get_theory ("Interpret." ^ thyID)

   else Thy_Info.get_theory ("Isac." ^ thyID);

 fun get_theory thy =   

     if thy = "empty_thy_id"

     then (get_thy "Base_Tools") (*lower bound of Knowledge*)

     else (get_thy thy) handle _ => raise ERROR ("ME_Isa: thy \"" ^ thy ^ "\" not in system");

 fun id_to_ctxt thy' = Proof_Context.init_global (get_theory thy');

 fun to_ctxt thy = Proof_Context.init_global thy;

 val id_empty = "empty_thy_id";

 fun Isac _ = Proof_Context.theory_of (id_to_ctxt "Isac_Knowledge");

 fun parent_of thy1 thy2 = if Context.subthy (thy1, thy2) then thy2 else thy1;

 fun sub_common (thy1, thy2) =

   if Context.subthy (thy1, thy2) then

     thy2

   else if Context.subthy (thy2, thy1) then

       thy1

     else get_theory "Isac_Knowledge"

 (**)end(**)