src/Pure/context.ML
author wenzelm
Fri Dec 14 11:52:54 2001 +0100 (2001-12-14)
changeset 12498 3b0091bf06e8
parent 11819 9283b3c11234
child 14976 65f572245276
permissions -rw-r--r--
changed Thm.varifyT';
     1 (*  Title:      Pure/context.ML
     2     ID:         $Id$
     3     Author:     Markus Wenzel, TU Muenchen
     4     License:    GPL (GNU GENERAL PUBLIC LICENSE)
     5 
     6 Global theory context.
     7 *)
     8 
     9 signature BASIC_CONTEXT =
    10 sig
    11   val context: theory -> unit
    12   val the_context: unit -> theory
    13 end;
    14 
    15 signature CONTEXT =
    16 sig
    17   include BASIC_CONTEXT
    18   val get_context: unit -> theory option
    19   val set_context: theory option -> unit
    20   val reset_context: unit -> unit
    21   val setmp: theory option -> ('a -> 'b) -> 'a -> 'b
    22   val pass: theory option -> ('a -> 'b) -> 'a -> 'b * theory option
    23   val pass_theory: theory -> ('a -> 'b) -> 'a -> 'b * theory
    24   val save: ('a -> 'b) -> 'a -> 'b
    25   val >> : (theory -> theory) -> unit
    26   val ml_output: (string -> unit) * (string -> unit)
    27   val use_mltext: string -> bool -> theory option -> unit
    28   val use_mltext_theory: string -> bool -> theory -> theory
    29   val use_let: string -> string -> string -> theory -> theory
    30   val use_setup: string -> theory -> theory
    31 end;
    32 
    33 structure Context: CONTEXT =
    34 struct
    35 
    36 
    37 (* theory context *)
    38 
    39 local
    40   val current_theory = ref (None: theory option);
    41 in
    42   fun get_context () = ! current_theory;
    43   fun set_context opt_thy = current_theory := opt_thy;
    44   fun setmp opt_thy f x = Library.setmp current_theory opt_thy f x;
    45 end;
    46 
    47 fun the_context () =
    48   (case get_context () of
    49     Some thy => thy
    50   | _ => error "Unknown theory context");
    51 
    52 fun context thy = set_context (Some thy);
    53 fun reset_context () = set_context None;
    54 
    55 fun pass opt_thy f x =
    56   setmp opt_thy (fn x => let val y = f x in (y, get_context ()) end) x;
    57 
    58 fun pass_theory thy f x =
    59   (case pass (Some thy) f x of
    60     (y, Some thy') => (y, thy')
    61   | (_, None) => error "Lost theory context in ML");
    62 
    63 fun save f x = setmp (get_context ()) f x;
    64 
    65 
    66 (* map context *)
    67 
    68 nonfix >>;
    69 fun >> f = set_context (Some (f (the_context ())));
    70 
    71 
    72 (* use ML text *)
    73 
    74 val ml_output = (writeln, error_msg: string -> unit);
    75 fun use_output verb txt = use_text ml_output verb (Symbol.plain_output txt);
    76 
    77 fun use_mltext txt verb opt_thy = setmp opt_thy (fn () => use_output verb txt) ();
    78 fun use_mltext_theory txt verb thy = #2 (pass_theory thy (use_output verb) txt);
    79 
    80 fun use_context txt = use_mltext_theory ("Context.>> (" ^ txt ^ ");") false;
    81 
    82 fun use_let bind body txt =
    83   use_context ("let " ^ bind ^ " = " ^ txt ^ " in\n" ^ body ^ " end");
    84 
    85 val use_setup =
    86   use_let "val setup: (theory -> theory) list" "Library.apply setup";
    87 
    88 
    89 end;
    90 
    91 structure BasicContext: BASIC_CONTEXT = Context;
    92 open BasicContext;