src/Pure/context.ML
author wenzelm
Thu Jul 08 18:31:04 1999 +0200 (1999-07-08)
changeset 6930 4b40fb299f9f
parent 6310 353a8a9d9d2c
child 8348 ebbbfdb35c84
permissions -rw-r--r--
improved error msgs of cterm_instantiate;
fixed incr_indexes;
wenzelm@6185
     1
(*  Title:      Pure/context.ML
wenzelm@6185
     2
    ID:         $Id$
wenzelm@6185
     3
    Author:     Markus Wenzel, TU Muenchen
wenzelm@6185
     4
wenzelm@6185
     5
Global theory context.
wenzelm@6185
     6
*)
wenzelm@6185
     7
wenzelm@6185
     8
signature BASIC_CONTEXT =
wenzelm@6185
     9
sig
wenzelm@6185
    10
  val context: theory -> unit
wenzelm@6185
    11
  val the_context: unit -> theory
wenzelm@6185
    12
end;
wenzelm@6185
    13
wenzelm@6185
    14
signature CONTEXT =
wenzelm@6185
    15
sig
wenzelm@6185
    16
  include BASIC_CONTEXT
wenzelm@6185
    17
  val get_context: unit -> theory option
wenzelm@6185
    18
  val set_context: theory option -> unit
wenzelm@6185
    19
  val reset_context: unit -> unit
wenzelm@6238
    20
  val setmp: theory option -> ('a -> 'b) -> 'a -> 'b
wenzelm@6310
    21
  val pass: theory option -> ('a -> 'b) -> 'a -> 'b * theory option
wenzelm@6310
    22
  val pass_theory: theory -> ('a -> 'b) -> 'a -> 'b * theory
wenzelm@6238
    23
  val save: ('a -> 'b) -> 'a -> 'b
wenzelm@6185
    24
  val >> : (theory -> theory) -> unit
wenzelm@6185
    25
end;
wenzelm@6185
    26
wenzelm@6185
    27
structure Context: CONTEXT =
wenzelm@6185
    28
struct
wenzelm@6185
    29
wenzelm@6185
    30
wenzelm@6185
    31
(* theory context *)
wenzelm@6185
    32
wenzelm@6185
    33
local
wenzelm@6185
    34
  val current_theory = ref (None: theory option);
wenzelm@6185
    35
in
wenzelm@6185
    36
  fun get_context () = ! current_theory;
wenzelm@6185
    37
  fun set_context opt_thy = current_theory := opt_thy;
wenzelm@6238
    38
  fun setmp opt_thy f x = Library.setmp current_theory opt_thy f x;
wenzelm@6185
    39
end;
wenzelm@6185
    40
wenzelm@6185
    41
fun the_context () =
wenzelm@6185
    42
  (case get_context () of
wenzelm@6185
    43
    Some thy => thy
wenzelm@6185
    44
  | _ => error "Unknown theory context");
wenzelm@6185
    45
wenzelm@6185
    46
fun context thy = set_context (Some thy);
wenzelm@6185
    47
fun reset_context () = set_context None;
wenzelm@6185
    48
wenzelm@6310
    49
fun pass opt_thy f x =
wenzelm@6261
    50
  setmp opt_thy (fn x => let val y = f x in (y, get_context ()) end) x;
wenzelm@6261
    51
wenzelm@6310
    52
fun pass_theory thy f x =
wenzelm@6310
    53
  (case pass (Some thy) f x of
wenzelm@6261
    54
    (y, Some thy') => (y, thy')
wenzelm@6261
    55
  | (_, None) => error "Missing ML theory context");
wenzelm@6261
    56
wenzelm@6238
    57
fun save f x = setmp (get_context ()) f x;
wenzelm@6238
    58
wenzelm@6185
    59
wenzelm@6185
    60
(* map context *)
wenzelm@6185
    61
wenzelm@6185
    62
nonfix >>;
wenzelm@6185
    63
fun >> f = set_context (Some (f (the_context ())));
wenzelm@6185
    64
wenzelm@6185
    65
wenzelm@6185
    66
end;
wenzelm@6185
    67
wenzelm@6185
    68
structure BasicContext: BASIC_CONTEXT = Context;
wenzelm@6185
    69
open BasicContext;