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.;
wenzelm@20925
     1
(*  Title:      Pure/General/secure.ML
wenzelm@20925
     2
    Author:     Makarius
wenzelm@20925
     3
wenzelm@20925
     4
Secure critical operations.
wenzelm@20925
     5
*)
wenzelm@20925
     6
wenzelm@20925
     7
signature SECURE =
wenzelm@20925
     8
sig
wenzelm@20977
     9
  val set_secure: unit -> unit
wenzelm@20925
    10
  val is_secure: unit -> bool
wenzelm@26080
    11
  val deny_secure: string -> unit
wenzelm@31330
    12
  val secure_mltext: unit -> unit
wenzelm@30672
    13
  val use_text: use_context -> int * string -> bool -> string -> unit
wenzelm@30672
    14
  val use_file: use_context -> bool -> string -> unit
wenzelm@30625
    15
  val toplevel_pp: string list -> string -> unit
wenzelm@37239
    16
  val PG_setup: unit -> unit
wenzelm@20925
    17
  val commit: unit -> unit
wenzelm@20925
    18
end;
wenzelm@20925
    19
wenzelm@20925
    20
structure Secure: SECURE =
wenzelm@20925
    21
struct
wenzelm@20925
    22
wenzelm@20992
    23
(** secure flag **)
wenzelm@20925
    24
wenzelm@32738
    25
val secure = Unsynchronized.ref false;
wenzelm@20925
    26
wenzelm@20977
    27
fun set_secure () = secure := true;
wenzelm@20925
    28
fun is_secure () = ! secure;
wenzelm@20925
    29
wenzelm@22567
    30
fun deny_secure msg = if is_secure () then error msg else ();
wenzelm@20925
    31
wenzelm@20925
    32
wenzelm@25753
    33
wenzelm@20992
    34
(** critical operations **)
wenzelm@20992
    35
wenzelm@20992
    36
(* ML evaluation *)
wenzelm@20925
    37
wenzelm@20925
    38
fun secure_mltext () = deny_secure "Cannot evaluate ML source in secure mode";
wenzelm@20925
    39
wenzelm@30672
    40
val raw_use_text = use_text;
wenzelm@30672
    41
val raw_use_file = use_file;
wenzelm@30672
    42
val raw_toplevel_pp = toplevel_pp;
wenzelm@20925
    43
wenzelm@30672
    44
fun use_text context pos verbose txt = (secure_mltext (); raw_use_text context pos verbose txt);
wenzelm@30672
    45
fun use_file context verbose name = (secure_mltext (); raw_use_file context verbose name);
wenzelm@23922
    46
wenzelm@30672
    47
fun toplevel_pp path pp = (secure_mltext (); raw_toplevel_pp ML_Parse.global_context path pp);
wenzelm@30625
    48
wenzelm@32739
    49
wenzelm@32739
    50
(* global evaluation *)
wenzelm@32739
    51
wenzelm@32739
    52
val use_global = raw_use_text ML_Parse.global_context (0, "") false;
wenzelm@32739
    53
wenzelm@32739
    54
fun commit () = use_global "commit();";   (*commit is dynamically bound!*)
wenzelm@37239
    55
wenzelm@38799
    56
fun PG_setup () =
wenzelm@38799
    57
  use_global "val change = Unsynchronized.change; structure ThyLoad = ProofGeneral.ThyLoad;";
wenzelm@20925
    58
wenzelm@20925
    59
end;
wenzelm@20925
    60
wenzelm@23978
    61
(*override previous toplevel bindings!*)
wenzelm@21770
    62
val use_text = Secure.use_text;
wenzelm@21770
    63
val use_file = Secure.use_file;
wenzelm@42818
    64
wenzelm@42818
    65
fun use s =
wenzelm@44200
    66
  Position.setmp_thread_data (Position.file_only s)
wenzelm@42818
    67
    (fn () =>
wenzelm@42818
    68
      Secure.use_file ML_Parse.global_context true s
wenzelm@42818
    69
        handle ERROR msg => (writeln msg; error "ML error")) ();
wenzelm@42818
    70
wenzelm@30625
    71
val toplevel_pp = Secure.toplevel_pp;
wenzelm@40748
    72