src/Pure/context.ML
author wenzelm
Fri, 05 Feb 1999 20:57:18 +0100
changeset 6238 bd7b4a23118f
parent 6185 11bf7a8b6a02
child 6261 6dc692fb3d28
permissions -rw-r--r--
setmp: theory option; save;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
6185
11bf7a8b6a02 Global theory context (used to be in Thy/context.ML);
wenzelm
parents:
diff changeset
     1
(*  Title:      Pure/context.ML
11bf7a8b6a02 Global theory context (used to be in Thy/context.ML);
wenzelm
parents:
diff changeset
     2
    ID:         $Id$
11bf7a8b6a02 Global theory context (used to be in Thy/context.ML);
wenzelm
parents:
diff changeset
     3
    Author:     Markus Wenzel, TU Muenchen
11bf7a8b6a02 Global theory context (used to be in Thy/context.ML);
wenzelm
parents:
diff changeset
     4
11bf7a8b6a02 Global theory context (used to be in Thy/context.ML);
wenzelm
parents:
diff changeset
     5
Global theory context.
11bf7a8b6a02 Global theory context (used to be in Thy/context.ML);
wenzelm
parents:
diff changeset
     6
*)
11bf7a8b6a02 Global theory context (used to be in Thy/context.ML);
wenzelm
parents:
diff changeset
     7
11bf7a8b6a02 Global theory context (used to be in Thy/context.ML);
wenzelm
parents:
diff changeset
     8
signature BASIC_CONTEXT =
11bf7a8b6a02 Global theory context (used to be in Thy/context.ML);
wenzelm
parents:
diff changeset
     9
sig
11bf7a8b6a02 Global theory context (used to be in Thy/context.ML);
wenzelm
parents:
diff changeset
    10
  val context: theory -> unit
11bf7a8b6a02 Global theory context (used to be in Thy/context.ML);
wenzelm
parents:
diff changeset
    11
  val the_context: unit -> theory
11bf7a8b6a02 Global theory context (used to be in Thy/context.ML);
wenzelm
parents:
diff changeset
    12
end;
11bf7a8b6a02 Global theory context (used to be in Thy/context.ML);
wenzelm
parents:
diff changeset
    13
11bf7a8b6a02 Global theory context (used to be in Thy/context.ML);
wenzelm
parents:
diff changeset
    14
signature CONTEXT =
11bf7a8b6a02 Global theory context (used to be in Thy/context.ML);
wenzelm
parents:
diff changeset
    15
sig
11bf7a8b6a02 Global theory context (used to be in Thy/context.ML);
wenzelm
parents:
diff changeset
    16
  include BASIC_CONTEXT
11bf7a8b6a02 Global theory context (used to be in Thy/context.ML);
wenzelm
parents:
diff changeset
    17
  val get_context: unit -> theory option
11bf7a8b6a02 Global theory context (used to be in Thy/context.ML);
wenzelm
parents:
diff changeset
    18
  val set_context: theory option -> unit
11bf7a8b6a02 Global theory context (used to be in Thy/context.ML);
wenzelm
parents:
diff changeset
    19
  val reset_context: unit -> unit
6238
bd7b4a23118f setmp: theory option;
wenzelm
parents: 6185
diff changeset
    20
  val setmp: theory option -> ('a -> 'b) -> 'a -> 'b
bd7b4a23118f setmp: theory option;
wenzelm
parents: 6185
diff changeset
    21
  val save: ('a -> 'b) -> 'a -> 'b
6185
11bf7a8b6a02 Global theory context (used to be in Thy/context.ML);
wenzelm
parents:
diff changeset
    22
  val >> : (theory -> theory) -> unit
11bf7a8b6a02 Global theory context (used to be in Thy/context.ML);
wenzelm
parents:
diff changeset
    23
end;
11bf7a8b6a02 Global theory context (used to be in Thy/context.ML);
wenzelm
parents:
diff changeset
    24
11bf7a8b6a02 Global theory context (used to be in Thy/context.ML);
wenzelm
parents:
diff changeset
    25
structure Context: CONTEXT =
11bf7a8b6a02 Global theory context (used to be in Thy/context.ML);
wenzelm
parents:
diff changeset
    26
struct
11bf7a8b6a02 Global theory context (used to be in Thy/context.ML);
wenzelm
parents:
diff changeset
    27
11bf7a8b6a02 Global theory context (used to be in Thy/context.ML);
wenzelm
parents:
diff changeset
    28
11bf7a8b6a02 Global theory context (used to be in Thy/context.ML);
wenzelm
parents:
diff changeset
    29
(* theory context *)
11bf7a8b6a02 Global theory context (used to be in Thy/context.ML);
wenzelm
parents:
diff changeset
    30
11bf7a8b6a02 Global theory context (used to be in Thy/context.ML);
wenzelm
parents:
diff changeset
    31
local
11bf7a8b6a02 Global theory context (used to be in Thy/context.ML);
wenzelm
parents:
diff changeset
    32
  val current_theory = ref (None: theory option);
11bf7a8b6a02 Global theory context (used to be in Thy/context.ML);
wenzelm
parents:
diff changeset
    33
in
11bf7a8b6a02 Global theory context (used to be in Thy/context.ML);
wenzelm
parents:
diff changeset
    34
  fun get_context () = ! current_theory;
11bf7a8b6a02 Global theory context (used to be in Thy/context.ML);
wenzelm
parents:
diff changeset
    35
  fun set_context opt_thy = current_theory := opt_thy;
6238
bd7b4a23118f setmp: theory option;
wenzelm
parents: 6185
diff changeset
    36
  fun setmp opt_thy f x = Library.setmp current_theory opt_thy f x;
6185
11bf7a8b6a02 Global theory context (used to be in Thy/context.ML);
wenzelm
parents:
diff changeset
    37
end;
11bf7a8b6a02 Global theory context (used to be in Thy/context.ML);
wenzelm
parents:
diff changeset
    38
11bf7a8b6a02 Global theory context (used to be in Thy/context.ML);
wenzelm
parents:
diff changeset
    39
fun the_context () =
11bf7a8b6a02 Global theory context (used to be in Thy/context.ML);
wenzelm
parents:
diff changeset
    40
  (case get_context () of
11bf7a8b6a02 Global theory context (used to be in Thy/context.ML);
wenzelm
parents:
diff changeset
    41
    Some thy => thy
11bf7a8b6a02 Global theory context (used to be in Thy/context.ML);
wenzelm
parents:
diff changeset
    42
  | _ => error "Unknown theory context");
11bf7a8b6a02 Global theory context (used to be in Thy/context.ML);
wenzelm
parents:
diff changeset
    43
11bf7a8b6a02 Global theory context (used to be in Thy/context.ML);
wenzelm
parents:
diff changeset
    44
fun context thy = set_context (Some thy);
11bf7a8b6a02 Global theory context (used to be in Thy/context.ML);
wenzelm
parents:
diff changeset
    45
fun reset_context () = set_context None;
11bf7a8b6a02 Global theory context (used to be in Thy/context.ML);
wenzelm
parents:
diff changeset
    46
6238
bd7b4a23118f setmp: theory option;
wenzelm
parents: 6185
diff changeset
    47
fun save f x = setmp (get_context ()) f x;
bd7b4a23118f setmp: theory option;
wenzelm
parents: 6185
diff changeset
    48
6185
11bf7a8b6a02 Global theory context (used to be in Thy/context.ML);
wenzelm
parents:
diff changeset
    49
11bf7a8b6a02 Global theory context (used to be in Thy/context.ML);
wenzelm
parents:
diff changeset
    50
(* map context *)
11bf7a8b6a02 Global theory context (used to be in Thy/context.ML);
wenzelm
parents:
diff changeset
    51
11bf7a8b6a02 Global theory context (used to be in Thy/context.ML);
wenzelm
parents:
diff changeset
    52
nonfix >>;
11bf7a8b6a02 Global theory context (used to be in Thy/context.ML);
wenzelm
parents:
diff changeset
    53
fun >> f = set_context (Some (f (the_context ())));
11bf7a8b6a02 Global theory context (used to be in Thy/context.ML);
wenzelm
parents:
diff changeset
    54
11bf7a8b6a02 Global theory context (used to be in Thy/context.ML);
wenzelm
parents:
diff changeset
    55
11bf7a8b6a02 Global theory context (used to be in Thy/context.ML);
wenzelm
parents:
diff changeset
    56
end;
11bf7a8b6a02 Global theory context (used to be in Thy/context.ML);
wenzelm
parents:
diff changeset
    57
11bf7a8b6a02 Global theory context (used to be in Thy/context.ML);
wenzelm
parents:
diff changeset
    58
structure BasicContext: BASIC_CONTEXT = Context;
11bf7a8b6a02 Global theory context (used to be in Thy/context.ML);
wenzelm
parents:
diff changeset
    59
open BasicContext;