src/Pure/Thy/context.ML
author wenzelm
Sat Jun 20 20:18:51 1998 +0200 (1998-06-20)
changeset 5059 dcdb21e53537
parent 5049 bde086cfa597
child 5249 9d7e6f7110ef
permissions -rw-r--r--
renamed Thm(s) back to thm(s);
     1 (*  Title:      Pure/Thy/context.ML
     2     ID:         $Id$
     3     Author:     Markus Wenzel, TU Muenchen
     4 
     5 Global contexts: session and theory.
     6 *)
     7 
     8 signature BASIC_CONTEXT =
     9 sig
    10   val context: theory -> unit
    11   val the_context: unit -> theory
    12   val thm: xstring -> thm
    13   val thms: xstring -> thm list
    14   val Goal: string -> thm list
    15   val Goalw: thm list -> string -> thm list
    16 end;
    17 
    18 signature CONTEXT =
    19 sig
    20   include BASIC_CONTEXT
    21   val get_session: unit -> string list
    22   val add_session: string -> unit
    23   val reset_session: unit -> unit
    24   val welcome: unit -> string
    25   val get_context: unit -> theory option
    26   val set_context: theory option -> unit
    27   val reset_context: unit -> unit
    28   val >> : (theory -> theory) -> unit
    29 end;
    30 
    31 structure Context: CONTEXT =
    32 struct
    33 
    34 
    35 (** session **)
    36 
    37 val current_session = ref ([]: string list);
    38 
    39 fun get_session () = ! current_session;
    40 fun add_session s = current_session := ! current_session @ [s];
    41 fun reset_session () = current_session := [];
    42 
    43 fun welcome () =
    44   "Welcome to Isabelle/" ^
    45     (case get_session () of [] => "Pure" | ss => space_implode "/" ss) ^
    46     " (" ^ version ^ ")";
    47 
    48 
    49 
    50 (** theory context **)
    51 
    52 local
    53   val current_theory = ref (None: theory option);
    54 in
    55   fun get_context () = ! current_theory;
    56   fun set_context opt_thy = current_theory := opt_thy;
    57 end;
    58 
    59 fun the_context () =
    60   (case get_context () of
    61     Some thy => thy
    62   | _ => error "Unknown theory context");
    63 
    64 fun context thy = set_context (Some thy);
    65 fun reset_context () = set_context None;
    66 
    67 
    68 (* map context *)
    69 
    70 nonfix >>;
    71 fun >> f = set_context (Some (f (the_context ())));
    72 
    73 
    74 (* retrieve thms *)
    75 
    76 fun thm name = PureThy.get_thm (the_context ()) name;
    77 fun thms name = PureThy.get_thms (the_context ()) name;
    78 
    79 
    80 (* shortcut goal commands *)
    81 
    82 fun Goal s = Goals.atomic_goal (the_context ()) s;
    83 fun Goalw thms s = Goals.atomic_goalw (the_context ()) thms s;
    84 
    85 
    86 end;
    87 
    88 
    89 structure BasicContext: BASIC_CONTEXT = Context;
    90 open BasicContext;