src/Pure/General/secure.ML
author wenzelm
Sun Apr 06 15:19:22 2014 +0200 (2014-04-06 ago)
changeset 56434 7acc933bd7cc
parent 44200 ce0112e26b3b
child 58842 22b87ab47d3b
permissions -rw-r--r--
clarified ML bootstrap;
     1 (*  Title:      Pure/General/secure.ML
     2     Author:     Makarius
     3 
     4 Secure critical operations.
     5 *)
     6 
     7 signature SECURE =
     8 sig
     9   val set_secure: unit -> unit
    10   val is_secure: unit -> bool
    11   val deny_secure: string -> unit
    12   val secure_mltext: unit -> unit
    13   val use_text: use_context -> int * string -> bool -> string -> unit
    14   val use_file: use_context -> bool -> string -> unit
    15   val toplevel_pp: string list -> string -> unit
    16   val PG_setup: unit -> unit
    17   val commit: unit -> unit
    18 end;
    19 
    20 structure Secure: SECURE =
    21 struct
    22 
    23 (** secure flag **)
    24 
    25 val secure = Unsynchronized.ref false;
    26 
    27 fun set_secure () = secure := true;
    28 fun is_secure () = ! secure;
    29 
    30 fun deny_secure msg = if is_secure () then error msg else ();
    31 
    32 
    33 
    34 (** critical operations **)
    35 
    36 (* ML evaluation *)
    37 
    38 fun secure_mltext () = deny_secure "Cannot evaluate ML source in secure mode";
    39 
    40 val raw_use_text = use_text;
    41 val raw_use_file = use_file;
    42 val raw_toplevel_pp = toplevel_pp;
    43 
    44 fun use_text context pos verbose txt = (secure_mltext (); raw_use_text context pos verbose txt);
    45 fun use_file context verbose name = (secure_mltext (); raw_use_file context verbose name);
    46 
    47 fun toplevel_pp path pp = (secure_mltext (); raw_toplevel_pp ML_Parse.global_context path pp);
    48 
    49 
    50 (* global evaluation *)
    51 
    52 val use_global = raw_use_text ML_Parse.global_context (0, "") false;
    53 
    54 fun commit () = use_global "commit();";   (*commit is dynamically bound!*)
    55 
    56 fun PG_setup () =
    57   use_global "val change = Unsynchronized.change; structure ThyLoad = ProofGeneral.ThyLoad;";
    58 
    59 end;
    60