src/Pure/General/secure.ML
author wenzelm
Fri Nov 25 18:37:14 2011 +0100 (2011-11-25 ago)
changeset 45633 2cb7e34f6096
parent 44200 ce0112e26b3b
child 56434 7acc933bd7cc
permissions -rw-r--r--
retain stderr and include it in syslog, which is buffered and thus increases the chance that users see remains from crashes etc.;
     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 
    61 (*override previous toplevel bindings!*)
    62 val use_text = Secure.use_text;
    63 val use_file = Secure.use_file;
    64 
    65 fun use s =
    66   Position.setmp_thread_data (Position.file_only s)
    67     (fn () =>
    68       Secure.use_file ML_Parse.global_context true s
    69         handle ERROR msg => (writeln msg; error "ML error")) ();
    70 
    71 val toplevel_pp = Secure.toplevel_pp;
    72