src/Pure/context.ML
changeset 17340 11f959f0fe6c
parent 17221 6cd180204582
child 17412 e26cb20ef0cc
equal deleted inserted replaced
17339:ab97ccef124a 17340:11f959f0fe6c
    17 end;
    17 end;
    18 
    18 
    19 signature CONTEXT =
    19 signature CONTEXT =
    20 sig
    20 sig
    21   include BASIC_CONTEXT
    21   include BASIC_CONTEXT
    22   exception DATA_FAIL of exn * string
       
    23   (*theory context*)
    22   (*theory context*)
    24   val theory_name: theory -> string
    23   val theory_name: theory -> string
    25   val parents_of: theory -> theory list
    24   val parents_of: theory -> theory list
    26   val ancestors_of: theory -> theory list
    25   val ancestors_of: theory -> theory list
    27   val is_stale: theory -> bool
    26   val is_stale: theory -> bool
   105 
   104 
   106 (** theory data **)
   105 (** theory data **)
   107 
   106 
   108 (* data kinds and access methods *)
   107 (* data kinds and access methods *)
   109 
   108 
   110 exception DATA_FAIL of exn * string;
       
   111 
       
   112 local
   109 local
   113 
   110 
   114 type kind =
   111 type kind =
   115  {name: string,
   112  {name: string,
   116   empty: Object.T,
   113   empty: Object.T,
   121 val kinds = ref (Inttab.empty: kind Inttab.table);
   118 val kinds = ref (Inttab.empty: kind Inttab.table);
   122 
   119 
   123 fun invoke meth_name meth_fn k =
   120 fun invoke meth_name meth_fn k =
   124   (case Inttab.curried_lookup (! kinds) k of
   121   (case Inttab.curried_lookup (! kinds) k of
   125     SOME kind => meth_fn kind |> transform_failure (fn exn =>
   122     SOME kind => meth_fn kind |> transform_failure (fn exn =>
   126       DATA_FAIL (exn, "Theory data method " ^ #name kind ^ "." ^ meth_name ^ " failed"))
   123       EXCEPTION (exn, "Theory data method " ^ #name kind ^ "." ^ meth_name ^ " failed"))
   127   | NONE => sys_error ("Invalid theory data identifier " ^ string_of_int k));
   124   | NONE => sys_error ("Invalid theory data identifier " ^ string_of_int k));
   128 
   125 
   129 in
   126 in
   130 
   127 
   131 fun invoke_name k    = invoke "name" (K o #name) k ();
   128 fun invoke_name k    = invoke "name" (K o #name) k ();
   525 val kinds = ref (Inttab.empty: kind Inttab.table);
   522 val kinds = ref (Inttab.empty: kind Inttab.table);
   526 
   523 
   527 fun invoke meth_name meth_fn k =
   524 fun invoke meth_name meth_fn k =
   528   (case Inttab.curried_lookup (! kinds) k of
   525   (case Inttab.curried_lookup (! kinds) k of
   529     SOME kind => meth_fn kind |> transform_failure (fn exn =>
   526     SOME kind => meth_fn kind |> transform_failure (fn exn =>
   530       DATA_FAIL (exn, "Proof data method " ^ #name kind ^ "." ^ meth_name ^ " failed"))
   527       EXCEPTION (exn, "Proof data method " ^ #name kind ^ "." ^ meth_name ^ " failed"))
   531   | NONE => sys_error ("Invalid proof data identifier " ^ string_of_int k));
   528   | NONE => sys_error ("Invalid proof data identifier " ^ string_of_int k));
   532 
   529 
   533 fun invoke_name k = invoke "name" (K o #name) k ();
   530 fun invoke_name k = invoke "name" (K o #name) k ();
   534 val invoke_init   = invoke "init" #init;
   531 val invoke_init   = invoke "init" #init;
   535 
   532