(* 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 id_empty: id

  val Isac: 'a -> theory

  val parent_of: theory -> theory -> theory

  val sub_common : theory * theory -> theory

\<^isac_test>\<open>

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

\<close>

end

(**)

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

struct

(**)

type id = string;

val id_empty = "empty_thy_id";

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", "Calc_Binop",

  "BaseDefinitions", "Know_Store"]

val session_interpret_names = ["Interpret"]

(*this is troublesome since the introduction of sessions*)

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 = id_empty

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

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

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

fun Isac _ = 

 (get_theory "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(**)