equal
deleted
inserted
replaced
11 val deny_secure: string -> unit |
11 val deny_secure: string -> unit |
12 val secure_mltext: unit -> unit |
12 val secure_mltext: unit -> unit |
13 val use_text: use_context -> int * string -> bool -> string -> unit |
13 val use_text: use_context -> int * string -> bool -> string -> unit |
14 val use_file: use_context -> bool -> string -> unit |
14 val use_file: use_context -> bool -> string -> unit |
15 val toplevel_pp: string list -> string -> unit |
15 val toplevel_pp: string list -> string -> unit |
16 val Isar_setup: unit -> unit |
|
17 val PG_setup: unit -> unit |
16 val PG_setup: unit -> unit |
18 val commit: unit -> unit |
17 val commit: unit -> unit |
19 val bash_output: string -> string * int |
18 val bash_output: string -> string * int |
20 val bash: string -> int |
19 val bash: string -> int |
21 end; |
20 end; |
54 |
53 |
55 val use_global = raw_use_text ML_Parse.global_context (0, "") false; |
54 val use_global = raw_use_text ML_Parse.global_context (0, "") false; |
56 |
55 |
57 fun commit () = use_global "commit();"; (*commit is dynamically bound!*) |
56 fun commit () = use_global "commit();"; (*commit is dynamically bound!*) |
58 |
57 |
59 fun Isar_setup () = use_global "open Unsynchronized;"; |
58 fun PG_setup () = |
60 fun PG_setup () = use_global "structure ThyLoad = ProofGeneral.ThyLoad;"; |
59 use_global "val change = Unsynchronized.change; structure ThyLoad = ProofGeneral.ThyLoad;"; |
61 |
60 |
62 |
61 |
63 (* shell commands *) |
62 (* shell commands *) |
64 |
63 |
65 fun secure_shell () = deny_secure "Cannot execute shell commands in secure mode"; |
64 fun secure_shell () = deny_secure "Cannot execute shell commands in secure mode"; |